coq/coq issues and pull requests | Ecosyste.ms: Issues

#17804 - Generate opam files using Dune.

Pull Request - State: closed - Opened by Zimmi48 over 1 year ago - 16 comments
Labels: kind: infrastructure, part: build

#17800 - Add introduction to the section on variants and inductive types in the reference manual

Pull Request - State: closed - Opened by herbelin over 1 year ago - 34 comments
Labels: kind: documentation, part: inductives

#17797 - Move the documentation of Pwd and Cd to the extraction chapter.

Pull Request - State: closed - Opened by Zimmi48 over 1 year ago - 20 comments
Labels: kind: documentation

#17790 - Update the coqide.opam file to match what is accepted in opam-repository.

Pull Request - State: closed - Opened by Zimmi48 over 1 year ago - 6 comments
Labels: kind: infrastructure

#17789 - Fix `Typeclasses Unique Instances` option.

Pull Request - State: open - Opened by Janno over 1 year ago - 12 comments
Labels: kind: fix

#17787 - [stdlib] Some injectivity lemmas for lists

Pull Request - State: closed - Opened by haansn08 over 1 year ago - 7 comments
Labels: part: standard library, kind: enhancement

#17786 - Inductive types and recursive functions documentation needs an intro

Issue - State: closed - Opened by audreyseo over 1 year ago - 4 comments
Labels: kind: documentation

#17785 - Split Docker images in two: one for base and one for edge.

Pull Request - State: closed - Opened by Zimmi48 over 1 year ago - 39 comments
Labels: kind: infrastructure

#17782 - Anomaly when disabling a previously unbound notation in a custom grammar

Issue - State: closed - Opened by charguer over 1 year ago - 1 comment
Labels: part: notations, kind: anomaly

#17780 - Update base Ubuntu image in Dockerfile.

Pull Request - State: closed - Opened by Zimmi48 over 1 year ago - 7 comments
Labels: kind: infrastructure, needs: full CI

#17779 - Update nixpkgs and document upper bound on ANTLR compatibility.

Pull Request - State: closed - Opened by Zimmi48 over 1 year ago - 2 comments
Labels: kind: documentation, kind: infrastructure

#17777 - Expose [Evarconv.unify] as an Ltac2 primitive.

Pull Request - State: open - Opened by rlepigre over 1 year ago
Labels: needs: full CI

#17760 - Flags.in_synterp_phase is not robust to async interruptions

Issue - State: open - Opened by ejgallego over 1 year ago - 7 comments
Labels: priority: blocker

#17742 - Fix memory issue with MathComp 2

Pull Request - State: closed - Opened by proux01 over 1 year ago - 7 comments
Labels: needs: full CI

#17730 - Ltac2: expose Tac2core.throw

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: internal

#17722 - [CI] Test MathComp 2 in CI

Pull Request - State: open - Opened by proux01 over 1 year ago - 9 comments
Labels: needs: rebase, part: CI

#17701 - Experiment to preserve information from typeclass failures

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 9 comments
Labels: needs: progress, kind: user messages, part: typeclasses, needs: full CI

#17700 - [stdlib] remove things deprecated in 8.17

Pull Request - State: open - Opened by andres-erbsen over 1 year ago - 9 comments
Labels: kind: cleanup, part: standard library, needs: overlay

#17700 - [stdlib] remove things deprecated in 8.17

Pull Request - State: open - Opened by andres-erbsen over 1 year ago - 9 comments
Labels: kind: cleanup, part: standard library, needs: overlay

#17698 - Draft: Setup basic cram tests for coqdep

Pull Request - State: closed - Opened by rlepigre over 1 year ago - 5 comments
Labels: needs: discussion, needs: rebase, stale, needs: full CI

#17689 - CI: add ITree

Pull Request - State: closed - Opened by liyishuai over 1 year ago - 6 comments
Labels: kind: infrastructure

#17683 - Release 8.18

Issue - State: open - Opened by gares over 1 year ago
Labels: kind: meta

#17643 - Fix check of applied abbreviations in intern for pattern

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: needs: full CI

#17642 - Improve breaks in debug pprinting

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

#17641 - Stop using QVar.repr (it was only used for printing)

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: cleanup

#17640 - Remove unused Univ.ContextSet.{of_instance,add_instance}

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: kind: cleanup, part: universes, kind: internal

#17639 - Add equations to the explicit bench packages + Improve bench failure detection and reporting

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 4 comments
Labels: kind: infrastructure

#17638 - Guard many unguarded `try..with` expressions

Pull Request - State: open - Opened by LasseBlaauwbroek over 1 year ago - 1 comment

#17637 - [experiment] Build congruence subproofs directly instead of invoking tactics.

Pull Request - State: open - Opened by ppedrot over 1 year ago - 2 comments
Labels: needs: full CI

#17636 - Pass stdlib with default goal selector ! (except ssr)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 5 comments
Labels: kind: cleanup

#17635 - Disable async proofs for output test #17579

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: internal

#17634 - Add `assert is_interactive` in Stm.edit_at

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 2 comments
Labels: part: STM, kind: internal

#17633 - Move Termops.decompose_app_vect to EConstr, rename decompose_app->decompose_app_list, decompose_app_vect->decompose_app

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: kind: cleanup, kind: internal

#17632 - CI: produce time log even when failing

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 4 comments
Labels: kind: enhancement, part: CI

#17631 - Remove unused Grammar.Parsable.consume

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: cleanup

#17630 - Check that the env is evar free before using the kernel in Check/Eval

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: fix

#17629 - coqpp: do not print line annotation when loc is dummy

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: fix, kind: infrastructure, part: tools

#17628 - Fix stage of generic_notation_printing_rules

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: fix

#17626 - Primitive integer computation loops

Issue - State: open - Opened by ppedrot over 1 year ago - 2 comments
Labels: part: primitive types

#17624 - CoqIde Menus Not Working on macOS Ventura 13.3.1

Issue - State: open - Opened by ali-ghanbari over 1 year ago - 2 comments

#17623 - Expose `interp_search_request` in API

Pull Request - State: closed - Opened by maximedenes over 1 year ago - 1 comment
Labels: kind: internal, part: search

#17622 - Fix calls to partial summary unfreeze

Pull Request - State: closed - Opened by maximedenes over 1 year ago - 3 comments
Labels: kind: internal

#17619 - Incorrect handling of sort qualities in Coercion.unify_product

Issue - State: closed - Opened by SkySkimmer over 1 year ago

#17618 - Small Pp cleanup

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 5 comments
Labels: kind: cleanup

#17617 - Tactics in terms breaks binders in notations.

Issue - State: open - Opened by jlottes over 1 year ago - 1 comment

#17616 - Provide API for elpi-style import time vernac extends

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 3 comments

#17615 - Check declared section variables of axioms in the kernel

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: kind: fix, kind: cleanup, part: kernel, needs: full CI

#17614 - Kernel does not check declared section variables for axioms

Issue - State: open - Opened by SkySkimmer over 1 year ago

#17613 - Kernel: preserve univ info in conversion errors

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: needs: full CI

#17612 - Typeclass instance hints are added by cache_function not rebuild

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: cleanup

#17611 - TC declaration observer API

Pull Request - State: closed - Opened by gares over 1 year ago - 4 comments
Labels: kind: feature

#17610 - -vio and -vos hang with par:

Issue - State: open - Opened by SkySkimmer over 1 year ago

#17609 - Ltac2 @ external questions

Issue - State: closed - Opened by jfehrle over 1 year ago - 1 comment
Labels: kind: question, part: ltac2

#17608 - Ltac2 open_constr fails when multiple goals are focused

Issue - State: open - Opened by jfehrle over 1 year ago - 2 comments
Labels: kind: documentation, part: ltac2

#17607 - Fix incorrect env variable in render_line_results

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: kind: fix, kind: infrastructure

#17606 - Generalize lemmas from `Z` to `Numbers`.

Issue - State: open - Opened by HaoYang670 over 1 year ago

#17605 - Fix inverted logic in `Summary.ref ~local:true`

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 4 comments
Labels: kind: redesign, kind: fix

#17604 - Experiment: use debruijn instead of ids for the ltac2 interp env

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 2 comments
Labels: needs: full CI

#17603 - Latin subscripts in PDF manual

Issue - State: open - Opened by akr over 1 year ago - 2 comments

#17602 - Refman debug mode

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 7 comments
Labels: kind: infrastructure

#17601 - add deprecation warnings to Numbers.Cyclic.ZModulo.ZModulo

Pull Request - State: closed - Opened by andres-erbsen over 1 year ago - 7 comments
Labels: kind: user messages, part: standard library

#17600 - EConstr term equality: ignore universes with Irrelevant variance

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 2 comments

#17599 - Don't leave an open proof in implicit-arguments.rst

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 5 comments
Labels: kind: documentation

#17598 - Doc: Remove duplicate `match_term_context` label in ltac2.rst

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: documentation

#17597 - Ltac2 multimatch: preserve backtracking error from last branch

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 6 comments
Labels: kind: fix

#17596 - Unexpected coqtop message.

Issue - State: closed - Opened by akr over 1 year ago - 3 comments

#17595 - [ci] quick fix for MC 2.0 release

Pull Request - State: closed - Opened by gares over 1 year ago - 9 comments
Labels: kind: infrastructure

#17594 - Backtracking failure reported as `Match_failure` but doesn't identify the construct that failed

Issue - State: open - Opened by jfehrle over 1 year ago
Labels: part: ltac2

#17593 - Polymorphic Inductive Cumulativity causing match goal to distinguish "identical" terms

Issue - State: open - Opened by jlottes over 1 year ago - 2 comments

#17592 - In interactive mode, print with exninfo before resetting state

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 6 comments
Labels: kind: fix, part: STM, part: toplevel

#17591 - Do not let field_simplify mess with side conditions (fix #17584).

Pull Request - State: open - Opened by silene over 1 year ago - 4 comments
Labels: kind: fix, part: ring/field

#17590 - Fast path in the Tacticals.check_evars function.

Pull Request - State: open - Opened by ppedrot over 1 year ago - 6 comments
Labels: kind: performance

#17589 - Fixes #17583: regression using numerals in the syntax of tactic notations

Pull Request - State: open - Opened by herbelin over 1 year ago - 2 comments
Labels: kind: fix, part: tactics, part: notations

#17588 - More informative "expression does not evaluate to a tactic"

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: user messages

#17587 - Fix insertion of default timeout

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: fix

#17586 - Reject Timeout 0, correctly handle when synterp takes longer than the timeout without getting a signal.

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 4 comments
Labels: kind: fix

#17585 - Revised warning API: warnings can have multiple categories

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 7 comments
Labels: kind: user messages

#17584 - field_simplify creates goal "False" in simple case

Issue - State: open - Opened by MSoegtropIMC over 1 year ago - 5 comments

#17583 - Syntax error: [natural] expected after 'Extern' (in [hint]).

Issue - State: open - Opened by jlottes over 1 year ago - 2 comments
Labels: part: tactics, part: notations, kind: regression

#17582 - Move Discharge.result type to Term_typing and stop exposing it

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: cleanup

#17581 - [test] Hack a bench for mattam82/Coq-Equations#547.

Pull Request - State: closed - Opened by ppedrot over 1 year ago - 2 comments
Labels: needs: full CI

#17580 - Combining Timeout and Default Timeout misbehaves

Issue - State: open - Opened by Columbus240 over 1 year ago - 1 comment

#17579 - Anomaly if timeout is zero on Linux

Issue - State: closed - Opened by Columbus240 over 1 year ago - 2 comments

#17578 - Ltac2: improve "tactic definition must be a syntactical value" error

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 4 comments
Labels: kind: user messages

#17577 - Puzzling error message for "Ltac2 x := apply I."

Issue - State: closed - Opened by jfehrle over 1 year ago
Labels: part: ltac2, kind: usability

#17576 - Let with Qed: produce really-Qed side definition

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 16 comments
Labels: needs: rebase

#17575 - ltac2val:() quotation in ltac1 to return Ltac1.t values

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: kind: enhancement

#17574 - Keep anticipate synterp objects even for sealed modules

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: fix

#17573 - Add debug printer for dirpath maps

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: infrastructure

#17572 - Run coqchk on tests in bugs/

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: infrastructure

#17571 - coqchk failure with module aliasing

Issue - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: part: checker, kind: bug

#17570 - coqchk missing dependencies from opaque modules

Issue - State: open - Opened by SkySkimmer over 1 year ago
Labels: part: checker, kind: bug

#17569 - Ltac2: use ValExt for uint63 and float64

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 6 comments
Labels: kind: cleanup

#17568 - gen_rules improvements: remove -fake-source, allow cross dependencies between theories/ and Ltac2/

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 5 comments
Labels: kind: infrastructure, part: build

#17567 - coqdep error could not find META.* should not be fatal

Issue - State: closed - Opened by JasonGross over 1 year ago - 2 comments
Labels: resolved: invalid, part: coqdep

#17566 - Legacy unification (`apply`) + `Polymorphic Inductive Cumulativity` results in confusing and suspicious differences between evar and evar-free behavior

Issue - State: open - Opened by JasonGross over 1 year ago - 2 comments
Labels: part: universes, part: unification, part: apply

GitHub / coq/coq issues and pull requests