aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/lib.mllib
Commit message (Collapse)AuthorAge
* Remove non-existent dependencyGravatar mrmr19932018-03-05
|
* [lib] Split auxiliary libraries into Coq-specific and general.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | | | | | | | | | | | | | | | | | Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
| | | | | | | Coqdep_boot has almost no dependencies, and hence can be compiled very early during the build, without relying on .ml.d files. Some code of system.ml is now in a separate file minisys.ml, which is also included in system.ml for compatibility.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\
| * Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
| | | | | | | | Fixes compilation of Coq with OCaml 4.03 beta 1.
* | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
| |
| * 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).
* 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.
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
|
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
| | | | | files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM.
* STM: move out a couple of submodulesGravatar Enrico Tassi2014-03-13
| | | | | These modules are not as reusable as one may want them to be, but moving them out simplifies a little STM.
* Work around for bug in threads + blocking io streamlinedGravatar Enrico Tassi2014-01-30
|
* Spawn: managed processesGravatar Enrico Tassi2014-01-26
| | | | | | | | | The Spawn and Spawned modules factor the operation of spawning a process. Both synchronous and asynchronous channels are supported. Both threaded and glib like main loop models are supported. Still, not all combinations are truly tested not equipped with a decent API: only async + glib and sync + thread are, since these are the models we use for coqide<->coqtop and coqtop<->worker respectively.
* Ephemeron: marshaling friendly keysGravatar gareuselesinge2013-10-18
| | | | | | | | | Ideally all unmarshallable content in the state should be stocked using Ephemeron keys. In this way the state becomes always marshallable (because the unmarshallable content is magically dropped). The mli contains more detailed doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
| | | | | | | | | | | | | | | Simple framework for remote counters. The slaves ask the master for a fresh value. On the master the thread manager answers with a bunch of fresh values (so that further requests can be immediately satisfied). Remote counters are guarded with a mutex on the master, because all slave managers as well as the master thread can access the counter at the same time. I know the name sucks. These counters are remote for the slaves, and local for the master. I'm open to suggestions... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vcs data structure (Git inspired builder for Dag)Gravatar gareuselesinge2013-08-08
| | | | | | | Given named branches, one can incrementally build a Dag using Git like commands git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16672 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dag data structureGravatar gareuselesinge2013-08-08
| | | | | | | This is a very simple, only growing, Dag structure with per node optional info and per edge info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Searchable stack data structureGravatar gareuselesinge2013-08-08
| | | | | | It is like Stack but one can search without popping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16670 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future library to represent pure computationsGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | Since the whole system is imperative, futures are run protecting the global state, and the final state is also saved to let the user freely chain futures. Futures can represent local (lazy) computations or remote ones (delegated). Delegating a future lets a third party assign its value at some poit in the future; in the meanwhile accessing the future value raises an exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
| | | | | | | | | | | | | 1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Gmap is now useless, hail to Map!Gravatar ppedrot2013-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing Fmap from libraries, it is not used anymore.Gravatar ppedrot2013-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16519 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing Fset, since it is not used anymore.Gravatar ppedrot2013-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the Tries module, uniformizing the names according toGravatar ppedrot2013-05-09
| | | | | | Map/Set style and renaming the file accordingly as Trie. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16504 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of module Gmapl.Gravatar ppedrot2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
* New module Xml_printer (dual to Xml_parser)Gravatar gareuselesinge2013-05-06
| | | | | | | Code for printing XML moved from xml_utils.ml to xml_printer.ml and improved to generate less garbage using Buffer.t systematically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 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
* 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
* 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
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
| | | | | | | | | | | | kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 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
* 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
* 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 an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 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
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | 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
* Moving XML handling to lib directoryGravatar ppedrot2011-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: Refactoring of hashconsingGravatar puech2011-07-29
| | | | | | | - moved the alterate Hashtable module to a separate file - moved all hashconsing-related function to a separate section in Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14312 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
| | | | | | | Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
* An generic imperative union-find, used for deps of evars in Class_tacticsGravatar letouzey2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13831 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove Safe_marshalGravatar glondu2011-01-06
| | | | | | | | | | | | Safe_marshal was using intermediate strings that are subject to Sys.max_string_length limitation. Use directly binary channel-oriented functions instead. This is a fix for bug #2471. Remark: this might reduce robustness w.r.t. noise in the communication channel. AFAIK, the original purpose of Safe_marshal was to work around a bug on Windows... this should be investigated further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep_boot : misc improvementsGravatar letouzey2010-09-17
| | | | | | | | | | - modules names can include quote ' - errors when parsing .mllib files are now properly reported instead of dying ugly on some sort of Failure - same when coqdep has to parse the output of ocamldep -modules - lib/lib.mllib contains a typo (lowercase ident) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13423 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 06:34:01 +0000