| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-03 | Merge PR #8613: [ci] [travis] Remove CI contrib testing from Travis. | Gaëtan Gilbert | |
| 2018-10-02 | [doc] [api] Remove `ocamldoc` support in favor of `odoc` | Emilio Jesus Gallego Arias | |
| This PR removes support for `ocamldoc` in favor of `odoc`. Following a recent discussion in OCaml's discord, it turns out that basically all the ecosystem has migrated to odoc, thus we follow suit and may focus on `odoc` for Coq's ML API documentation. | |||
| 2018-10-02 | Move the compat-update-process to right after branching | Jason Gross | |
| Also test that the compat updating script hasn't become outdated on the CI. | |||
| 2018-10-02 | Update dev/doc/release-process: compat+automate | Jason Gross | |
| As requested in https://github.com/coq/coq/issues/8311#issuecomment-415976318 the release process describes the steps to take. All automatable steps are taken by the new script dev/tools/update-compat.py I've tried to make the script relatively easy to update if functions get renamed or moved, but since it's doing unstructured source manipulation, it is sort-of fragile. We could plausibly add a file to the test-suite to ensure that we catch script-breakage early, but this would require dropping compatibility support much earlier in the development cycle (the compatibility changes would have to come right when the new version is branched, rather than shortly before the beta release). | |||
| 2018-10-02 | [dune] Fix couple of minor bugs in #8617 | Emilio Jesus Gallego Arias | |
| I forgot to update `.PHONY` and to put the proper flags in the new workspace file. | |||
| 2018-10-02 | Merge PR #8625: Fix issue #8611 - Change extensions of log files in WIndows ↵ | Théo Zimmermann | |
| build to … | |||
| 2018-10-02 | [ci] overlay for elpi | Enrico Tassi | |
| 2018-10-02 | Fix issue #8611 - Change extensions of log files in WIndows build to ↵ | Michael Soegtrop | |
| _log.txt and _err.txt so that they can be viewed immediately in gitlab | |||
| 2018-10-02 | [ci] [travis] Remove CI contrib testing from Travis. | Emilio Jesus Gallego Arias | |
| This was kept as a fallback for some time, not worth keeping it anymore as our GitLab setup seems mature and reliable enough. | |||
| 2018-10-02 | [dune] Provide workspace file will all OCaml builds tested in CI. | Emilio Jesus Gallego Arias | |
| 2018-10-02 | Merge PR #8612: Fix issue 8610 - Change important CI DOS batch files to CRLF | Théo Zimmermann | |
| 2018-10-02 | [dune] [doc] Some tweaks to doc + per user flags. | Emilio Jesus Gallego Arias | |
| 2018-10-02 | Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one. | Pierre-Marie Pédrot | |
| 2018-10-02 | Document the coqpp implementation of VERNAC EXTEND. | Pierre-Marie Pédrot | |
| 2018-10-02 | Pass unnamed arguments to ML macros. | Pierre-Marie Pédrot | |
| This was imposing a bit of useless burden on the API for no good reason. | |||
| 2018-10-02 | Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0 | Pierre-Marie Pédrot | |
| 2018-10-01 | Fix issue 8610 - Change important CI DOS batch files to CRLF | Michael Soegtrop | |
| 2018-10-01 | [ci] Add plugin-tutorial to CI. | Emilio Jesus Gallego Arias | |
| This closes #7618. | |||
| 2018-10-01 | Merge PR #8579: [dune] [merlin] Fix some usability issues. | Maxime Dénès | |
| 2018-09-30 | Fix issue 8603 Move Windows CI runs to folder C:/ci | Michael Soegtrop | |
| 2018-09-30 | Typo in top_printers.ml. | Hugo Herbelin | |
| 2018-09-27 | [dune] [merlin] Fix some usability issues. | Emilio Jesus Gallego Arias | |
| As suggested on Gitter by @maximedenes we improve documentation and update Kernel's `.merlin` so it actually reports on the stricter set of warnings. We also set the language version to the proper one so users will get a better error message [the fact that we can use `(env_var ...)` with the wrong Dune version is a Dune bug indeed]. | |||
| 2018-09-27 | [ci] Allow `make ci-$contrib` when we have a build under Dune. | Emilio Jesus Gallego Arias | |
| This should allow people to test CI contribs under Dune. It should be good for now but it is still a work in progress. | |||
| 2018-09-27 | Overlays for Ltac2 and Equations. | Hugo Herbelin | |
| 2018-09-26 | [ocaml] Update required OCaml version to 4.05.0 | Emilio Jesus Gallego Arias | |
| Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml version so it makes sense we bump our dependency to 4.05.0 as we can use some newer compiler features. | |||
| 2018-09-26 | [print] Restrict use of "debug" Termops printer. | Emilio Jesus Gallego Arias | |
| The functions in `Termops.print_*` are meant to be debug printers, however, they are sometimes used in non-debug code due to a API confusion. We thus wrap such functions into an `Internal` module, improve documentation, and switch users to the right API. | |||
| 2018-09-26 | Merge PR #8534: Checking if low-level name printers are used on purpose or not | Maxime Dénès | |
| 2018-09-26 | Merge PR #8419: Remove romega in favor of lia | Théo Zimmermann | |
| 2018-09-25 | overlay to test elpi 1.1 | Enrico Tassi | |
| 2018-09-25 | elpi 1.1.0 | Enrico Tassi | |
| 2018-09-25 | Remove romega | Vincent Laporte | |
| 2018-09-25 | Merge PR #6343: [engine] Remove and deprecate `nf_enter` et al. | Pierre-Marie Pédrot | |
| 2018-09-24 | Merge PR #8520: [ci] [docker] Move to OPAM 2.0 | Gaëtan Gilbert | |
| 2018-09-24 | [engine] Remove and deprecate `nf_enter` et al. | Emilio Jesus Gallego Arias | |
| After the introduction of `EConstr`, "normalization" has become unnecessary, we thus deprecate the `nf_*` family of functions. Test-suite and CI pass after the fix for #8513. | |||
| 2018-09-24 | Merge PR #8527: dev/doc/profiling.txt: per-component flame graphs | Pierre-Marie Pédrot | |
| 2018-09-24 | [ci] [docker] Move to OPAM 2.0 | Emilio Jesus Gallego Arias | |
| The OPAM 1.2 repository has been frozen, thus we must use OPAM 2.0 if we want to get newer versions of packages / compilers. For now we must perform a manual install of OPAM as no packages for Ubuntu 18.04 exist. Note that this means nothing about the installability of Coq itself, whose OPAM repository should remain in 1.2 format for quite a long period. | |||
| 2018-09-24 | Merge PR #8519: Issue #8514 windows ci failures | Théo Zimmermann | |
| 2018-09-23 | Checking if low-level name printers are used on purpose or not. | Hugo Herbelin | |
| In particular we check if really used for internal debugging purpose or to display a message to the user. In the latter case, we replace it (when possible) by a higher-level printer (e.g. printing foo instead of Top.foo). In the former case, we clarify that the use is a debugging use. Still not perfect (see a few FIXME). | |||
| 2018-09-21 | dev/doc/profiling.txt: per-component flame graphs | Andres Erbsen | |
| 2018-09-21 | Use unique names in windows CI for cygwin and coq install folder | Michael Soegtrop | |
| Don't zip artifacts but create an artifact folder structure | |||
| 2018-09-21 | Merge commit 6a8c37c02504463afaa677641d75d9977020edf6 Windows buildfile ↵ | Michael Soegtrop | |
| cleanup and stability and logging enhancements from v8.8 | |||
| 2018-09-21 | [dune] [configure] Allow to set prefix using environment variable. | Emilio Jesus Gallego Arias | |
| This is a hack to enable correct OPAM building, the medium-term plan is to avoid having to set a prefix at configure time but instead using a set of rules to locate the Coq library. We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2 | |||
| 2018-09-20 | Update minimum required dependency versions of Sphinx doc. | Théo Zimmermann | |
| The minimum required versions of the Sphinx-related (and ANTLR) Python packages for Coq 8.10 were chosen as the lower bound between what is currently in Debian Buster and in NixOS 18.09 Jellyfish (in practice the lower bound was always met by NixOS 18.09 Jellyfish). These minimum required versions were documented. In the docker image used by GitLab CI, we install these Python packages through pip as this allows us to pin them to these specific versions. In Travis, we let them unspecified to always test the latest versions. Finally, we also add the new dependencies of the Sphinx PDF manual. | |||
| 2018-09-19 | Fix Windows builds: OPAM has changed its URL schema. | Théo Zimmermann | |
| 2018-09-19 | Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared) | Matthieu Sozeau | |
| 2018-09-19 | Merge PR #7257: Fixing yet a source of dependency on alphabetic order in ↵ | Pierre-Marie Pédrot | |
| unification. | |||
| 2018-09-17 | Merge PR #6906: [VM] Optimize structured values | Pierre-Marie Pédrot | |
| 2018-09-17 | Merge PR #8053: [dune] Add apidoc target using `odoc` | Gaëtan Gilbert | |
| 2018-09-17 | [VM] Move structured_constant to Vmvalues | Maxime Dénès | |
| 2018-09-15 | Overlay for cross-crypto. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |