aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
AgeCommit message (Collapse)Author
2015-12-09Remove remaining occurrences of Unix.readdir.Guillaume Melquiond
2015-12-09Replace Unix.readdir by Sys.readdir in dir cache.Emilio Jesus Gallego Arias
This makes the function sightly more portable.
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-25Fix for case-insensitive path looking continued (#2554): Adding aHugo Herbelin
second chance to dynamically regenerate the file system cache when a file is not found (suggested by Guillaume M.).
2015-11-25Generalizing the patch to bug #2554 on fixing path looking withHugo Herbelin
correct case on MacOS X whose file system is case-insensitive but case-preserving (HFS+ configured in case-insensitive mode). Generalized it to any case-preserving case-insensitive file system, which makes it applicable to Windows with NTFS used in case-insensitive mode but also to Linux when mounting a case-insensitive file system. Removed the blow-up of the patch, improved the core of the patch by checking whether the case is correct only for the suffix part of the file to be found (not for the part which corresponds to the path in which where to look), and finally used a cache so that the effect of the patch is not observable. Note that the cache is implemented in a way not synchronous with backtracking what implies e.g. that a file compiled in the middle of an interactive session would not be found until Coq is restarted, even by backtracking before the corresponding Require. For history see commits b712864e9cf499f1298c1aca1ad8a8b17e145079, 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 69941d4e195650bf59285b897c14d6287defea0f e7043eec55085f4101bfb126d8829de6f6086c5a. as well as https://coq.inria.fr/bugs/show_bug.cgi?id=2554 discussion on coq-club "8.5 and MathClasses" (May 2015) discussion on coqdev "Coq awfully slow on MacOS X" (Sep 2015)
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-29Make the interface of System.raw_extern_intern much saner.Guillaume Melquiond
There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures.
2015-09-29Prevent States.intern_state and System.extern_intern from looking up files ↵Guillaume Melquiond
in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner.
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-20Revert "On MacOS X, ensuring that files found in the file system have the"Maxime Dénès
and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files" and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X." This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 and 69941d4e195650bf59285b897c14d6287defea0f and e7043eec55085f4101bfb126d8829de6f6086c5a. Trying to emulate a case sensitive file system on top of a case aware one is too costly: 3x slowdown when compiling the stdlib or CompCert.
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-22Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X.Hugo Herbelin
Thanks to Vadim Zaliva for testing.
2015-05-20Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that filesHugo Herbelin
found in the file system have the expected lowercase/uppercase spelling)
2015-05-15On MacOS X, ensuring that files found in the file system have theHugo Herbelin
expected lowercase/uppercase spelling (based on a patch by Pierre B.). This should fix #2554 (and see also discussion on coq-club, May 2015).
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
2015-02-16Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise.
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
(Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
2014-11-27better to always print the thread idEnrico Tassi
2014-10-24-help failing (fix 3762)Enrico Tassi
2014-09-09toploop plugins taken into account when printing --help (close: 3535)Enrico Tassi
E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
backtracks, print time spent in each of successive calls.
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
2014-07-07time tacHugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:42:12 +0000