aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too.
2018-12-14Merge PR #9147: [dune] [doc] Support for building the reference manual with ↵Théo Zimmermann
Dune.
2018-12-14Update pinned nixpkgs to use Dune 1.6.Théo Zimmermann
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost ↵Gaëtan Gilbert
of evars in shelf)
2018-12-13Merge PR #9194: Fixing uses of sed in #8985 which do not work on MacOS XMatthieu Sozeau
2018-12-13Fixing uses of sed which do not work on MacOS X.Hugo Herbelin
This was introduced in PR #8985.
2018-12-13Merge PR #9117: Accept argument names for extra arguments with "extra scopes"Matthieu Sozeau
2018-12-13Merge PR #9210: Fix issue #9176 : Windows: change cygwin repoThéo Zimmermann
2018-12-13Merge PR #9211: Fixing incorrect mention of coercions as being part of the ↵Théo Zimmermann
interning phase
2018-12-13[dune] [doc] Support for building the reference manual with Dune.Emilio Jesus Gallego Arias
This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted.
2018-12-13Merge PR #9032: checker: check inductive types by roundtrip through the kernel.Pierre-Marie Pédrot
2018-12-13Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as ↵Pierre-Marie Pédrot
pattern variables
2018-12-13Merge PR #9169: [rtauto] [auto] Use new proof engine.Pierre-Marie Pédrot
2018-12-13Merge PR #9217: [ci] [appveyor] Temporally disable test suite on Appveyor.Gaëtan Gilbert
2018-12-13Merge PR #9196: Document the deprecation of hint declaration withou database ↵Maxime Dénès
in refman.
2018-12-13Merge PR #8096: Higher-level libobject API for objects with fixed scopesEnrico Tassi
2018-12-13[ci] [appveyor] Temporally disable test suite on Appveyor.Emilio Jesus Gallego Arias
Hopefully we will re-enable it back soon, I am preparing a refactoring that should make it more robust w.r.t paths and changes on Windows which will enable to use a faster build system. But now it is timing out 100% of the times [due to #8655] so it is not useful.
2018-12-12Merge PR #9101: Fix 8922 againHugo Herbelin
2018-12-12Merge PR #9087: Add CI job building stdlib with `async-proofs on`Emilio Jesus Gallego Arias
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-12Accept argument names for extra arguments with "extra scopes"Maxime Dénès
The checks were unnecessarily restrictive (since names can be used for documentation purposes), and the error message was a bit wrong (it mentioned a restriction on the explicit status of arguments).
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Fix issue #9176 : Windows: change cygwin repoMichael Soegtrop
2018-12-12Fixing incorrect mention of coercions as being part of the interning phase.Hugo Herbelin
2018-12-12[rtauto] [auto] Use new proof engine.Emilio Jesus Gallego Arias
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-12Fixes #9166 (no warning on pattern variables named like a deprecated alias).Hugo Herbelin
2018-12-12Avoid Fixpoint without struct nor body in stdlibMaxime Dénès
As reported in #9060, the STM does not handle such constructions properly. They are anyway fragile, for example Guarded reports a failure if run at the end of the scripts, so this patch is an improvement.
2018-12-12Add CI job building stdlib with `-async-proofs on`Maxime Dénès
2018-12-12User flags for coqtop/coqc in Makefile and CI build templateMaxime Dénès
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix ↵Maxime Dénès
comments.
2018-12-11Add missing formatting.Théo Zimmermann
2018-12-11Merge PR #9197: Fixing imports in debug printers: gramlib depends on Loc ↵Emilio Jesus Gallego Arias
which is in lib.cma
2018-12-11Merge PR #8655: Test suite: use coqc and then coqchkEnrico Tassi
2018-12-11Merge PR #9155: Fix race condition triggered by fresh universe generationEnrico Tassi
2018-12-11Fixing imports in debug printers: gramlib depends on Loc which is in lib.cma.Hugo Herbelin
2018-12-11Document the deprecation of hint declaration withou database in refman.Théo Zimmermann
Follow-up of #8987.
2018-12-11Tests for #4509, #6202 which happen to be fixed (was a lost of evars in shelf).Hugo Herbelin
2018-12-11Merge PR #9151: [dune] Teach coq_dune about `.glob` and `.aux` files.Théo Zimmermann
2018-12-10Fix Invalid_argument in List.iter2Jim Fehrle
2018-12-10For diffs, return exactly the characters that make up STRING and FIELD tokensJim Fehrle
2018-12-10Fix #9091: don't show deleted compacted hypotheses twice in diffJim Fehrle
2018-12-10Treat unmatched goals as new for diffs (highlighted)Jim Fehrle
Improve debug output
2018-12-10[test-suite] Fail when the checker failsVincent Laporte
2018-12-10[test-suite] Run `coqchk` on most test casesVincent Laporte
2018-12-10[dune] Teach coq_dune about `.glob` and `.aux` files.Emilio Jesus Gallego Arias
This is a required step in order to be able to call `coqdoc` an generate the documentation of the stdlib, and also useful for other uses such as the asynchronous engine.
2018-12-10Merge PR #9145: Do so that an error message follows the "Error:" header on ↵Emilio Jesus Gallego Arias
the same line
2018-12-10Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.packEmilio Jesus Gallego Arias
2018-12-10Merge PR #9177: add relation-algebra to CI test suiteGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:46:30 +0000