aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
AgeCommit message (Collapse)Author
2014-01-30Relaunch all Unix.waitpid when they ended with EINTRPierre Letouzey
Moreover, cleanup of System.connect (used by the "external" tactic).
2014-01-04.vi files: .vo files without proofsEnrico Tassi
File format: The .vo file format changed: - after the magic number there are 3 segments. A segment is made of 3 components: bynary int, an ocaml value, a digest. The binary int is the position of the digest, so that one can skip the value without unmarshalling it - the first segment is the library, as before - the second segment is the STM task list - the third segment is the opaque table, as before A .vo file has a complete opaque table (all proof terms are there). A .vi file follows the same format of a .vo file, but some entries in the opaque table are missing. A proof task is stocked instead. Utilities: coqc: option -quick generates a .vi insted of a .vo coq_makefile: target quick to generate all .vi coqdep: generate deps for .vi files too votour: can browse .vi files too, the first question is which segment should be read coqchk: rejects .vi files
2013-11-24Hardening the reading function of vo files.Pierre-Marie Pédrot
2013-11-07Partial application hunt.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17067 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-28Removing some lone List.assoc & List.mem in lib.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
Since digests are strings (of size 16), we just dump them now in vo files (cf. Digest.output) instead of using Marshal on them : this is cleaner and saves a few bytes. Increased VOMAGIC to clearly identify this change in the format. Please rerun ./configure after this commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Removing mandatory suffixes for library files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (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-01v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Actually adding backtrace handling.ppedrot
I hope I did not forget some [with] clauses. Otherwise, some stack frame will be missing from the debug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (lib)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15991 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13More monomorphizationsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-05More accurate timings for "Time foo"letouzey
The elapsed time in seconds was computed via a difference of Unix.time(), but these Unix.time() aren't precise enough (just a number of seconds), and a difference is hence even less precise. We now use Unix.gettimeofday, and round the time difference to the millisecond. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15858 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12lib directory is cut in 2 cma.pboutill
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20coqrc in the right XDG_CONFIG_HOME/coq folderpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Patch by Dan Grayson to ensure that "Add LoadPath ... as ..." closesherbelin
the file descriptors on directories that it does not need to keep open (the maximum number of simultaneously opened file descriptors supported by the operating system is not so large in practice, e.g. 256 on MacOS X). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14565 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01[/]+ is equivalent to [/] in System and its copypboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14435 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-19Remove System.process_time (dead code)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14145 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Win32: remove the need for Coq.bat and Coqide.batletouzey
This is an adaptation of commit r13750 of branch 8.3 - coqlib is currently computed relatively of Sys.executable_name, hence no need to set it manually - in Win32, better detection of user home dir : in System.ml, if HOME isn't set, we look now for HOMEDRIVE\HOMEPATH, and then for USERPROFILE - concerning PATH, in Win32 we now add coqbin (or the location of coqide) to PATH during the initialization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14041 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Account for Stephane Glondu's remarks.fkirchne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13035 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28Use existing functions to reimplement search_exe.fkirchne
Most of the code in search_exe_in_path was about parsing the PATH into a list of directories, which is now done in function lpath_from_path. Existence of the file is checked using already existing functions, so that duplication is minimized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13033 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-11Look for csdp in $PATH at runtime, remove -csdpdir configure optionglondu
The csdp path computed by the configure script wasn't used at all, but was forcing presence of csdp at configure time whereas it is not used at all in the build process. Instead, we replace the configure-time check with a runtime check for existence of csdp in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Fixed anomaly when trying to load non existing file starting with "./" or "../".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12227 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Backporting from v8.2 to trunk:herbelin
- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
- Improved warning when found several path to the same file in path [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to true (i.e. eq_true) [Datatypes.v, tactics] PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-30Fichiers oubliés lors du 11188 :-(herbelin
On en profite pour faire dépendre l'avertissement de where_in_path du mode silencieux. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11193 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-11implements a better way to respect the Unix convention that processes ↵bertot
receive their own name as first argument. This is needed to make external tactics work when the external program is interpreted and the operating system is Mac OS git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10437 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-28Correction d'un bug dans check_and_warnnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10100 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-22Ajout d'un warning losrqu'un nom de bibliothèque est ambigünotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-21Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deherbelin
chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30Correction bug #990 (LoadPath et option -R de coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8877 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-23bug de coqide sous windows (bad file descriptor)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7603 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19Déplacement de fonctionnalités unix et browser de ide vers libherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Bug synchronisation fonction connectherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6685 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout d'un processus de communication entre Coq et un outil externeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6677 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-08un argument booleen inutilisé dans expand_macrosletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5737 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Lazy manuelles dans le codecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-05Lazy experimentale temporaire...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 12:43:37 +0000