aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/system.mli
Commit message (Collapse)AuthorAge
* [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | One less global flag.
* [stm] Move process_id to Spawned.Gravatar Emilio Jesus Gallego Arias2017-12-11
| | | | | This brings us one step closer to actually moving all STM flags to `stm`.
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move toplevel/STM flags from `Flags` to their proper components; this ensures that low-level code doesn't depend on them, which was incorrect and source of many problems wrt the interfaces. Lower-level components should not be aware whether they are running in batch or interactive mode, but instead provide a functional interface. In particular: == Added flags == - `Safe_typing.allow_delayed_constants` Allow delayed constants in the kernel. - `Flags.record_aux_file` Output `Proof using` information from the kernel. - `System.trust_file_cache` Assume that the file system won't change during our run. == Deleted flags == - `Flags.compilation_mode` - `Flags.batch_mode` Additionally, we modify the STM entry point and `coqtop` to account for the needed state. Note that testing may be necessary and the number of combinations possible exceeds what the test-suite / regular use does. The next step is to fix the initialization problems [c.f. Bugzilla], which will require a larger rework of the STM interface.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Fix #4837: ./configure -local makes coqdep issue many warningsGravatar Maxime Dénès2016-11-04
| | | | | | We simply remove the warnings about paths mixing Win32 and Unix separators, since that situation does not seem problematic (c.f. discussion on the bug tracker).
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\
| * Print magic numbers in bad magic error messageGravatar Tej Chajed2016-04-25
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|\|
| * 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-02
|\|
| * 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
|\|
| * 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-06-01
|\|
| * Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that filesGravatar Hugo Herbelin2015-05-20
| | | | | | | | | | found in the file system have the expected lowercase/uppercase spelling)
* | Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-16
| | | | | | | | | | | | | | | | 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.
| * Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| | | | | | | | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
| * Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
|/ | | | | | | 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).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | | 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
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
| | | | backtracks, print time spent in each of successive calls.
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
| | | | | | | | | | | | | | | | | | | | | | | 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
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
| | | | | | | | | | | 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
* Removing mandatory suffixes for library files.Gravatar ppedrot2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
* v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)Gravatar herbelin2013-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - 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
* Remove System.process_time (dead code)Gravatar glondu2011-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection against anomaly when loading a state with bad magic number.Gravatar herbelin2010-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Account for Stephane Glondu's remarks.Gravatar fkirchne2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use existing functions to reimplement search_exe.Gravatar fkirchne2010-05-28
| | | | | | | | | 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
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - 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
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
| | | | | | | | | | | | | | | | | | | dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Look for csdp in $PATH at runtime, remove -csdpdir configure optionGravatar glondu2010-04-11
| | | | | | | | | 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - 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
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
| | | | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 23:24:40 +0000