aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-04[dune] [ide] Don't install the internal CoqIDE UI library.Emilio Jesus Gallego Arias
This library is unstable and not meant to be consumed by anyone. We thus make it private.
2019-03-04Merge PR #9660: Set COQLIB so the test suite runs locally on Windows.Enrico Tassi
Reviewed-by: ejgallego Ack-by: SkySkimmer Ack-by: gares Ack-by: jfehrle Ack-by: vbgl
2019-03-04Merge PR #9594: When Nix build is finished and pushed to Cachix, update a ↵Maxime Dénès
specific branch. Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: maximedenes Reviewed-by: vbgl
2019-03-04Merge PR #9047: [dune] Shim for starting `coqtop/coqide` with minimal config.Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-03-03[dune] Shim for starting `coqtop/coqide` with minimal config.Emilio Jesus Gallego Arias
As requested by Gaëtan Gilbert, we add shims - `dev/shim/coqtop-prelude` - `dev/shim/coqide-prelude` that will build and start `coqtop` and `coqide` with just the prelude loaded properly. `dune exec dev/shim/coqtop-prelude` will build and execute this shim, equivalent to doing `make states && bin/coqtop` under the old model. This PR is just a bit of "a hack" until proper support for Coq libraries arrives to Dune, however there is nothing wrong with it. In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to compute the full installation path to allow `%{bin:foo}` in deps, [this is a kind of shortcoming of the current implementation, and the error message is just terrible] We cannot depend on installed `.vo` files without doing a gross hack [including them inside an ml lib] so for now we just depend on their non-installed forms. Using `%{bin}` is good enough for the shims who would like to locate binaries using `PATH`. The long term plan (for now) is to have a command similar to `dune utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell with the corresponding libraries on the path. This will work for `dir=stdlib/Init/` for example, or for any other combination.
2019-03-01Merge PR #9676: Move test_mode from Flags to Vernacentries (use point)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Merge PR #9624: [Kernel] Simpler generation of opcode filesEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: rgrinberg Ack-by: vbgl
2019-03-01Merge PR #9677: Update coqdev.el to use -topfileEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Set COQLIB so the test suite will run locally on Windows.Jim Fehrle
2019-03-01When Nix build is finished and pushed to Cachix, update a specific branch.Théo Zimmermann
This should allow CI jobs that use our Cachix to only test against Coq versions that are already available in Cachix, avoiding very long build and time outs e.g. in the math-classes CI. Co-authored-by: Vincent Laporte <Vincent.Laporte@inria.fr>
2019-03-01Merge PR #9626: [lib] Add `Map.update` from OCaml 4.06Pierre-Marie Pédrot
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-03-01[Kernel] Simpler generation of opcode filesVincent Laporte
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program rather than a pipeline of sed and awk text processing.
2019-03-01write_uint63.ml: add headerVincent Laporte
2019-03-01Merge PR #9006: [dune] Add quickide target for building of IDE.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-03-01Update coqdev.el to use -topfileGaëtan Gilbert
PG would do it by default but since we override coq-prog-args it doesn't.
2019-03-01Move test_mode from Flags to Vernacentries (use point)Gaëtan Gilbert
2019-03-01[dune] Add quickide target for building of IDE.Emilio Jesus Gallego Arias
Note that `states` doesn't work reliably yet, but that is a separate problem that will be fixed in Dune 1.6. [Or we could also fix it improving the rules in envars.ml]
2019-03-01Merge PR #9656: Fix deprecation warningEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Merge PR #9610: Fix #9110: mention check-owners-pr.shEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: vbgl
2019-03-01Merge PR #9619: Print location for type error in pattern variableEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Merge PR #9672: [doc] ssr: Fix the documentation of `by [tacs]`Théo Zimmermann
Reviewed-by: gares
2019-03-01[doc] ssr: Fix the documentation of `by [tacs]`Erik Martin-Dorel
Closes coq/coq#9669
2019-02-28Fix #9110: mention check-owners-pr.shThéo Zimmermann
2019-02-28Merge PR #9621: [ide] only use Coq_config for the URL of the manualPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-02-28Print location for type error in pattern variableGaëtan Gilbert
See #9616
2019-02-28[Gitlab-CI] Creates a deploy-templateVincent Laporte
To be used when pushing an artifact to a github repository
2019-02-28Merge PR #9578: Document primitive integersThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-02-28Merge PR #9649: [dune] Simple rule to generate Stdlib's documentation.Théo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-02-27[ide] only use Coq_config for the URL of the manualEnrico Tassi
2019-02-27Merge PR #9622: Fix makefile deps for coqidePierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-02-27[make] coqide target needs STM workersEnrico Tassi
2019-02-27[ide] coqtop -> coqidetop in user messagesEnrico Tassi
2019-02-26[dune] Simple rule to generate Stdlib's documentation.Emilio Jesus Gallego Arias
Ideally this will be handled by Dune's native library support, but this could be useful for the likes of #9648. I am not sure what should be done w.r.t. style files.
2019-02-26Merge PR #9612: Fix #9526: Registering inductives for primitive integers ↵Vincent Laporte
doesn't check enough Ack-by: SkySkimmer Reviewed-by: vbgl
2019-02-26Fix deprecation warningEnrico Tassi
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-26Merge PR #9648: [Gitlab-CI] Deploy api documentation to GH-PagesEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: vbgl
2019-02-26Merge PR #9653: Fix gitattributes for Makefile.duneEmilio Jesus Gallego Arias
2019-02-26Fix gitattributes for Makefile.duneGaëtan Gilbert
Since it matches *.dune and Makefile* the later needs to come second in the gitattributes file.
2019-02-26Merge PR #9567: [vernac] Unify declaration hooks.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-02-25[Manual] Refactor documentation of internal registration commandsVincent Laporte
2019-02-25[Manual] Document primitive integersVincent Laporte
2019-02-25[Manual] Document the “Primitive” commandVincent Laporte
2019-02-25[Manual] Document “Register Inline”Vincent Laporte
2019-02-25[Manual] Document “Register” to kernel namespaceVincent Laporte
2019-02-25Merge PR #9620: Stdlib HTML documentation: fix a few absolute URLsThéo Zimmermann
Reviewed-by: Zimmi48
2019-02-25Merge PR #9511: Enable whitespace checking for some forgotten files.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-25[Gitlab-CI] Deploy api documentation to GH-PagesVincent Laporte
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
Supersedes #8718.
2019-02-22Merge PR #9364: Apply implicit binders to Hypothesis inside sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:06:43 +0000