aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gravatar Gaëtan Gilbert2018-05-22
|\
* \ Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span ↵Gravatar Gaëtan Gilbert2018-05-22
|\ \ | | | | | | | | | multiple lines
* \ \ Merge PR #6859: [stm] Make toplevels standalone executables.Gravatar Théo Zimmermann2018-05-22
|\ \ \
| | * | [ci] [gitlab] Fix printenv sorting for variables that span multiple lines.Gravatar Emilio Jesus Gallego Arias2018-05-21
| |/ / |/| |
| * | [ide] Remove special option `-ideslave`Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
| * | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
| * | [ci] Add Dune to the base system.Gravatar Emilio Jesus Gallego Arias2018-05-21
|/ / | | | | | | | | | | | | It is needed by Elpi and pidetop, and it is anyways needed for most OCaml packages, including some Coq tools in the future. The future base Docker image will include it by default.
* | Merge PR #7557: Add test cases from #7554Gravatar Théo Zimmermann2018-05-20
|\ \
| * | Add test cases from #7554Gravatar Tej Chajed2018-05-20
| | | | | | | | | | | | Failed in v8.7.2 but were fixed by v8.8.0.
* | | Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵Gravatar Michael Soegtrop2018-05-19
|\ \ \ | | | | | | | | | | | | packaging scripts.
* \ \ \ Merge PR #7550: [CI] Fix the script used by math-classes.Gravatar Emilio Jesus Gallego Arias2018-05-18
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \ \ \
| | * | | [CI] Fix the script used by math-classes.Gravatar Pierre-Marie Pédrot2018-05-18
| |/ / / |/| | | | | | | | | | | We call configure to properly regenerate the Makefile and its dependencies.
| | | * [circle] Use Docker image from Gitlab registry.Gravatar Emilio Jesus Gallego Arias2018-05-17
| |_|/ |/| |
* | | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵Gravatar Emilio Jesus Gallego Arias2018-05-17
|\ \ \ | | | | | | | | | | | | by default.
* \ \ \ Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\ \ \ \
* \ \ \ \ Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in ↵Gravatar Pierre-Marie Pédrot2018-05-17
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | `comDefinition`.
* \ \ \ \ \ Merge PR #6870: [ide] Don't set `quiet` on start.Gravatar Enrico Tassi2018-05-17
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7525: [ci] Try to build more of fiat-crypto.Gravatar Gaëtan Gilbert2018-05-17
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6808: Add unit tests to test-suiteGravatar Gaëtan Gilbert2018-05-17
|\ \ \ \ \ \ \ \
| | | | | | * | | Document nested proofs and associated option.Gravatar Théo Zimmermann2018-05-17
| | | | | | | | |
| | | | | | * | | [STM] Nested Proofs Allowed has to be executed immediatelyGravatar Enrico Tassi2018-05-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | since it affects scheduling (actually the error the option lets one silence)
| | | | | | * | | Remove deprecation warning for nested proofs.Gravatar Théo Zimmermann2018-05-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not clear yet that support for nested proofs will actually get removed in a future version.
| | | | | | * | | Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
| |_|_|_|_|/ / / |/| | | | | | |
* | | | | | | | Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.Gravatar Maxime Dénès2018-05-16
|\ \ \ \ \ \ \ \
| | * | | | | | | Modify make system to include Makefile.common in the test suiteGravatar Gaëtan Gilbert2018-05-16
| | | | | | | | |
| | | * | | | | | [ci] Try to build more of fiat-crypto.Gravatar Emilio Jesus Gallego Arias2018-05-16
| |_|/ / / / / / |/| | | | | | |
* | | | | | | | Merge PR #7514: [ci] Don't build lite versions of CI developments.Gravatar Gaëtan Gilbert2018-05-16
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7535: Typo in documentation of DeriveGravatar Théo Zimmermann2018-05-16
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7493: Minor update of the documentation about the rcfileGravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | Typo in documentation of DeriveGravatar Joachim Breitner2018-05-16
| |/ / / / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7079: Remove naked pointers from the VMGravatar Maxime Dénès2018-05-16
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7391: Add a small documentation writer's guideGravatar Maxime Dénès2018-05-16
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * [windows] Don't make menhir and int anymore.Gravatar Emilio Jesus Gallego Arias2018-05-16
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As pointed out by @MSoegtropIMC [here](https://github.com/coq/coq/pull/7522#issuecomment-389478963) there are not needed to build the packages, so not building them will save a couple of minutes.
| | | | | | * | | | | unit tests: add .merlinGravatar Gaëtan Gilbert2018-05-16
| | | | | | | | | | |
| | | | | | * | | | | add unit tests to test suiteGravatar Paul Steckler2018-05-16
| |_|_|_|_|/ / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7436: [travis] Remove some more jobs from PR testing now that they ↵Gravatar Gaëtan Gilbert2018-05-16
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | are on Gitlab.
| | | | * | | | | | | Minor update of the documentation/man about the resource file.Gravatar Hugo Herbelin2018-05-16
| | | | | | | | | | |
* | | | | | | | | | | Merge PR #7484: Fix non-portable shebang in test-suite.Gravatar Enrico Tassi2018-05-16
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7227: [ssr] import ssreflect test suite from math-compGravatar Maxime Dénès2018-05-16
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.Gravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | | [ci] Don't build lite versions of CI developments.Gravatar Emilio Jesus Gallego Arias2018-05-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the original Travis CI setup, the per-job time limit was an issue. However, Gitlab has much improved this problem due to a) Coq not being built for each contrib, b) user-configurable time limit. We thus disable the expensive builds from Travis: `fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`, `math-comp`, `unimath`, `vst` and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`] in full. We also update the `math-comp` script as the `odd-order` theorem lives in a separate repository and it is a key CI case.
| | | | * | | | | | | | | | [travis] Remove some more jobs from PR testing now that they are on Gitlab.Gravatar Emilio Jesus Gallego Arias2018-05-16
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a "test" PR, but could be merged if we like it.
| | | | | | | | | * | | | [ide] Don't set `quiet` on start.Gravatar Emilio Jesus Gallego Arias2018-05-16
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes `coqidetop` behavior consistent with the one of `coqtop`. This was likely needed in the past when Coq used to print all kind of stuff to stdout, including goal display. Now, it is not the case anymore and this flag mainly controls printing verbosity.
* | | | | | | | | | | | Merge PR #7507: gitlab CI: fix [warnings] templateGravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.Gravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7519: git / gpg integration linkGravatar Théo Zimmermann2018-05-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7465: Don't use ref universe_opt_subst in universe normalisation ↵Gravatar Pierre-Marie Pédrot2018-05-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | function
| | | | | | | | * | | | | | | | [doc] More feedback on doc writer guideGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Co-Authored-By: @Zimmi48
| | | | | | | | * | | | | | | | [doc] Search for 'coqtop' in $PATH if COQBIN is unsetGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | | | | | | | | |