coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix #4403: insufficient handling of type-in-type in kernel.	Gaëtan Gilbert	2018-05-13
\|
*	Merge PR #7340: Remove DirClosedSection.	Enrico Tassi	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
\|\ \ \
* \ \ \	Merge PR #7466: Remove tutorials from the repo	Maxime Dénès	2018-05-11
\|\ \ \ \
* \ \ \ \	Merge PR #7461: [sphinx] Improve the proof handling chapter.	Maxime Dénès	2018-05-11
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7341: Don't recurse into closed modules/sections in split_lib.	Enrico Tassi	2018-05-11
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7363: [ci] Fix another issue with the timing tests	Gaëtan Gilbert	2018-05-11
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7456: [toplevel] Don't ignore output filename provided by user in -o	Théo Zimmermann	2018-05-11
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7437: [coqdep] Minor cleanups.	Pierre-Marie Pédrot	2018-05-10
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \|	Suggest going to /documentation to see a list of tutorials.	Théo Zimmermann	2018-05-10
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	One can build all the HTML doc using default.nix.	Théo Zimmermann	2018-05-10
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	Clean-up in Makefile.doc and include Sphinx in doc-html target.	Théo Zimmermann	2018-05-10
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	Remove tutorials.	Théo Zimmermann	2018-05-10
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7473: [ci] Add mit-plv/cross-crypto	Emilio Jesus Gallego Arias	2018-05-10
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7471: [travis] Fix version of camlp5 for OCaml 4.06.1.	Emilio Jesus Gallego Arias	2018-05-10
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \|	[build] Build checker generated files using a make rule.	Emilio Jesus Gallego Arias	2018-05-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Currently, `configure.ml` does copy/link some files from `kernel` to `checker` in an ad-hoc way. Instead, it is preferable to add a copy rule to make and let it handle the dependencies properly. This also fixes a dependency bug in Windows, as files wouldn't be properly refreshed if `configure` was not run each time.
\| \| * \| \| \| \| \| \| \| \|	[ci] Add mit-plv/cross-crypto	Jason Gross	2018-05-09
\| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
\| \| \| \| \| \| * \| \| \|	[sphinx] Improve proof handling chapter.	Théo Zimmermann	2018-05-09
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	Clarify that the description of coqtop does not reflect all user interfaces.	Théo Zimmermann	2018-05-09
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	[sphinx] Improvements around the Show commands, including missing indices ↵	Théo Zimmermann	2018-05-09
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	and indentation.
\| * \| \| \| \| \| \| \|	[travis] Add explicit opam switch command to guarantee we're using the ↵	Théo Zimmermann	2018-05-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	requested compiler.
\| * \| \| \| \| \| \| \|	[travis] Fix version of camlp5 for OCaml 4.06.1.	Théo Zimmermann	2018-05-09
\|/ / / / / / / /
\| \| \| \| \| \| * /	use at least 6 Xs in mktemp filename templates	Sven M. Hallberg	2018-05-09
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	OpenBSD mktemp fails with an error otherwise.
\| \| * \| \| \| \|	test for coqc -o	Enrico Tassi	2018-05-09
\| \| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq.	Gaëtan Gilbert	2018-05-09
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7435: [gitlab] Add bleeding-edge flambda build.	Gaëtan Gilbert	2018-05-09
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7459: Try to fix CODEOWNERS	Théo Zimmermann	2018-05-08
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408	Pierre-Marie Pédrot	2018-05-08
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \|	Try to fix CODEOWNERS	Maxime Dénès	2018-05-08
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \|	[gitlab] Do expensive builds with a flambda-compiled Coq.	Emilio Jesus Gallego Arias	2018-05-08
\| \| \|/ / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Gains seem superior to 50%, but data is taken from Gitlab so no reliable at all.
\| \| \| * \| \| \| \|	[CoqProject] Add some comments and remove unnecessary use of Pp.	Emilio Jesus Gallego Arias	2018-05-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	But indeed we need to split this file, as it is used now from CoqIDE is incorrect.
\| \| \| * \| \| \| \|	[coqdep] Remove unnecessary dependency on Pp and CError.	Emilio Jesus Gallego Arias	2018-05-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows for even earlier bootstrapping.
\| \| \| * \| \| \| \|	[coqdep] Minor cleanups.	Emilio Jesus Gallego Arias	2018-05-08
\| \|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Remove inclusion of the `tactics` directory, this is coming from a time loadable modules were found there, now all are under `plugins`. - Remove 2 dependencies so we can bootstrap coqdep earlier. - Use `Format` instead of `Printf` for printing.
\| \| \| * \| \| \|	[toplevel] Don't ignore output filename provided by user in -o	Emilio Jesus Gallego Arias	2018-05-08
\| \|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was a silly bug introduced in 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly forward the command line option. Thanks to @SkySkimmer for finding out the problem. closes #7447
\| \| * \| \| \|	[gitlab] Add bleeding-edge flambda build.	Emilio Jesus Gallego Arias	2018-05-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We also introduce a bit more systematic job naming: `base/edge`. In order to make the flambda switch selectable we update the Docker image so all the dependencies are installed in that one. Note the extra quote rule for the flambda parameters, but unless we can assign arrays to Gitlab variables there is not a good way to do this I'm afraid. With this patch we are getting close to being able to remove most builds from Travis.
\| * \| \| \| \|	[lib] Re-add `set_timeout` to help users workaround #7408	Emilio Jesus Gallego Arias	2018-05-07
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It seems like #7408 will need some potentially intrusive work, so let's add the low-level hook back so third party developments can work well with `8.8.1/master` for the moment.
* \| \| \| \|	Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)	Maxime Dénès	2018-05-07
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7371: Propose some updates of the CODEOWNER file.	Maxime Dénès	2018-05-07
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7445: [ci] Add ounit to the base Docker package set.	Gaëtan Gilbert	2018-05-07
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ↵	Maxime Dénès	2018-05-07
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	other improvements
* \ \ \ \ \ \ \	Merge PR #7440: [ci] Add a default target to `Makefile.ci`	Gaëtan Gilbert	2018-05-07
\|\ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \|	[ci] Add ounit to the base Docker package set.	Emilio Jesus Gallego Arias	2018-05-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This should help #6808.
* \| \| \| \| \| \| \| \|	Merge PR #7427: Fix #7413: coqdep warning on repeated files	Pierre-Marie Pédrot	2018-05-07
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CI	Gaëtan Gilbert	2018-05-06
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow ↵	Maxime Dénès	2018-05-06
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	kernel style.
\| \| \| \| * \| \| \| \| \| \|	[ci] Add a default target to `Makefile.ci`	Emilio Jesus Gallego Arias	2018-05-06
\| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	So we avoid problems like the one in #7438.
\| \| * \| \| \| \| \| \| \|	[gitlab] [circleci] Use a Custom Docker Image as base CI setup.	Emilio Jesus Gallego Arias	2018-05-05
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We provide a custom `Dockerfile` for Coq's CI system, based on `ubuntu:bionic`. The image includes the required set of packages and OPAM switches. This greatly simplifies the Gitlab and Circle scripts, at the cost of having to push a Docker build for them to depend on. Travis is not included in this PR as it requires significant more refactoring due to lack of native Docker support. This is work in progress but ready, a build hook is used so the image is properly tagged in the Docker autobuilder. We need to improve the autobuilder setup but this last point requires some design on how to trigger it. Fixes #7383
\| \| \| * \| \| \| \| \|	[sphinx] Fixes around apply, including indentation and fixing a Coq warning.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \|	[sphinx] Fixes around refine, including indentation and a hard-coded ref.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \| \| \|