coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-20	[CI] Update coq_makefile	Pierre Roux

2020-04-15	Ignore -native-compiler option when disabled	Pierre Roux

2020-03-16	Fix coq-makefile/native1 test	Pierre Roux
	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).
2019-11-20	From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵	charguer
	(fixing bug #11057). 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.
2019-11-01	[test-suite] acknowledge coq_mafile installs .vos	Enrico Tassi

2018-11-05	Pass native and VM flags to the kernel through environment	Maxime Dénès
	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
2018-10-19	Porting the test-suite to coqpp.	Pierre-Marie Pédrot

2018-04-05	Improve shell scripts	zapashcanon

2017-08-29	coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs	Enrico Tassi

2017-07-20	more verbose logs for coq-makefile	Enrico Tassi

2017-07-20	coq-makefile: make test suite detect more errors	Enrico Tassi
	Replacing ; with && and enabling bash's pipefail option
2017-06-12	Merge PR#709: Bytecode compilation apart from 'make world', again	Maxime Dénès

2017-06-01	Test-suite: do not test native compiler if disabled by configure.	Maxime Dénès

2017-06-01	test-suite/coq-makefile: we do not build byte file by default anymore	Pierre Letouzey

2017-05-28	Merge PR#689: Changes to make coq-makefile not failing on MacOS X.	Maxime Dénès

2017-05-28	Merge PR#683: coq_makefile: build .cma for each .mlpack	Maxime Dénès

2017-05-27	coq_makefile: build .cma for each .mlpack	Enrico Tassi
	It used to generate only .cmo (the packed one). While this works if the plugin has no external dependencies, it does not if it does. The bug affected only bytecode builds
2017-05-27	Use specific shell for more robustness.	Théo Zimmermann

2017-05-26	Changes to make coq-makefile not failing on MacOS X.	Hugo Herbelin
	There is still however a failure with "rmdir --ignore-fail-on-non-empty".
2017-05-23	test suite for coq_makefile2	Enrico Tassi