coq/test-suite/coq-makefile/plugin-reach-outside-API-and-fail, branch master The formal proof system [API] remove large file containing duplicate interfaces 2017-12-27T13:19:59+00:00 Enrico Tassi 2017-12-22T13:11:55+00:00 b37d3f199e4521e2ae20cc96f0f2b04acc36c7cc ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. 
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
Fixing failing mkdir in test-suite for coq-makefile. 2017-11-24T12:31:41+00:00 Hugo Herbelin 2017-11-24T12:31:41+00:00 1077f801309cf4bd08eb0e63cf9a84271bcaf255 Calling the test a second time after a make clean was failing due to an existing "src" directory left by the first call. 
Calling the test a second time after a make clean was failing due to
an existing "src" directory left by the first call.
Remove dependency of test-suite on git (fix #5725). 2017-11-08T14:30:05+00:00 Théo Zimmermann 2017-11-08T14:29:56+00:00 360d28670511d51c2b63692c9ce0f7ebe5f1ae3e The two lines that this commit remove are spurious as a `git clean -dfx || true` is already performed in `test-suite/coq-makefile/template/init.sh`. While this resolves the accidental dependency on git, I am still unhappy with this call of `git clean -dfx`. 
The two lines that this commit remove are spurious as a `git clean -dfx || true`
is already performed in `test-suite/coq-makefile/template/init.sh`.
While this resolves the accidental dependency on git, I am still unhappy with
this call of `git clean -dfx`.
more verbose logs for coq-makefile 2017-07-20T13:40:48+00:00 Enrico Tassi 2017-07-17T12:03:35+00:00 82b197a87e154d5206d74dfe53f5b5f5215f1a3e 






Add support for "-bypass-API" argument of "coq_makefile"
2017-06-12T14:43:32+00:00

Matej Košík

2017-05-30T08:49:41+00:00

c054dda76825435019ad1b29f7f4292d937d98f9

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





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