aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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).
2018-05-15[doc] Small fixesClément Pit-Claudel
2018-05-15[doc] Compute the path to coqdoc at run time, not at load timeClément Pit-Claudel
2018-05-15Update MERGING.mdMatthieu Sozeau
Simpler
2018-05-15Update MERGING.mdMatthieu Sozeau
Actually there are more general instructions
2018-05-15git / gpg integration linkMatthieu Sozeau
2018-05-15Merge PR #7213: Do not compute constr matching context if not used.Matthieu Sozeau
2018-05-15[sphinx] Fix indentation at the end of proof handling chapter.Théo Zimmermann
2018-05-15Merge PR #7487: Remove duplicate entries for Proof, Qed, Defined, Admitted.Maxime Dénès
2018-05-15Merge PR #7503: [ci] [circleci] Remove jobs done in Gitlab efficiently.Gaëtan Gilbert
2018-05-15[ssr] import ssreflect test suite from math-compEnrico Tassi
2018-05-15Merge PR #7224: Attempt to fix the doubly encapsulated Ltac errors in coqideEnrico Tassi
2018-05-14Merge PR #7190: Option for quick compilation of the reference manual, ↵Maxime Dénès
bypassing dependencies
2018-05-14Merge PR #7506: Add GitLab CI badge in first position.Maxime Dénès
2018-05-14Merge PR #7504: Define code owners for more CI files.Maxime Dénès
2018-05-14Merge PR #7170: Script to identify the code owner for given filesMaxime Dénès
2018-05-14Update CI README with info about gitlab windows and docker jobs.Gaëtan Gilbert
2018-05-14Gitlab: skip docker job when $SKIP_DOCKER == "true".Gaëtan Gilbert
2018-05-14Gitlab: build docker image in pipeline and use through registry.Gaëtan Gilbert
A docker-boot job is added which builds the docker image and pushes it to the registry, the other jobs running on the image from the registry. The boot job reuses the already pushed image if it exists and matches, this is important to cut down its runtime. Making a new image takes 30min for all the switches https://gitlab.com/SkySkimmer/coq/-/jobs/66650546 For testing I removed all jobs except boot and main build, and after that run I built only the standard switch. Building 1 switch takes around 20min https://gitlab.com/SkySkimmer/coq/-/jobs/66656942 When the registry is up to date it takes 2min https://gitlab.com/SkySkimmer/coq/-/jobs/66658790 (I don't know about all switches but probably no more than 5min) Each pipeline pushes the image to $CI_REGISTRY_IMAGE:$CI_PIPELINE_ID which is eg registry.gitlab.com/skyskimmer/coq:21557176 and is what the other jobs use to run themselves. For caching it pulls from and pushes to a constant name, in this test $CI_REGISTRY_IMAGE:$CACHEKEY. We might also want to pull from the main coq repo to avoid redoing work. The question of having 1 image or 1 image/switch remains open. Using the gitlab registry doesn't really work for circle CI, so the dockerhub account would have to remain (or circle could return to an opam-boot job, or be removed from our CI). There are similar concerns with travis if we want to move it to docker.
2018-05-14Merge PR #7337: dir-locals: add bug-reference-mode variablesEmilio Jesus Gallego Arias
2018-05-14Merge PR #7482: Update CI documentation following recent evolutions.Emilio Jesus Gallego Arias
2018-05-14Merge PR #7502: Fixing little printing bug with "Locate" on recursive notationsEmilio Jesus Gallego Arias
2018-05-14Merge PR #7344: Windows packaging build with Gitlab CIGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:06:21 +0000