coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix CI with parallel make (messed up dependencies)	Gaëtan Gilbert	2017-12-21
\| \| \| \| \| \| \| \| \|	When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper.
*	Circle CI: separate job to boot opam with all used packages.	Gaëtan Gilbert	2017-12-14
\|
*	Circle CI: remove warning jobs	Gaëtan Gilbert	2017-12-14
\|
*	Circle CI: uses dependencies between external developments.	Gaëtan Gilbert	2017-12-13
\|
*	Circle CI: enable TIMED for external developments	Gaëtan Gilbert	2017-12-13
\|
*	Circle CI: use cache for opam	Gaëtan Gilbert	2017-12-13
\|
*	Circle CI: enable native compiler.	Gaëtan Gilbert	2017-12-13
\|
*	Near-full implementation of Circle CI.	Gaëtan Gilbert	2017-12-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	VS gitlab: + fiat-crypto (Circle has 4GB RAM, gitlab 2GB) - caching opam (TODO) - publishing artefacts (TODO) * tests with -local, not installed VS travis: + reusing build products - flambda validate job (TODO?) - OSX jobs (TODO at least check if free OSX is possible) - linter (TODO?)
*	CI: poc Circleci configuration	Arnaud Spiwack	2017-12-11
	Revert "CI: poc Circleci configuration" Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34. CI: poc Circleci configuration Fixup Try minimising build for faster testing Various fixes Fixup: yaml identation Do not -j2: native compiler seems to take too much memory Revert "Do not -j2: native compiler seems to take too much memory" This reverts commit 4886151288a8d895c0fd23f9bded0970c59e1372. Deactivate native compiler Fixup (how did this happen?) Do not call time (not install on docker images, will fix later) Fixup Fixup