aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
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.
2018-05-21[ci] Add Dune to the base system.Emilio Jesus Gallego Arias
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.
2018-05-20Merge PR #7557: Add test cases from #7554Théo Zimmermann
2018-05-20Add test cases from #7554Tej Chajed
Failed in v8.7.2 but were fixed by v8.8.0.
2018-05-19Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵Michael Soegtrop
packaging scripts.
2018-05-18Merge PR #7550: [CI] Fix the script used by math-classes.Emilio Jesus Gallego Arias
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-18[CI] Fix the script used by math-classes.Pierre-Marie Pédrot
We call configure to properly regenerate the Makefile and its dependencies.
2018-05-17Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵Emilio Jesus Gallego Arias
by default.
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-17Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in ↵Pierre-Marie Pédrot
`comDefinition`.
2018-05-17Merge PR #6870: [ide] Don't set `quiet` on start.Enrico Tassi
2018-05-17Merge PR #7525: [ci] Try to build more of fiat-crypto.Gaëtan Gilbert
2018-05-17Merge PR #6808: Add unit tests to test-suiteGaëtan Gilbert
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-17[STM] Nested Proofs Allowed has to be executed immediatelyEnrico Tassi
since it affects scheduling (actually the error the option lets one silence)
2018-05-17Remove deprecation warning for nested proofs.Théo Zimmermann
It is not clear yet that support for nested proofs will actually get removed in a future version.
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-16Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.Maxime Dénès
2018-05-16Modify make system to include Makefile.common in the test suiteGaëtan Gilbert
2018-05-16[ci] Try to build more of fiat-crypto.Emilio Jesus Gallego Arias
2018-05-16Merge PR #7514: [ci] Don't build lite versions of CI developments.Gaëtan Gilbert
2018-05-16Merge PR #7535: Typo in documentation of DeriveThéo Zimmermann
2018-05-16Merge PR #7493: Minor update of the documentation about the rcfileEmilio Jesus Gallego Arias
2018-05-16Typo in documentation of DeriveJoachim Breitner
2018-05-16Merge PR #7079: Remove naked pointers from the VMMaxime Dénès
2018-05-16Merge PR #7391: Add a small documentation writer's guideMaxime Dénès
2018-05-16[windows] Don't make menhir and int anymore.Emilio Jesus Gallego Arias
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.
2018-05-16unit tests: add .merlinGaëtan Gilbert
2018-05-16add unit tests to test suitePaul Steckler
2018-05-16Merge PR #7436: [travis] Remove some more jobs from PR testing now that they ↵Gaëtan Gilbert
are on Gitlab.
2018-05-16Minor update of the documentation/man about the resource file.Hugo Herbelin
2018-05-16Merge PR #7484: Fix non-portable shebang in test-suite.Enrico Tassi
2018-05-16Merge PR #7227: [ssr] import ssreflect test suite from math-compMaxime Dénès
2018-05-16Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.Emilio Jesus Gallego Arias
2018-05-16[ci] Don't build lite versions of CI developments.Emilio Jesus Gallego Arias
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.
2018-05-16[travis] Remove some more jobs from PR testing now that they are on Gitlab.Emilio Jesus Gallego Arias
This is a "test" PR, but could be merged if we like it.
2018-05-16[ide] Don't set `quiet` on start.Emilio Jesus Gallego Arias
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.
2018-05-16Merge PR #7507: gitlab CI: fix [warnings] templateEmilio Jesus Gallego Arias
2018-05-16Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.Emilio Jesus Gallego Arias
2018-05-15Merge PR #7519: git / gpg integration linkThéo Zimmermann
2018-05-15Merge PR #7465: Don't use ref universe_opt_subst in universe normalisation ↵Pierre-Marie Pédrot
function
2018-05-15[doc] More feedback on doc writer guideClément Pit-Claudel
Co-Authored-By: @Zimmi48
2018-05-15[doc] Search for 'coqtop' in $PATH if COQBIN is unsetClément Pit-Claudel
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
Co-Authored-By: @Zimmi48
2018-05-15[doc] Clarify a comment in the READMEClément Pit-Claudel
2018-05-15[doc] Add an ELisp snippet to insert Sphinx roles and quotesClément Pit-Claudel
2018-05-15[doc] Add a README to doc/sphinx/Clément Pit-Claudel
The readme is auto-generated by combining introductory text with the docstrings in coqdomain.py.
2018-05-15[doc] Document all directives and roles of our Sphinx domainClément Pit-Claudel
Also get rid of a few unused or redundant constructs: the :ltac: role and the 'tac' directive (unused) and the :gallina: and :notation: roles (redundant).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:32:12 +0000