aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-13Merge PR #9757: [refman] Add 'warn' option to coqtop directive.Emilio Jesus Gallego Arias
Reviewed-by: cpitclaudel
2019-03-13Merge PR #9723: Fix undefined gramlib_MLLIB_DEPENDENCIES in make installEnrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9739: [dune] [configure] Fix `gramlib` path for hardcoded includes.Enrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9748: [dune] Add shim for coqtop.byteThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-03-13[refman] Fix Sphinx-translation regression in Arguments command.Théo Zimmermann
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-13Merge PR #9627: Small retroknowledge/primitive cleanupVincent Laporte
Ack-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: vbgl
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
Fix semantic conflict between #9389 and #9654.
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ↵Emilio Jesus Gallego Arias
record Reviewed-by: ejgallego
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
Ack-by: gares Ack-by: herbelin Ack-by: mattam82 Ack-by: ppedrot
2019-03-12[dune] Add shim for coqtop.byteEmilio Jesus Gallego Arias
We add a shim for running the byte version of coqtop. This fixes the Coq part of #9727 , the Dune part is still open at https://github.com/ocaml/dune/issues/108 but this PR includes a workaround. Unfortunately we have to introduce a small inefficiency in the build process as we build both byte and native versions of plugins for this work reliable. As this is a choice done during bootstrap it won't be easy to fix until we have our own `dune coqtop` command and we can control the rules depending on the final target. This should affect the `check` target so still fast builds should be possible, but if this is a problem we could add a `byteboot` target to help.
2019-03-12Merge PR #9738: [ci] [docker] Upgrade odoc to 1.4.0Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-03-11[dune] [configure] Fix `gramlib` path for hardcoded includes.Emilio Jesus Gallego Arias
The regular make build uses a non-standard header path for their files [as a way to workaround the ugliness of the non-hygienic build] This breaks in Dune as it uses the regular object file pack, so `coq_makefile` won't find it. We cherry pick a change from #8729 which fixes the updated version of bug #9735 , even tho `coq_makefile` should stop relying on hardcoded paths and use findlib instead. Closes #9735
2019-03-11[ci] [docker] Upgrade odoc to 1.4.0Emilio Jesus Gallego Arias
This is routine as for API doc writers to be able to access the newer features.
2019-03-11Fix undefined gramlib_MLLIB_DEPENDENCIES in make installGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
This operation is done directly in Safe_typing.register_inline and has nothing to do with retroknowledge afaict.
2019-03-11Merge PR #9698: Remove last random failuresGaëtan Gilbert
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego
2019-03-11Merge PR #9675: Dune: remove -short-paths flag.Emilio Jesus Gallego Arias
Ack-by: ejgallego Reviewed-by: gares
2019-03-11Merge PR #9570: Refresh contributing guide and README.Maxime Dénès
Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2019-03-10Merge PR #9654: [sphinx] Add warn option to coqtop directive.Clément Pit-Claudel
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: vbgl Reviewed-by: cpitclaudel
2019-03-10Merge PR #9728: Fix issue #9722 pkg-config not foundThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-08Fix issue #9722 pkg-config not foundMichael Soegtrop
2019-03-08Merge PR #9720: [refman] Fix typo in local application of tacticsThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-08[sphinx] Fix typo in local application of tacticshawnzug
2019-03-07Merge PR #9133: Move README-V1-V5 to credits chapterClément Pit-Claudel
Reviewed-by: cpitclaudel
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-03-05Merge PR #9524: Fix #7632: Change syntax of autoapply according to the ↵Pierre-Marie Pédrot
documentation. Reviewed-by: ppedrot
2019-03-05Merge PR #9701: [CI] Add stdlib2Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-05[CI] Add stdlib2Vincent Laporte
2019-03-05Remove regularly failing test from test-suite.Théo Zimmermann
2019-03-05Put regularly failing async tests in allow_failure mode.Théo Zimmermann
2019-03-04Merge PR #9687: Cleanup exported variables in Makefile.buildEnrico Tassi
Reviewed-by: gares
2019-03-04Merge PR #8700: Removing debugging warning when no exception handler is ↵Emilio Jesus Gallego Arias
registered in futures Ack-by: ejgallego
2019-03-04Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-04Removing debugging warning when no exception handler is registered in futures.Hugo Herbelin
As far as I understood, this was useful for tine-tuning the stm but this is no longuer needed: it is ok not to have exception handler when a constant registration does not span over several commands (such as "Goal ... Qed" or obligations).
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-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
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-03Cleanup exported variables in Makefile.buildGaëtan Gilbert
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>
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:23:24 +0000