aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-02[ci] [fiat-crypto] Use the pinned bedrock2Jason Gross
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2, only with the pinned version, and bedrock2 is still relatively unstable. So we make the CI not have Fiat-Crypto depend on bedrock2, and instead use the pinned submodule, by using `EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
2020-02-02Merge PR #11500: [ci] [fiat-crypto-legacy] Use new, faster targetsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-02Merge PR #11484: Fix 11483 (Performance bug of PrimFLoat.compare with ↵Pierre-Marie Pédrot
native_compute) Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-02Merge PR #11326: Refactoring part of #11120 about printing applied global ↵Emilio Jesus Gallego Arias
references Reviewed-by: ejgallego
2020-02-02Merge PR #11466: checkdeps.py: add missing dep & report deps all at onceThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-31[ci] [fiat-crypto-legacy] Use new, faster targetsJason Gross
The computation of which files to build is now mostly cached rather than computed, eliminting basically all of the wait-time from `make` to the first invocation of `coqc`. Note that we no longer need to invoke `./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds up `coqdep` somewhat significantly. Fixes #9298
2020-01-30Constrextern.ml: Move a function earlier to be usable for pattern printing.Hugo Herbelin
2020-01-30Minor indentation change.Hugo Herbelin
2020-01-30Refactoring code for matching partial applications against notations.Hugo Herbelin
Should be semantically equivalent.
2020-01-30Refactoring code for externing applications.Hugo Herbelin
Should be semantically equivalent.
2020-01-30Printing tests for applied references combined with impl. args. and notations.Hugo Herbelin
This shows a few bugs and even anomalies. See issue #11091. See further commits for some fixes.
2020-01-30Constrextern.ml: for readability, use auxiliary function for externing records.Hugo Herbelin
2020-01-30Merge PR #11377: coqtop: stop on Sys_blocked_ioEmilio Jesus Gallego Arias
Ack-by: JasonGross Reviewed-by: ejgallego Ack-by: gares
2020-01-30coqtop: stop on Sys_blocked_ioGaëtan Gilbert
Close #10918
2020-01-30Fix 11483Pierre Roux
Performance bug of PrimFLoat.compare with native_compute When adapting Coq.Interval with @erikmd and @silene, we noticed that PrimFLoat.compare is taking a lot of time with native_compute (much more than with vm_compute). This comes from the implementation using the OCaml polymorphic comparison instead of the float comparison.
2020-01-30Merge PR #11464: Fix off-by-one in docs of `first num last` (fix #11463)Enrico Tassi
Reviewed-by: gares
2020-01-30Merge PR #11418: Add some more info to the maintainer doc.Maxime Dénès
Reviewed-by: maximedenes
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
Reviewed-by: maximedenes
2020-01-30Merge PR #11480: Remove unused CEphemeron.iter_opt, cleanup commentsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-30Merge PR #11409: [rfc] [mltop] Removal of dynamic loading of object and ↵Pierre-Marie Pédrot
`.ml` files Ack-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2020-01-30Remove unused CEphemeron.iter_opt, cleanup commentsGaëtan Gilbert
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
This seems seldom used and I think in general instrumentation this way is pretty limited (usually better to use the build system to tweak) It thus seems worth removing as to simplify `Mltop` a bit, but of course comments are welcome.
2020-01-29Merge PR #11399: Checker: use inductive's check_template flagPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-29Merge PR #11408: [mltop] Remove error handling hacks in favor of default ↵Pierre-Marie Pédrot
methods. Reviewed-by: ppedrot
2020-01-29Merge PR #11455: Small API additions to kernel/univPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-29Merge PR #11472: Fix #11467 ('e' was not displayed when printing decimal ↵Pierre-Marie Pédrot
notations in R) Reviewed-by: erikmd Reviewed-by: ppedrot
2020-01-29Merge PR #11473: Remove dead code in Globnames.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-29Merge PR #11469: Add reduction-effects to the CIGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-28Add reduction-effects to the CIJason Gross
2020-01-28Fix #11467Pierre Roux
'e' was not displayed when printing decimal notations in R : Require Import Reals. Check (1.23e1, 32e+1, 0.1)%R. was giving < (123-1%R, 321%R, 1-1%R) instead of < (123e-1%R, 32e1%R, 1e-1%R) This was introduced in #8764 (in Coq 8.10).
2020-01-28Merge PR #11376: Fix fold order in CArray.fold_right(2)_mapPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
2020-01-28Merge PR #11379: [ocaml] Remove Custom Backtrace module in favor of OCaml'sPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Merge PR #11419: schemes: use rigid universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Merge PR #11459: cleanup: Lib.freeze doesn't use its [~marshallable] argumentMaxime Dénès
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes
2020-01-27Rephrase to reduce ambiguityPaolo G. Giarrusso
This is the smallest possible change to clarify the text without making it even more formal.
2020-01-27Fix off-by-one in docs of `first num last` (fix #11463)Paolo G. Giarrusso
2020-01-27checkdeps.py: report *all* missing dependencies at oncePaolo G. Giarrusso
Otherwise you need a few feedback loops to install all dependencies.
2020-01-27checkdeps: check for sphinxcontrib-bibtexPaolo G. Giarrusso
I lacked this package, and got: ``` $ make -j2 COQ_USE_DUNE=1 refman-html [...] env doc/sphinx_build (exit 2) (cd _build/default/doc && /usr/bin/env COQLIB=.. sphinx-build -j4 -W -b html -d sphinx_build/doctrees sphinx sphinx_build/html) Running Sphinx v2.1.2 Extension error: Could not import extension sphinxcontrib.bibtex (exception: No module named 'sphinxcontrib.bibtex') make: *** [refman-html] Error 1 ```
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2020-01-27Checker: use inductive's check_template flagGaëtan Gilbert
And enable related test.
2020-01-27Merge PR #11415: Remove the CoqIDE "Revert all Buffers" command.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-01-27schemes: use rigid universesGaëtan Gilbert
so for instance ~~~coq Set Printing All. Set Printing Universes. Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . Lemma bla@{u v|u < v} : foo@{u v} -> False. Proof. induction 1. Qed. ~~~ works.
2020-01-27Fix fold order in CArray.fold_right(2)_mapGaëtan Gilbert
These functions are unused in Coq itself but this may break some plugins. Close #10987
2020-01-27Small API additions to kernel/univGaëtan Gilbert
- allow viewing the internal representation of uglobal and universe (with universe, this replaces the "map" function. I kept exists and for_all as they felt somewhat convenient) - add universe set and map modules (currently unused but they're natural)
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: maximedenes
2020-01-23Merge PR #11446: Changed Gitlab CI runner tag for Windows to windows-inriaEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-01-23Changed Gitlab CI runner tag for Windows to windows-inriaMichael Soegtrop
2020-01-23Merge PR #11444: Minor tweaks to the 8.11 changelog.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2020-01-23Merge PR #11445: Clear patches folder before each windows build runThéo Zimmermann
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:03:29 +0000