coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-06-24	[test-suite] Fix printers test	Gaëtan Gilbert
	- fix the printers themselves after discharge was moved to the kernel - change the test to make it more robust In addition to checking that there is no "Error\|Unbound" in the output, ensure that the "go" function at the end of base_include is defined. If there are any errors in base_include it won't be defined. This makes us find out that the test was silently failing in all CI jobs except trunk+make. It failed to find the "include" file and so failed with "could not find file include.", which we didn't detect. To fix this: - change automatically included paths in Coqinit.init_ocaml_path to be based on coqlib instead of coqroot. This way top_printers.ml and base_include can find the compiled ml objects. - fix for dune: adapt the script to use include_dune when INSIDE_DUNE, add dependencies to test-suite/dune. The dependencies should be calculated automatically once Dune has better support for debug, or we implement proper support for test printers. Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
2019-05-28	Fix printers.sh test when missing coqtop.byte, print more info	Gaëtan Gilbert

2018-04-05	Improve shell scripts	zapashcanon

2017-06-11	A stronger test that #use"include";; works well.	Hugo Herbelin

2017-05-10	Moving code for miscellaneous tests to specific files.	Hugo Herbelin
	The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.