aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/clib.mllib
Commit message (Collapse)AuthorAge
* 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.
* remove unused iArrayGravatar Enrico Tassi2015-01-06
|
* Adding a terminal library.Gravatar Pierre-Marie Pédrot2014-11-15
|
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
| | | | | | printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics.
* RichPp: New module.Gravatar Regis-Gianas2014-11-04
| | | | | | | | | It is responsible for turning a tagged pretty-printing into a semi-structured document. clib.mllib: Include RichPp as well as Xml_*. The migration of Xml_* from lib to clib is needed by RichPp depends on these modules.
* Pp compiles after feedbackGravatar Enrico Tassi2014-07-29
|
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | | | | | | | | | lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
|
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
|
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
| | | | (hopefully), and forbids generic equality. Still, it allows generic hash.
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
| | | | | | | | | | | the provided type to come with a hashing function. The internal representation is changed, such that values are first compared w.r.t. to their hash. This effectively saves a lot of comparisons which may be far more expensive than O(1), as in the string case, hence resulting in an overall speedup. CAVEAT: everything is not implemented yet, and order-sensitive functions now do not respect the provided order anymore.
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
| | | This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
* Remove useless Xml_utilsGravatar Pierre Letouzey2014-01-30
|
* clib.mllib: remove duplicated Flags entryGravatar Pierre Letouzey2014-01-30
|
* Aux_file: cache information at compile time for later (re)useGravatar Enrico Tassi2014-01-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For a file dir/a.v the corresponding aux file dir/.a.aux can store arbitrary data. It maps a "Loc.t * string" (key) to a "string" (value). Pretty much anything can fit in this schema, but ATM I see only the following possible uses: 1) record inferred data, like the set of section variable used, so that one can later use this info to process proofs asynchronously (i.e. compute their discharged type without knowing the proof term). 2) record timings (how long it takes to build a proof term or check it), so that one can take smarter scheduling decisions 3) record a bloated proof trace for automatic tactics, so that one can replay it faster (a sort of cache). For that to be useful an Ltac API is required. The .aux file contains the path of the .v and its md5 hash. When loaded it defaults to the empty map is the file is not there or if the .v file changed. Not finding some data in the .aux file cannot be a failure, but finding it may help in many ways. The current file format is very simple but human readable. It is generated/parsed using printf/scanf and in particular the %S formatter for the value string. The file format is private to the Aux_file module: only an abstract interface is provided. The current file format is not robust in face of local changes. Any change invalidates the md5 hash (and the Loc.t is very likely to change too).
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
| | | | | | | | | | The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
* state_id data typeGravatar gareuselesinge2013-08-09
| | | | | | (this should have been the first commit of Paral-ITP) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a persistent stream data structure.Gravatar ppedrot2013-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16532 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a generic notion of hook. Hooks are functions to be setGravatar ppedrot2013-05-12
| | | | | | | exactly once at runtime, often to reduce the mutual dependency of modules. This module permits to track them more easily. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
| | | | | | it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: Globalization feedback (proof of concept)Gravatar gareuselesinge2013-04-25
| | | | | | | | | | | | | | | | | | | | A new feedback message for globalization infos can be sent by Coq to Coqide. Coqide stores the information in the proof of concept module wg_Tooltip, that also sets things up so that these infos are displayed as a tooltip when the mouse is over the text they are attached to. These infos are available only on locked text, and on the text just processed in the case of an error (on this piece of text, they vanish as the error tag vanishes as soon as the user edits the text). wg_Tooltip stocks these infos as lazy string. This is not needed in the proof of concept, but is necessary to scale up: Coq may not generate the full piece of info when the message is sent (because of high computational cost or big size) and just send an id; later on, when/if the user asks for the piece of info, the gui requests the info explicitly using the id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a module of immutable arrays. Not as full as CArray, but shouldGravatar ppedrot2013-04-09
| | | | | | be soon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16391 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated Exninfo to the new Store type.Gravatar ppedrot2013-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added exception enrichment. Now one can define additional arbitraryGravatar ppedrot2013-02-18
| | | | | | | | | | | information worn by exceptions. The implementation is quite hackish but it should work nonetheless. Basically, it adds an additional cell to exceptions arguments, in which you can put whatever you want. By typing invariants, you may not reach this cell by normal means, so it should be safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added backtrace primitives.Gravatar ppedrot2013-01-28
| | | | | | | | | | | | | | | | | | | | | | Using OCaml 3.11+ builtin facilities to record stack frames during exception raising, we can now recover at runtime the backtrace of an uncaught toplevel exception and display it to the user, without the infamous OCaml debugger. The backtrace is displayed when using the [-debug] flag. This requires a bit of discipline, as each time we reraise an exception we need to keep track of those frames we discarded between the previous raise and the current [try-with] branch. Currently, only [Anomaly] is handled, but this can be ported to any exception as long as we add the backtrace info into the exception, and we provide the corresponding handler to [Backtracke.register_backtrace_handler]. Hopefully this should not be to costly, as we only do little work when reraising, and only with the [-debug] flag set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a CString module.Gravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an Int module with dummy utility functions.Gravatar ppedrot2012-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15956 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Pp to CLib. In particular, Pp does not depend on CAMLP4/5Gravatar ppedrot2012-09-10
| | | | | | anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15792 85f007b7-540e-0410-9357-904b9bb8a0f7
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Put Option in ClibGravatar pboutill2012-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Deque module to CLib (to be used in CoqIDE).Gravatar ppedrot2012-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert copy/pasted function in to minilib thanks to clib.cmaGravatar pboutill2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 01:05:34 +0000