coq - The formal proof system

Age	Commit message (Collapse)	Author
2014-06-16	Preemptively remove files from native compilation.	Guillaume Melquiond
	Ocaml does not remove the .cmi file if compilation fails, thus causing subsequent native compilations to fail due to mismatching interfaces. For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
2014-05-22	Fix native_compute for systems with a limited size for the command line.	Guillaume Melquiond
	The call to the native compiler can fail due to the sheer amounts of -I options passed to it. Indeed, it is easy to get the command line to exceed 512KB, thus causing various operating systems to reject it. This commit avoids the issue by only passing the -I options that matter for the currently compiled code. Note that, in the worst case, this commit is still not sufficient on Windows (32KB max), but this worst case should be rather uncommon and thus can be ignored for now. For the record, the command-line size mandated by Posix is 4KB.
2014-04-29	Native compiler: hide compiled files in a .coq-native subdirectory.	Maxime Dénès

2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2013-12-29	Avoid generating .ml files in native compiler.	Maxime Dénès

2013-10-28	Native compiler: library compilation errors are now non fatal.	mdenes
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22	Misc changes around coqtop.ml :	letouzey
	- Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24	Reduced the noise level when dynlinking in bytecode mode or when	mdenes
	-no-native-compiler flag is on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16239 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-24	Native compiler: warnings were not turned off for OCaml 3.11	mdenes
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16140 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
	native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7