aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-01Merge PR #12431: [ci] Split fiat-crypto into non-OCaml and OCamlGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-31[ci] Split fiat-crypto into non-OCaml and OCamlJason Gross
Note that this should reduce the overall build time of fiat-crypto related targets by about 10--20 minutes, as I've removed the heaviest jobs (about 25--30 minutes in serial) from the OCaml target. I'd like to keep the OCaml target around just to make sure that Coq doesn't introduce a change to extraction that breaks compilation of extracted OCaml code. See https://github.com/ocaml/ocaml/issues/7826 for the issue tracking performance of compiling the extracted OCaml code (and perhaps there should be another issue opened on the OCaml bug tracker about flambda on the fiat-crypto extracted files?) Alternative to #12405 Closes #12405 Fixes #12400
2020-05-29Merge PR #12393: [declare] Miscellaneous nits from my main dev treeGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-29Merge PR #12421: Fixes for compilation without native dynlinkEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-28Fixing compilation with -natdynlink no.Hugo Herbelin
This complements #11407 about storing digests of modules.
2020-05-27Merge PR #12389: Small coq_makefile improvement.Enrico Tassi
Reviewed-by: gares
2020-05-27Adding changelog.Martin Bodin
2020-05-27Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters ↵Martin Bodin
section.
2020-05-27Merge PR #12408: Fix output tests for location errors when running in async ↵Emilio Jesus Gallego Arias
mode. Reviewed-by: JasonGross Reviewed-by: ejgallego
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
A step towards enforcing some more static invariants.
2020-05-26[declare] Factor common universe computation in close proof.Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_deferred in close_proofEmilio Jesus Gallego Arias
A step towards enforcing some more static invariants.
2020-05-26[declare] Factor out universe computation in close_proofEmilio Jesus Gallego Arias
A step towards enforcing some more static invariants.
2020-05-26[declare] Nit on errors.Emilio Jesus Gallego Arias
2020-05-26[declare] Turn restrict_ucontext hack into an internal parameterEmilio Jesus Gallego Arias
This is not needed outside of `Declare` now.
2020-05-26[nit] Remove unused exported error message in obligationsEmilio Jesus Gallego Arias
2020-05-26[declare] Don't expose internal parameter oblsEmilio Jesus Gallego Arias
2020-05-26[declare] Simplify exported type of definition_entryEmilio Jesus Gallego Arias
This reduces the amount of exported internals, in particular w.r.t. proof delaying and side effects which we will need in future refactorings. Actually turning the type from `Evd.side_effects proof_entry` to `unit proof_entry` is left for the next commits.
2020-05-26Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugsGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-25dev/tools/make-changelog.sh now asks about fixed bugsJason Gross
Fixes #12386
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
In this mode, an additional error was emitted, which made the test fail: Error: There are pending proofs: Unnamed_thm.
2020-05-25Merge PR #12403: Fix hyperlinks in changes.rstThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-25Add a changelog.Pierre-Marie Pédrot
2020-05-25Remove the prolog tactic.Pierre-Marie Pédrot
It was deprecated in 8.12 and not used in the wild.
2020-05-24Fix hyperlinks in changes.rstMatthew Dempsky
2020-05-24Merge PR #12392: [backport-pr] Select correct remote of the master branch.Jason Gross
Reviewed-by: JasonGross
2020-05-24Merge PR #12379: Omit voluminous Latex warningsThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-23[dev/tools] Fix #12314: do not die silently if branch has no remote.Théo Zimmermann
2020-05-22[backport-pr] Select correct remote of the master branch.Théo Zimmermann
2020-05-22Merge PR #12076: [coqchk] Fix #5030 (coqchk reports names from opaque ↵Pierre-Marie Pédrot
modules as axioms) Reviewed-by: herbelin Reviewed-by: ppedrot
2020-05-22[coqchk] Improve previous heuristic.Pierre Roux
Instead of considering all constants without body in the environment, consider only the ones appearing in the body of the opacified constant.
2020-05-22[coqchk] Add testPierre Roux
2020-05-22[coqchk] Fix #5030Pierre Roux
When encountering ```Coq Module M : T. ... Lemma c :... ... Qed. ... End M. ``` every field `c` without body in `T` but with a body in `M` is registered as opacified in a table along with all constants `opacified(c)` without body in the environment at this point (i.e., all axioms potentially used by c). Then, when printing axioms, if `c` appears in the final environment it is replaced by `opacified(c)` in the resulting list of axioms.
2020-05-22[coqchk] Change list to setPierre Roux
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with ↵Pierre-Marie Pédrot
eta-expansion of "match" branches Reviewed-by: gares Ack-by: ppedrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-21Fix an uncaught python exception in timingJason Gross
Previously, when either the 'before' or 'after' had no files, we'd get an uncaught exception: ``` Traceback (most recent call last): File "/home/jgross/Documents/repos/coq/tools/make-both-time-files.py", line 16, in <module> table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem) File "/home/jgross/Documents/repos/coq/tools/TimeFileMaker.py", line 391, in make_diff_table_string right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values()) ValueError: max() arg is an empty sequence ``` Fixes #12387
2020-05-21Merge PR #12371: [obligations] Minor refactoringGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-21Merge PR #12368: Print a newline at the end of timing tablesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-21Merge PR #12364: [ci] [docker] Bump ocamlformat and duneGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: vbgl
2020-05-21Merge PR #12358: [topfmt] Set formatter + flush fixGaëtan Gilbert
Reviewed-by: JasonGross Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-21Merge PR #12316: Use pagination in fetching the number of reviewsGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-20Print a newline at the end of timing tablesJason Gross
This, for example, improves the CI display, so that `$ echo 'end:coq.test'` does not appear on the same line as the end of the timing table.
2020-05-20[merge-pr] Use a simpler method to get all pagesJason Gross
h/t SkySkimmer at https://github.com/coq/coq/pull/12316#issuecomment-630952659
2020-05-20[merge-pr.sh] Follow next links insteadJason Gross
As per PR review request
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 19:10:40 +0000