Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / coq/coq issues and pull requests

#20262 - Add local qualities to env when Check calls kernel typechecking

Pull Request - State: open - Opened by SkySkimmer 1 day ago
Labels: kind: fix

#20261 - Error undeclared quality with Check

Issue - State: open - Opened by SkySkimmer 1 day ago
Labels: kind: bug

#20260 - Print rigid qualities in sorts even if print universes is off

Pull Request - State: open - Opened by SkySkimmer 1 day ago
Labels: kind: user messages

#20259 - CI: Lean importer repo moved to coq community

Pull Request - State: closed - Opened by SkySkimmer 1 day ago - 1 comment
Labels: kind: infrastructure, part: CI

#20258 - Bench add invariant for rocq-runtime

Pull Request - State: open - Opened by SkySkimmer 1 day ago - 1 comment
Labels: kind: infrastructure

#20257 - experiment put proofs in main vo segment

Pull Request - State: open - Opened by SkySkimmer 1 day ago - 1 comment
Labels: needs: full CI

#20256 - Rocqide try to fix incorrect character conversions

Pull Request - State: open - Opened by SkySkimmer 1 day ago - 2 comments
Labels: kind: fix, part: CoqIDE

#20255 - Fix bench false positive detection of failed dependency

Pull Request - State: closed - Opened by SkySkimmer 2 days ago - 3 comments
Labels: kind: infrastructure

#20254 - Anomaly "Uncaught exception Not_found." by including a module type in a module

Issue - State: open - Opened by chatpion 2 days ago
Labels: kind: bug, needs: triage

#20253 - coqdev.el stop using the shim

Pull Request - State: closed - Opened by SkySkimmer 2 days ago - 1 comment
Labels: kind: infrastructure

#20252 - Try fixing unification of projections

Pull Request - State: open - Opened by mattam82 2 days ago - 4 comments

#20251 - Anomaly "File "pretyping/retyping.ml", line 143, characters 10-16: Assertion failed." with `Set Debug "tactic-unification"`

Issue - State: open - Opened by Tragicus 2 days ago - 3 comments
Labels: kind: bug, needs: triage, needs: minimization

#20250 - CI: Fix elpi

Pull Request - State: closed - Opened by SkySkimmer 2 days ago - 3 comments
Labels: kind: infrastructure

#20249 - Retype in eta_constructor

Pull Request - State: open - Opened by Tragicus 2 days ago - 4 comments
Labels: needs: fixing, needs: full CI

#20248 - check_evar_instance produce nicer error when retyping fails

Pull Request - State: open - Opened by SkySkimmer 2 days ago - 3 comments
Labels: kind: user messages

#20247 - `Unset Universe Checking` unifies all sorts

Pull Request - State: open - Opened by JasonGross 3 days ago - 3 comments
Labels: kind: fix, part: kernel, part: universes, part: sort polymorphism

#20246 - Unification loop / stack overflow

Issue - State: open - Opened by EugeneFlesselle 3 days ago - 2 comments
Labels: kind: bug

#20245 - Ltac2 should support direct manipulation of sorts, universe instances, and constraints

Issue - State: open - Opened by JasonGross 4 days ago
Labels: part: universes, part: ltac2, kind: wish, part: sort polymorphism

#20244 - Rely on explicit printing of pairs of terms in some module errors

Pull Request - State: open - Opened by ppedrot 5 days ago
Labels: kind: fix, needs: test-suite update

#20243 - Ltac2.Constr.in_context don't drop goal state

Pull Request - State: open - Opened by SkySkimmer 5 days ago - 2 comments
Labels: kind: fix, part: ltac2

#20242 - "Signature components for field ... do not match: expected type ... but found type ..." should never print identical types for the expected and found type

Issue - State: open - Opened by JasonGross 5 days ago - 1 comment
Labels: kind: user messages, part: modules, kind: bug, part: sort polymorphism

#20241 - The kernel should permit differing sorts/qualities on sort-polymorphic inductives when `Universe Checking` is unset

Issue - State: open - Opened by JasonGross 5 days ago - 4 comments
Labels: kind: bug, part: sort polymorphism

#20239 - ssrmatching cleanups

Pull Request - State: closed - Opened by SkySkimmer 6 days ago - 2 comments
Labels: kind: cleanup

#20238 - Update comment in ssreflect.SsrSyntax

Pull Request - State: closed - Opened by SkySkimmer 6 days ago - 3 comments
Labels: kind: cleanup, part: ssreflect

#20237 - ci: bump sel to 0.6.0

Pull Request - State: closed - Opened by gares 6 days ago - 3 comments
Labels: kind: infrastructure

#20236 - ROCQ_PROFILE_COMPONENTS handle negated list

Pull Request - State: open - Opened by SkySkimmer 7 days ago
Labels: kind: internal

#20235 - Print/About print arguments with DelimOnlyTmpScope

Pull Request - State: closed - Opened by SkySkimmer 7 days ago - 3 comments
Labels: kind: fix, kind: user messages

#20234 - Print/About print binding instances in binder style

Pull Request - State: open - Opened by SkySkimmer 7 days ago - 1 comment
Labels: kind: user messages

#20233 - Stop using deprecated typing.io in python code

Pull Request - State: closed - Opened by SkySkimmer 7 days ago - 2 comments
Labels: kind: documentation

#20232 - refman-pdf deeper table of contents

Pull Request - State: open - Opened by SkySkimmer 7 days ago - 5 comments
Labels: kind: documentation

#20231 - Clarify Set Definitional UIP effect

Pull Request - State: closed - Opened by SkySkimmer 7 days ago - 2 comments
Labels: kind: documentation

#20230 - Delay getenv calls

Pull Request - State: closed - Opened by SkySkimmer 7 days ago - 5 comments
Labels: kind: fix

#20229 - "Warning, feedback message received but no listener to handle it!"

Issue - State: closed - Opened by proux01 7 days ago
Labels: kind: user messages, kind: bug

#20228 - Timeout doesn't work

Issue - State: open - Opened by OwenConoly 8 days ago - 8 comments
Labels: platform: Windows, kind: bug, needs: triage

#20227 - Evd.is_maybe_typeclass_hook uses econstr

Pull Request - State: closed - Opened by SkySkimmer 8 days ago - 1 comment
Labels: kind: cleanup

#20226 - Warning when generating a constraint involving a template universe

Pull Request - State: open - Opened by SkySkimmer 8 days ago
Labels: kind: user messages, needs: full CI

#20225 - recheck_against don't generate spurious template constraints

Pull Request - State: open - Opened by SkySkimmer 8 days ago - 2 comments
Labels: kind: fix

#20224 - `destruct` generates spurious template constraints

Issue - State: open - Opened by SkySkimmer 8 days ago
Labels: kind: bug

#20223 - Cases do not generate spurious template constraints in `in ...`

Pull Request - State: open - Opened by SkySkimmer 8 days ago - 2 comments
Labels: kind: fix

#20221 - Fix falsely general type variables in Ltac2.List

Pull Request - State: closed - Opened by SkySkimmer 8 days ago - 2 comments
Labels: kind: fix

#20220 - Ltac2 Fresh.Free using Nameops.Fresh, add convenience APIs

Pull Request - State: open - Opened by SkySkimmer 9 days ago - 1 comment
Labels: kind: enhancement, part: ltac2

#20219 - Add Evd.set_eq_qualities and set_above_prop

Pull Request - State: closed - Opened by SkySkimmer 9 days ago - 3 comments
Labels: kind: cleanup

#20218 - Let binder (x:T|P) not depend on the implicit status of sig.

Pull Request - State: closed - Opened by SkySkimmer 9 days ago - 1 comment
Labels: kind: enhancement

#20217 - Tac2ffi stop exposing the raw tags

Pull Request - State: closed - Opened by SkySkimmer 9 days ago - 7 comments
Labels: kind: cleanup

#20216 - coqc -config should include OCAMLPATH

Issue - State: open - Opened by JasonGross 10 days ago - 2 comments
Labels: kind: wish

#20215 - Avoid constructing lists while processing hints

Pull Request - State: closed - Opened by SkySkimmer 10 days ago - 17 comments

#20214 - bench export ROCQ_PROFILE_COMPONENTS instead of COQ_...

Pull Request - State: closed - Opened by SkySkimmer 10 days ago - 1 comment
Labels: kind: cleanup

#20213 - Fix rocq dep issue with empty string arguments

Pull Request - State: closed - Opened by Janno 11 days ago - 6 comments
Labels: kind: fix, part: coqdep

#20212 - coqc hangs on processing a comment & Require Import on Windows, consuming all available memory

Issue - State: closed - Opened by JasonGross 11 days ago - 4 comments
Labels: platform: Windows, kind: bug, needs: triage, needs: minimization

#20211 - coqc should error when not given a .v file

Issue - State: open - Opened by JasonGross 12 days ago - 4 comments
Labels: kind: user messages, kind: wish

#20210 - eexists and eexists ?[e] behave differently.

Issue - State: open - Opened by rnrand 12 days ago
Labels: kind: bug, needs: triage

#20209 - `rocq dep` fails on attributes with empty string values in commands that take string arguments

Issue - State: closed - Opened by Janno 12 days ago - 2 comments
Labels: kind: regression, kind: bug, part: coqdep

#20208 - coqrst: replace `extra` by `extra-foo` telling what it depends on

Pull Request - State: closed - Opened by SkySkimmer 12 days ago - 1 comment
Labels: kind: documentation

#20207 - Ltac2 external check that the name is not already used

Pull Request - State: closed - Opened by SkySkimmer 12 days ago - 1 comment
Labels: kind: fix, part: ltac2

#20206 - Ltac2 APIs to manipulate local environments

Pull Request - State: open - Opened by SkySkimmer 12 days ago - 4 comments
Labels: kind: feature, part: ltac2

#20204 - Do not rely on name canonization in CS cache.

Pull Request - State: open - Opened by ppedrot 13 days ago - 7 comments
Labels: kind: cleanup

#20203 - Bench: add coq-elpi to explicit packages

Pull Request - State: closed - Opened by SkySkimmer 13 days ago - 3 comments
Labels: kind: infrastructure

#20202 - Add changelog for #19160

Pull Request - State: closed - Opened by SkySkimmer 13 days ago
Labels: kind: documentation

#20201 - Abstract the datatype of maps of hint modes.

Pull Request - State: closed - Opened by ppedrot 13 days ago - 8 comments
Labels: kind: cleanup

#20200 - Description of definitional UIP is ambiguous

Issue - State: closed - Opened by JasonGross 14 days ago - 1 comment
Labels: kind: documentation, kind: user messages, kind: wish

#20199 - Non-linear variable pattern in Ltac2 considered an unused variable.

Issue - State: closed - Opened by jpoiret 14 days ago - 1 comment
Labels: kind: bug, needs: triage

#20198 - fix bench (coq-bignums -> rocq-bignums)

Pull Request - State: closed - Opened by SkySkimmer 14 days ago - 1 comment
Labels: kind: infrastructure

#20197 - Add Ltac2 notation for rename.

Pull Request - State: open - Opened by jpoiret 14 days ago
Labels: needs: full CI

#20197 - Add Ltac2 notation for rename.

Pull Request - State: open - Opened by jpoiret 14 days ago
Labels: needs: full CI

#20196 - Collapse environment fields and remove dead API.

Pull Request - State: closed - Opened by ppedrot 14 days ago - 1 comment
Labels: kind: cleanup, part: kernel

#20195 - Stop relying on canonicalizing maps in the section mechanism.

Pull Request - State: closed - Opened by ppedrot 15 days ago - 1 comment
Labels: kind: cleanup

#20194 - [9.0] [CI] Fix stdlib-doc

Pull Request - State: closed - Opened by proux01 15 days ago - 1 comment
Labels: kind: infrastructure

#20193 - Please add the ability to add arbitrary open statements to extracted Ocaml code

Issue - State: open - Opened by llee454 16 days ago - 1 comment
Labels: part: extraction, needs: triage, kind: wish

#20192 - Reduce the reliance on CanOrd in upper layers

Pull Request - State: closed - Opened by ppedrot 16 days ago - 1 comment
Labels: kind: cleanup

#20191 - Remove automatic adding of coqbin to PATH on windows in envars

Pull Request - State: open - Opened by SkySkimmer 16 days ago - 13 comments
Labels: kind: cleanup, platform: Windows

#20190 - Handle queries in rocqshim when possible

Pull Request - State: closed - Opened by SkySkimmer 16 days ago - 6 comments
Labels: kind: fix, kind: cleanup, part: build

#20189 - [CI] Fix stdlib-doc

Pull Request - State: closed - Opened by proux01 16 days ago - 5 comments
Labels: kind: infrastructure

#20188 - "The variable Notation variable x is not available was not found in the current environment." should be more informative

Issue - State: open - Opened by JasonGross 17 days ago - 2 comments
Labels: kind: user messages, part: ltac2, kind: wish

#20187 - Ltac2 format %a should be `'a -> message` not `unit -> 'a -> message`

Issue - State: open - Opened by JasonGross 17 days ago - 1 comment
Labels: kind: question, kind: bug, part: ltac2

#20186 - `Ltac2.Control` {throw,assert} functions take formats

Pull Request - State: open - Opened by JasonGross 17 days ago - 2 comments
Labels: needs: progress, kind: enhancement, part: ltac2, needs: full CI

#20185 - Request: quality analogue of `max` (or: ability to have primitive projections on more complicated sort-polymorphic records)

Issue - State: closed - Opened by JasonGross 17 days ago - 1 comment
Labels: resolved: won't fix, part: primitive records, kind: wish, part: sort polymorphism

#20184 - Add Ltac2.Option.{is_some,is_none,compare,join,iter}

Pull Request - State: closed - Opened by JasonGross 17 days ago - 1 comment
Labels: kind: enhancement, part: ltac2

#20183 - Use sets instead of ordered lists in hint stored data.

Pull Request - State: closed - Opened by ppedrot 17 days ago - 13 comments
Labels: kind: performance

#20182 - Rename and tweak Modops.add_module_type.

Pull Request - State: closed - Opened by ppedrot 18 days ago - 1 comment
Labels: kind: cleanup

#20181 - Set Printing Parentheses does not work as expected

Issue - State: closed - Opened by eerio 18 days ago - 2 comments
Labels: kind: bug

#20180 - Issue template: suggest mentioning which interface gets the bug

Pull Request - State: closed - Opened by SkySkimmer 18 days ago - 1 comment
Labels: kind: infrastructure

#20179 - Uncaught Exception

Issue - State: closed - Opened by mukeshtiwari 18 days ago - 2 comments
Labels: kind: bug, needs: triage

#20178 - Keep qvar in template poly entry and declarations

Pull Request - State: closed - Opened by SkySkimmer 19 days ago - 13 comments
Labels: kind: redesign

#20177 - Generate Sort poly eliminator

Pull Request - State: open - Opened by jpoiret 19 days ago - 28 comments

#20176 - Stop relying on a global visit state in extraction.

Pull Request - State: closed - Opened by ppedrot 19 days ago - 1 comment
Labels: kind: cleanup

#20175 - Support primitive operations in old and new unification.

Pull Request - State: open - Opened by Janno 19 days ago - 10 comments
Labels: kind: fix, needs: benchmarking, part: unification, needs: changelog entry, part: primitive types, needs: full CI

#20174 - Fix ci-equations_tests CI script.

Pull Request - State: closed - Opened by ppedrot 20 days ago - 3 comments
Labels: kind: infrastructure

#20173 - Fix equations install

Pull Request - State: closed - Opened by SkySkimmer 20 days ago - 1 comment
Labels: kind: infrastructure

#20172 - Fix whitespace in rocq usage command

Pull Request - State: closed - Opened by mattam82 20 days ago - 3 comments
Labels: kind: fix, kind: user messages

#20171 - Do not add functor delta-resolvers when strengthening.

Pull Request - State: closed - Opened by ppedrot 20 days ago - 1 comment
Labels: kind: fix

#20170 - Additional cleanups around the module implementation

Pull Request - State: closed - Opened by ppedrot 20 days ago - 3 comments
Labels: kind: cleanup

#20169 - Move timelog2html implementation to rocq-devtools package

Pull Request - State: closed - Opened by SkySkimmer 20 days ago - 3 comments
Labels: kind: infrastructure

#20168 - Changes for 9.0, with porting instructions and renaming advice

Pull Request - State: open - Opened by mattam82 20 days ago
Labels: needs: full CI

#20167 - Remove dead API in Tok.

Pull Request - State: closed - Opened by ppedrot 20 days ago - 9 comments
Labels: kind: cleanup

#20166 - [ci] Equations: use dune commands directly

Pull Request - State: closed - Opened by mattam82 20 days ago - 3 comments
Labels: kind: infrastructure

#20165 - Export a view type over Environ.env for Serlib and abstract env away.

Pull Request - State: closed - Opened by ppedrot 20 days ago - 5 comments
Labels: kind: cleanup

#20164 - Bench explicit package is rocq-equations not coq-equations

Pull Request - State: closed - Opened by SkySkimmer 20 days ago - 5 comments
Labels: kind: infrastructure