| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |\
| |
| |
| | |
subdirectory.
|
| | |
| |
| |
| | |
This allows us to avoid doing git clean.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
These work on precomputed build logs (in this case, from a recent
partial build of fiat-crypto).
They are meant to serve as human-readable sanity checks of output
format.
Separate out the sane bits of template/init.sh from the ones messing
with directory structure (which are fragile and make assumptions about
where the calling script is sourcing it from).
N.B. The test-suite removes all *.log files, so we use *.log.in.
N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile,
because coqc, on Windows, doesn't handle cygwin paths passed via
-coqlib, and `pwd` gives cygwin paths.
N.B. We have .gitattributes to satisfy the linter (as per
https://github.com/coq/coq/pull/6149#issuecomment-346410990)
|
| |
|
|
|
| |
The validity of this test depended on Makefile issueing warnings in English.
We simply force the global language of the shell to be C.
|
| |
|
|
| |
Replacing ; with && and enabling bash's pipefail option
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
zapashcanon
Enrico Tassi
Maxime Dénès
Gaëtan Gilbert
Jason Gross
Pierre-Marie Pédrot
Matej Košík
Gaëtan Gilbert
Théo Zimmermann