coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge 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-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7487: Remove duplicate entries for Proof, Qed, Defined, Admitted.	Maxime Dénès	2018-05-15
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7503: [ci] [circleci] Remove jobs done in Gitlab efficiently.	Gaëtan Gilbert	2018-05-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \|	[ssr] import ssreflect test suite from math-comp	Enrico Tassi	2018-05-15
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7224: Attempt to fix the doubly encapsulated Ltac errors in coqide	Enrico Tassi	2018-05-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7190: Option for quick compilation of the reference manual, ↵	Maxime Dénès	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	bypassing dependencies
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7506: Add GitLab CI badge in first position.	Maxime Dénès	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7504: Define code owners for more CI files.	Maxime Dénès	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7170: Script to identify the code owner for given files	Maxime Dénès	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Update CI README with info about gitlab windows and docker jobs.	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Gitlab: skip docker job when $SKIP_DOCKER == "true".	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Gitlab: build docker image in pipeline and use through registry.	Gaëtan Gilbert	2018-05-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7337: dir-locals: add bug-reference-mode variables	Emilio Jesus Gallego Arias	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7482: Update CI documentation following recent evolutions.	Emilio Jesus Gallego Arias	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7502: Fixing little printing bug with "Locate" on recursive notations	Emilio Jesus Gallego Arias	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7344: Windows packaging build with Gitlab CI	Gaëtan Gilbert	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵	Gaëtan Gilbert	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	symlink from repo
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Remove duplicate entries for Proof, Qed, Defined, Admitted.	Théo Zimmermann	2018-05-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	And marginal improvements in the last section of the Gallina chapter.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	gitlab CI: fix [warnings] template	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We never actually used the -warn-error flag...
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7374: [sphinx] More fatal warnings.	Maxime Dénès	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Add GitLab CI badge in first position.	Théo Zimmermann	2018-05-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Use evd_combX in Cases.	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Typing implementation doesn't use evdref.	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Typing: define functional alternatives to e_* functions	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Deprecate Refiner [evar_map ref] exported functions.	Gaëtan Gilbert	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Uses internal to Refiner remain.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Pick up user overlays when running GitLab CI on PRs.	Théo Zimmermann	2018-05-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Define code owners for more CI files.	Théo Zimmermann	2018-05-14
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Update CI documentation following recent evolutions.	Théo Zimmermann	2018-05-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7365: Mini fixes in the tactics chapter	Maxime Dénès	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[ci] [circleci] Remove jobs done in Gitlab efficiently.	Emilio Jesus Gallego Arias	2018-05-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Following the migration to Gitlab (#6919) we reduce Circle load, see also discussion in #7436 and #7482.
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Fixing a bug in printing the body of a located notation.	Hugo Herbelin	2018-05-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Removing a superfluous trailing newline in "Locate" for a notation.	Hugo Herbelin	2018-05-13
\| \|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo	Ralf Jung	2018-05-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7065
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7477: Support for notations with autonomous only-parsing and ↵	Emilio Jesus Gallego Arias	2018-05-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	only-printing declarations.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7489: gitlab CI: remove math-classes job	Emilio Jesus Gallego Arias	2018-05-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Sphinx: a "QUICK=1" option to bypass recompilation of the library.	Hugo Herbelin	2018-05-12
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gitlab CI: remove math-classes job	Gaëtan Gilbert	2018-05-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It's redundant as a dependency of formal-topology.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7340: Remove DirClosedSection.	Enrico Tassi	2018-05-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Doc: Renaming an old-style numerical evar in an alphabetical one.	Hugo Herbelin	2018-05-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Doc: Moving `\forall` to `forall` in file tactics.rst.	Hugo Herbelin	2018-05-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Doc: Some quotes missing in file tactics.rst.	Hugo Herbelin	2018-05-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Replacing a broken reference by hyperlinks in chapter tactics.	Hugo Herbelin	2018-05-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	A few fixes in chapter tactics.	Hugo Herbelin	2018-05-11
\| \|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7470: use at least 6 Xs in mktemp filename templates	Gaëtan Gilbert	2018-05-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6959: [build] Build checker generated files using a make rule.	Enrico Tassi	2018-05-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix non-portable shebang in test-suite.	Théo Zimmermann	2018-05-11
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Notations: advertize that distinct "only parsing"/"only printing" rules work.	Hugo Herbelin	2018-05-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7466: Remove tutorials from the repo	Maxime Dénès	2018-05-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \