aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Adding compatibility flag for 8.5.Gravatar Hugo Herbelin2015-12-14
| | | | Soon needing a more algebraic view at version numbers...
* Remove some occurrences of Unix.opendir.Gravatar Guillaume Melquiond2015-12-14
|
* Removing dead unsafe code in Genarg.Gravatar Pierre-Marie Pédrot2015-12-12
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\
| * Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removingGravatar Hugo Herbelin2015-12-10
| | | | | | | | "open Unix" from lib/system.ml.
| * Remove remaining occurrences of Unix.readdir.Gravatar Guillaume Melquiond2015-12-09
| |
| * Replace Unix.readdir by Sys.readdir in dir cache.Gravatar Emilio Jesus Gallego Arias2015-12-09
| | | | | | | | This makes the function sightly more portable.
* | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
| |
* | Leveraging GADTs to provide a better Dyn API.Gravatar Pierre-Marie Pédrot2015-12-05
| |
* | Specializing the Dyn module to each usecase.Gravatar Pierre-Marie Pédrot2015-12-04
| | | | | | | | | | | | Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|\|
| * Fix for case-insensitive path looking continued (#2554): Adding aGravatar Hugo Herbelin2015-11-25
| | | | | | | | | | second chance to dynamically regenerate the file system cache when a file is not found (suggested by Guillaume M.).
| * Generalizing the patch to bug #2554 on fixing path looking withGravatar Hugo Herbelin2015-11-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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)
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Fixed #4274, bad formatting of messages in emacs mode.Gravatar Pierre Courtieu2015-10-19
| |
| * Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-14
| |
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * aux_file: export API to ease writing of a Proof Using annotator.Gravatar Enrico Tassi2015-10-08
| |
| * CThread: blocking read + threads now worksGravatar Enrico Tassi2015-10-08
| |
| * Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | According to http://caml.inria.fr/mantis/view.php?id=5325 you can't use the same socket for both writing and reading. The result is lockups (may be fixed in 4.03).
| * Future: make not-here/not-ready messages customizableGravatar Enrico Tassi2015-10-08
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * emacs output mode: Added <infomsg> tag to debug messages.Gravatar Pierre Courtieu2015-10-02
| | | | | | | | So that they display in response buffer.
| * Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
| | | | | | | | | | | | 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.
| * Prevent States.intern_state and System.extern_intern from looking up files ↵Gravatar Guillaume Melquiond2015-09-29
| | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\|
* | Rich printing of messages.Gravatar Pierre-Marie Pédrot2015-09-20
| |
* | Adding rich printing primitives.Gravatar Pierre-Marie Pédrot2015-09-20
| |
| * Revert "On MacOS X, ensuring that files found in the file system have the"Gravatar Maxime Dénès2015-09-20
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-13
|\|
| * Fixing previous patch.Gravatar Pierre-Marie Pédrot2015-09-10
| |
| * Fixing the XML lexer definition of names to match the standard.Gravatar Pierre-Marie Pédrot2015-09-10
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-22
|\|
| * Revert the four previous commits and update the description of Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
| | | | | | | | | | Correcting the code w.r.t. to the API was not the right solution. Instead, the API comment had to be corrected.
| * More invariants in Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
| | | | | | | | | | | | We ensure statically by typing that the tags used by the rich printer are integers. Furthermore, we also expose through typing that tags are irrelevants in the returned XML.
| * More parametric type for generalized XML.Gravatar Pierre-Marie Pédrot2015-08-15
| |
| * Statically ensure that we omit null annotations in Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
| |
| * Fixing richpp behaviour w.r.t. its specification.Gravatar Pierre-Marie Pédrot2015-08-15
| | | | | | | | | | Contrarily to what was described in the API, nodes without annotations were not ignored by the printer but left there instead.
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-29
|\|
| * Fixing bug #4281: Better escaping of XML attributes.Gravatar Pierre-Marie Pédrot2015-07-28
| |
| * Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
| | | | | | | | | | | | | | | | File system.ml seemed like a better choice than util.ml for sharing the code, but it was bringing a bunch of useless dependencies to the IDE. There are presumably several other tools that would benefit from using open_utf8_file_in instead of open_in, e.g. coqdoc.
| * Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
| | | | | | | | This allows fatal_error to be used for printing anomalies at loading time.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-24
|\|
* | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-23
| | | | | | | | This allows fatal_error to be used for printing anomalies at loading time.
| * Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
| | | | | | | | | | Prints the VM bytecode produced by compilation of a constant or a call to vm_compute.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 22:30:15 +0000