Jason Gross
Jason Gross
I'd like a mode, a la [etherpad](https://etherpad.org/), that allows collaborative editing. I think editing should be collaborative, but evaluation of Coq should be able to be either local or synchronized....
This allows syntax such as ```coq Check [seq '(x, y) x + y) (zip (iota 0 5) (iota 0 5)). ``` prints as the ugly ```coq [seq (let '(x, y)...
Currently, neither of these works with PG; the first gets passed as `-set LooseHintBehavior=Strict`, while the second gets passed as `-set "'Loose" "Hint Behavior=Strict'"`, it seems (based on `Don't know...
If my `_CoqProject` file contains ``` -arg "-w '-deprecated-appcontext -notation-overridden'" ``` then PG is unable to start coqtop. It seems that it tries to pass `"-w" "'-deprecated-appcontext" "-notation-overridden'"` to `coqtop`,...
At https://github.com/coq-community/run-coq-bug-minimizer/runs/4123345900?check_suite_focus=true#step:5:46597 ``` *** No rule to make target '/builds/coq/coq/_build_ci/metacoq/template-coq/gen-src/datatypes.cmx', needed by 'gen-src/metacoq_template_plugin.cmx'. Stop. ``` You can recreate this (for now) by downloading the artifacts at https://gitlab.com/coq/coq/-/jobs/1750733291/artifacts/download and https://gitlab.com/coq/coq/-/jobs/1750733365/artifacts/download. This...
https://metacoq.github.io/coqcoqcorrect says "The general documentation of the MetaCoq project also applies to this version." where "documentation" points to https://metacoq.github.io/documentation which is a 404
If I want to set COQPATH for a particular project (or even globally), there doesn't seem to be any documentation on how to do this. Having something like ```json {...
This backwards compatible change makes math-classes work with coq/coq#10760 by replacing all instances of `rapply` which were relying on typeclass resolution happening *before* `refine` (instead of simultaneously with it) to...
### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...