coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Improve shell scripts	zapashcanon	2018-04-05
\|
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\
\| *	Remove -j ${NJOBS} from make invocations in the ci	Jason Gross	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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 ```
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\\|
* \|	[travis] [fiat] Test also fiat-core.	Emilio Jesus Gallego Arias	2017-06-02
\| \| \| \| \| \| \| \|	I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
\| *	Add parsers-examples target to fiat-parsers ci	Jason Gross	2017-05-23
\| \| \| \| \| \|	This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
\| *	[travis] [8.6.only] Backport latest changes from trunk.	Emilio Jesus Gallego Arias	2017-03-22
\|
*	[travis] Basic support for overlays.	Emilio Jesus Gallego Arias	2017-03-13
\| \| \| \| \| \| \|	We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support.
*	[travis] Adding a template file and using it for all targets.	Théo Zimmermann	2017-03-10
\|
*	[travis] Change headband for wider compatibility.	Théo Zimmermann	2017-03-10
\|
*	[travis] [External CI] fiat-parsers	Emilio Jesus Gallego Arias	2017-02-24