coq/Makefile.checker, branch master The formal proof system [build] Remove leftovers of codesigning / OSX IDe infrastructure. 2021-04-19T11:44:08+00:00 Emilio Jesus Gallego Arias 2021-04-04T13:17:37+00:00 819e8a4f84bc6798b4e890090fb74a3f02626d6b This is not used anymore, and after #14122 the makefile parts for the dmg generation are not used anymore. Closes #7476 . 
This is not used anymore, and after #14122 the makefile parts for the
dmg generation are not used anymore.

Closes #7476 .
Update headers in the whole code base. 2020-03-18T11:15:43+00:00 Théo Zimmermann 2020-03-18T11:14:26+00:00 a99776e10e0b2198d2b811ad82631111fb450f8a Add headers to a few files which were missing them. 
Add headers to a few files which were missing them.
make: guard cp calls with rm -f on executables 2019-10-30T15:11:12+00:00 Gaëtan Gilbert 2019-10-30T15:10:40+00:00 fe61f673dfdba1598842b9d56a761c5229aaf4e9 Fix #10728 
Fix #10728
Update py-style headers to new year. 2019-06-17T16:08:32+00:00 Théo Zimmermann 2019-06-06T09:22:08+00:00 7521031c01976b045f81b6123f9ee9be77122a55 






Remove checker printers
2018-11-08T14:01:24+00:00

Gaëtan Gilbert

2018-11-08T14:01:24+00:00

a7522a0ea76a6efaed9342d08a95363b56d88d32

Now that the checker is using the regular kernel files it can also use
the normal printers.





Now that the checker is using the regular kernel files it can also use
the normal printers.







[checker] Refactor by sharing code with the kernel
2018-11-06T13:19:37+00:00

Maxime Dénès

2018-10-09T16:21:04+00:00

a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3

For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.

With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.

We also rename some files from the checker so that they don't clash with
kernel files.





For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.

With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.

We also rename some files from the checker so that they don't clash with
kernel files.







Rename checker/{main->coqchk}
2018-10-29T12:10:38+00:00

Gaëtan Gilbert

2018-10-17T13:04:12+00:00

98a792b79c4bea810bc4fe623c9006e8eeaeb468












[build] Refactoring to config lib and ocamldebug tweaks.
2018-10-22T22:42:04+00:00

Emilio Jesus Gallego Arias

2018-10-17T13:24:15+00:00

1db19a8f454e0f8c5a60101c87ccd38e0883d530

We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.

Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.

We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.





We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.

Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.

We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.







Suppress useless "true bin/*.opt.exe" messages from no-op STRIP and CODESIGN steps.
2018-06-30T17:30:30+00:00

Jim Fehrle

2018-06-29T05:55:33+00:00

5d4616f63c66291d2e83c5d9847749fa89b33bf6












Infrastructure for ocamldebug on the checker
2018-05-13T11:49:11+00:00

Gaëtan Gilbert

2018-04-22T13:27:22+00:00

b06de08733bb01efcbb8b902fe3157b7045c8bb3