coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-01-04	Remove formal-topology from CI	Maxime Dénès
	This was suggested by the author. See https://github.com/bmsherman/topology/issues/23
2018-08-31	Download tarball instead of cloning external projects (when $CI is set).	Théo Zimmermann
	This allows to use fixed commits and not just branches or tags. We keep using git clone when $FORCE_GIT is set (for projects on gforge.inria.fr and projects pulling dependencies through git submodules). fiat-parsers also calls git submodule, but inside its own Makefile.
2018-04-05	Improve shell scripts	zapashcanon

2017-12-13	Put bignums, math-classes and corn dependencies in Makefile	Gaëtan Gilbert

2017-07-04	Merge branch 'v8.6'	Pierre-Marie Pédrot

2017-06-16	Remove -j ${NJOBS} from make invocations in the ci	Jason Gross
	According to https://www.gnu.org/software/make/manual/html_node/Options_002fRecursion.html#Options_002fRecursion it's not necessary, because we pass `-j ${NJOBS}` to the top-level `make` invocation in `.travis.yml`. Additionally, explicitly passing `-j` in, e.g., fiat-crypto, results in error messages such as ``` make[2]: * write jobserver: Bad file descriptor. Stop. make[2]: * Waiting for unfinished jobs.... make[2]: * write jobserver: Bad file descriptor. Stop. make[1]: * [coqprime] Error 2 make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2! make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c ``` because the `-j` on the `make` in the `ci-fiat-crypto.sh` script disables jobserver mode, and the submake in fiat-crypto to make coqprime does not explicitly pass `-j`, and so reenables jobserver mode, and then `make` gets very confused. Commit made with ```bash cd dev/ci git grep --name-only -- 'make -j ${NJOBS}' \| xargs sed s'/make -j \${NJOBS}/make/g' -i git grep --name-only -- 'make -f Makefile.coq -j ${NJOBS}' \| xargs sed s'/make -f Makefile.coq -j \${NJOBS}/make -f Makefile.coq/g' -i ```
2017-06-13	[travis] extra test ci-bignums (+factorize other scripts)	Pierre Letouzey

2017-06-13	[travis] overlay + extra deps for math-classes (and formal-topology)	Pierre Letouzey

2017-05-01	Add bmsherman/topology to the ci	Jason Gross
	This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.