aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelib.mli
Commit message (Collapse)AuthorAge
* Fix native_compute for systems with a limited size for the command line.Gravatar Guillaume Melquiond2014-05-22
| | | | | | | | | | | | | | 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.
* Native compiler: hide compiled files in a .coq-native subdirectory.Gravatar Maxime Dénès2014-04-29
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | 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.
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
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