coq/test-suite/coq-makefile/native1, branch master The formal proof system [CI] Update coq_makefile 2020-11-20T18:08:08+00:00 Pierre Roux 2020-11-13T11:03:19+00:00 146415fb624c182493d46413d738a3c2c3f47e02 






Ignore -native-compiler option when disabled
2020-04-15T14:38:24+00:00

Pierre Roux

2020-04-10T15:49:03+00:00

88b1f400ef05142a1f05cd7dcb34a4c682b7ab83












Fix coq-makefile/native1 test
2020-03-16T10:42:25+00:00

Pierre Roux

2020-03-14T17:42:54+00:00

0fdc7435d8b3666b17a9270375f5377fa340a773

This was accidentaly disabled by #6264 when no_native_compiler was
renamed to native_compiler.

Moreover, the (then unactivated test) was broken by commit 48ae6ce
(part of #9088).





This was accidentaly disabled by #6264 when no_native_compiler was
renamed to native_compiler.

Moreover, the (then unactivated test) was broken by commit 48ae6ce
(part of #9088).







From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixing bug #11057).
2019-11-20T11:02:00+00:00

charguer

2019-11-08T10:06:10+00:00

5bf25dfce23da1cee04b1c886e026f0dbc902c9c

With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.





With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.







[test-suite] acknowledge coq_mafile installs .vos
2019-11-01T11:17:08+00:00

Enrico Tassi

2019-10-28T11:51:49+00:00

76c72065a10381d91317c12436e3d6c1cd2e7348












Pass native and VM flags to the kernel through environment
2018-11-05T09:36:22+00:00

Maxime Dénès

2018-10-31T10:45:09+00:00

e2e7fea91f3af5dcf62052078da65489b796e9e2

The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).

We also add a `-bytecode-compiler` flag.

Fixes #4607





The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).

We also add a `-bytecode-compiler` flag.

Fixes #4607







Porting the test-suite to coqpp.
2018-10-19T14:24:46+00:00

Pierre-Marie Pédrot

2018-10-19T14:21:22+00:00

266050f7aaa0ee0b090b30b1acabaccda6919889












Improve shell scripts
2018-04-05T21:05:43+00:00

zapashcanon

2018-02-21T21:42:10+00:00

250502b01340ec6bedace85c6a2d4a4e57a107cf












coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs
2017-08-29T15:47:57+00:00

Enrico Tassi

2017-08-29T12:56:31+00:00

6e07e3a53e56882043b9db49f03fdf1470a16c46












more verbose logs for coq-makefile
2017-07-20T13:40:48+00:00

Enrico Tassi

2017-07-17T12:03:35+00:00

82b197a87e154d5206d74dfe53f5b5f5215f1a3e