aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-12-19Better error reporting when res is not what is expectedJason Gross
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
2019-12-19Fix complexity test-suite failure reporting on WinJason Gross
Apparently `expr 1 \+ 1` is fine on Linux but not cygwin/Windows, where it fails with "syntax error". Similarly for `-` and `/`.
2019-12-19Revert "Fix #11303: skip complexity tests on windows even if bogomips found"Jason Gross
This reverts commit ec505a2fa67b0776b624be54417e06c6512f1734. A better fix is coming
2019-12-19Fix #11303: skip complexity tests on windows even if bogomips foundGaëtan Gilbert
Apparently the bogomips produced by cygwin are extra-bogo.
2019-12-18Merge PR #6090: Implement open recursion in the pretyperEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: gares
2019-12-18Merge PR #9786: Fix Equation's ci scriptPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ↵Pierre-Marie Pédrot
~strict flag Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-18Merge PR #11267: FIND_SKIP_DIRS (make): ignore all dot directoriesEnrico Tassi
Reviewed-by: gares
2019-12-18Merge PR #11123: Fix signal polling for OCaml 4.10Maxime Dénès
Ack-by: ejgallego
2019-12-18Merge PR #11263: [micromega] fix efficiency regressionMaxime Dénès
Reviewed-by: maximedenes
2019-12-17Type pretyping is part of the open recursionPierre-Marie Pédrot
2019-12-17Exporting the open-recursion style API.Pierre-Marie Pédrot
2019-12-17Implementing open recursion in the pretyper.Pierre-Marie Pédrot
For now, the API is unchanged and this commit only splits pretyping code for each glob_constr constructor into a record field.
2019-12-17failwith -> caml_failwithGuillaume Munch-Maccagnoni
2019-12-17Fatal error in VM if SIGINT was seen but no exception occured.Guillaume Munch-Maccagnoni
2019-12-17Fix signal polling for OCaml 4.10Guillaume Munch-Maccagnoni
Issue #10603
2019-12-17Merge PR #11299: [VM] fix volatile declarationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-17[VM] fix volatile declarationGuillaume Munch-Maccagnoni
2019-12-17Merge PR #10762: Fix refine and eapply to mark shelved goals as ↵Maxime Dénès
non-resolvable, always Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
PR #9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes #11063 and fixes #11242 and fixes #11270
2019-12-17Merge PR #11294: Advertise doc for master branch in README.Maxime Dénès
Reviewed-by: maximedenes
2019-12-16FIND_SKIP_DIRS (make): ignore all dot directoriesGaëtan Gilbert
Fix #11266
2019-12-16Merge PR #11291: Being explicit on existence of a remote link in stdlib to ↵Théo Zimmermann
avoid possible "breach of privacy" Reviewed-by: Zimmi48
2019-12-16Overlay for #11027Gaëtan Gilbert
2019-12-16Advertise doc for master branch in README.Théo Zimmermann
2019-12-16Don't pass (ignored) implicits to interp_mutual_inductive_constrGaëtan Gilbert
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
It gets thrown away if the inductive is declared in a section anyway, and there is no user syntax to specify it.
2019-12-16reduce arguments of template_polymorphism_candidateGaëtan Gilbert
take only the template_check flag instead of the whole env
2019-12-16comInductive: remove redundant check_evars callsGaëtan Gilbert
We do [solve_remaining_evars all_and_fail_flags] immediately before calling [interp_mutual_inductive_constr] so these checks are extra.
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
There are no users in Coq but maybe some plugin wants it so don't completely remove it
2019-12-16Merge PR #10695: [ci] [dune] Updates to dune builds artifacts.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2019-12-16[make] Add _build_boot to find_skip_dirsEmilio Jesus Gallego Arias
2019-12-16[dune] Use a special directory for the boot buildEmilio Jesus Gallego Arias
This is related to and fixes #10694 in part. When calling bootstrap in an incremental build step, we must be sure the generated dune files are in place. In the CI, these won't be in place, so we must bootstrap without altering the digest and trace database coming from the artifact. Using a separate boot step to recreate the missing `dune` files works fine and takes just a few seconds.
2019-12-16[ci] [dune] Updates to dune builds artifacts.Emilio Jesus Gallego Arias
Closes #10694 We modify handling of artifacts for dune builds: - we preserve `_build/log` log as artifact for ci-builds, - we use a tar.gz as to preserve file permissions which is necessary in order to reuse the artifacts in an incremental build. Dune uses this rule to digest a file: ``` Digest.generic (file_contents f, f.stats.st_perm land 0o100 (* Only take USR_X in account *)) ``` Since a few releases, Gitlab CI uses `.zip` as the storage format for artifacts, this means that files in `_build` will get the executable bit set when they did not have it originally, making all the digest cache to miss. This caused #10694 . See https://gitlab.com/gitlab-org/gitlab/issues/18711
2019-12-14Make prodn look more like productionlistJim Fehrle
2019-12-14Being explicit on existence of a remote link.Hugo Herbelin
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
Check that we don't regress on PR #10762 example Fix regression discovered by Arthur in PR #10762 Fix script of #10298 which was relying on breaking semantics for `eapply` Add doc Add comment in clenvtac Actually, always mark shelved goals as unresolvable Update doc to reflect semantics w.r.t. shelved subgoals
2019-12-14Merge PR #11251: [micromega] reformating using ocamlformatMaxime Dénès
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2019-12-13[micromega] Enable ocamlformat.Emilio Jesus Gallego Arias
2019-12-13Merge PR #11259: [make] Rename Makefile to Makefile.make and INSTALL to ↵Théo Zimmermann
INSTALL.md Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: jfehrle
2019-12-13Merge PR #11257: [dev] [ocaml] Add ocamlformat configuration.Théo Zimmermann
Reviewed-by: Zimmi48
2019-12-13Add ocamlformat dependency to Nix fileMaxime Dénès
2019-12-13Merge PR #11283: Split up stdlib install command (too long)Maxime Dénès
Reviewed-by: maximedenes
2019-12-13[build] Allow the selection of build system using an env var.Emilio Jesus Gallego Arias
This is undocumented on purpose by now. Suggested by Gaëtan Gilbert
2019-12-13[doc] [INSTALL] split make-based install instructions to its own file.Emilio Jesus Gallego Arias
2019-12-13[doc] [INSTALL] Port INSTALL to markdown format.Emilio Jesus Gallego Arias
2019-12-13[make] Rename Makefile to Makefile.makeEmilio Jesus Gallego Arias
Picked from #8729. This should help preserve the history better when we split.
2019-12-13[fmt] [dune] Add ocamlformat configuration.Emilio Jesus Gallego Arias
For now we don't enable it in any source file, neither on dune files. `lint-repository` has been updated so it will check `dune build @fmt` returns 0.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 19:45:14 +0000