aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-14Give advice on managing GitHub notifications in CONTRIBUTING.Théo Zimmermann
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
2018-05-14Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵Gaëtan Gilbert
symlink from repo
2018-05-14Remove duplicate entries for Proof, Qed, Defined, Admitted.Théo Zimmermann
And marginal improvements in the last section of the Gallina chapter.
2018-05-14gitlab CI: fix [warnings] templateGaëtan Gilbert
We never actually used the -warn-error flag...
2018-05-14Merge PR #7374: [sphinx] More fatal warnings.Maxime Dénès
2018-05-14Add GitLab CI badge in first position.Théo Zimmermann
2018-05-14Use evd_combX in Cases.Gaëtan Gilbert
2018-05-14Typing implementation doesn't use evdref.Gaëtan Gilbert
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-05-14Typing: define functional alternatives to e_* functionsGaëtan Gilbert
2018-05-14Deprecate Refiner [evar_map ref] exported functions.Gaëtan Gilbert
Uses internal to Refiner remain.
2018-05-14Pick up user overlays when running GitLab CI on PRs.Théo Zimmermann
2018-05-14Define code owners for more CI files.Théo Zimmermann
2018-05-14Update CI documentation following recent evolutions.Théo Zimmermann
2018-05-14Merge PR #7365: Mini fixes in the tactics chapterMaxime Dénès
2018-05-14[ci] [circleci] Remove jobs done in Gitlab efficiently.Emilio Jesus Gallego Arias
Following the migration to Gitlab (#6919) we reduce Circle load, see also discussion in #7436 and #7482.
2018-05-13Fixing a bug in printing the body of a located notation.Hugo Herbelin
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
2018-05-13Removing a superfluous trailing newline in "Locate" for a notation.Hugo Herbelin
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
Fixes #7065
2018-05-13Infrastructure for ocamldebug on the checkerGaëtan Gilbert
2018-05-13Merge PR #7477: Support for notations with autonomous only-parsing and ↵Emilio Jesus Gallego Arias
only-printing declarations.
2018-05-13Merge PR #7489: gitlab CI: remove math-classes jobEmilio Jesus Gallego Arias
2018-05-13Fix #4403: insufficient handling of type-in-type in kernel.Gaëtan Gilbert
2018-05-12adds a hello world tactic in tuto0Yves Bertot
2018-05-12Sphinx: a "QUICK=1" option to bypass recompilation of the library.Hugo Herbelin
2018-05-11gitlab CI: remove math-classes jobGaëtan Gilbert
It's redundant as a dependency of formal-topology.
2018-05-11Merge PR #7340: Remove DirClosedSection.Enrico Tassi
2018-05-11Doc: Renaming an old-style numerical evar in an alphabetical one.Hugo Herbelin
2018-05-11Doc: Moving `\forall` to `forall` in file tactics.rst.Hugo Herbelin
Not only are most of "forall"s in the manual in Coq notation, but the math notation leads to have a specially long space after the comma.
2018-05-11Doc: Some quotes missing in file tactics.rst.Hugo Herbelin
2018-05-11Replacing a broken reference by hyperlinks in chapter tactics.Hugo Herbelin
2018-05-11A few fixes in chapter tactics.Hugo Herbelin
2018-05-11Merge PR #7470: use at least 6 Xs in mktemp filename templatesGaëtan Gilbert
2018-05-11Updates the contents of the third tutorialYves Bertot
2018-05-11This version contains documentation for the code of the packing tacticYves Bertot
warning have been removed Examples for the use of type classes and canonical structures in automatic proof have been moved to the end.
2018-05-11Merge PR #6959: [build] Build checker generated files using a make rule.Enrico Tassi
2018-05-11Update old parts of CHANGES to use current bug numbers.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-16 04:05:12 +0000