aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
...
* CString: avoid redefining is_subGravatar Pierre Letouzey2014-01-30
|
* Remove useless Xml_utilsGravatar Pierre Letouzey2014-01-30
|
* clib.mllib: remove duplicated Flags entryGravatar Pierre Letouzey2014-01-30
|
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
|
* Work around for bug in threads + blocking io streamlinedGravatar Enrico Tassi2014-01-30
|
* STM: tell the user if the master is recomputing states validated by workersGravatar Enrico Tassi2014-01-30
| | | | | | When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly.
* Fixing backtrace handling here and there.Gravatar Pierre-Marie Pédrot2014-01-30
|
* Adding a smartmap[i] operator to maps.Gravatar Pierre-Marie Pédrot2014-01-29
|
* CoqIDE: command line for extra coqtop "flags"Gravatar Enrico Tassi2014-01-26
| | | | Like the socket for the OCaml debugger
* 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.
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
|
* fix typoGravatar Enrico Tassi2014-01-06
|
* Paral-ITP: cleanup of command line flags and more conservative defaultGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | -async-proofs off the system behaves as in 8.4 -async-proofs lazy proofs are delayed (when possible) but never processed in parallel -async-proofs on proofs are processed in parallel (when possible). The number of workers is 1, can be changed with -async-proofs-j. Extra options to the worker process can be given with -async-proofs-worker-flags. The default for batch compilation used to be "lazy", now it is "off". The "lazy" default was there to test the machinery, but it makes very little sense in a batch scenario. If you process things sequentially, you'd better do them immediately instead of accumulating everything in memory until the end of the file and only then force all lazy computations. The default for -ideslave was and still is "on". It becomes dynamically "lazy" on a per task (proof) basis if the worker dies badly. Note that by passing "-async-proofs on" to coqc one can produce a .vo exploiting multiple workers. But this is rarely profitable given that master-to-worker communication is inefficient (i.e. it really depends on the size of proofs v.s. size of system state).
* .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
* Future: allow custom action when a delegated future is forcedGravatar Enrico Tassi2014-01-04
| | | | | | | | The default action is to raise NotReady, but one may want to make the action "blocking" but successful. Using this device all delayed proofs can be "delegated". If there are slaves, they will eventually pick up the task. If there are no slaves, then the future can behave like a regular, non delegated, lazy computation.
* 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).
* CoqIDE: new feedback "incomplete" to signal partial QedGravatar Enrico Tassi2013-12-24
|
* Future: optional greedy chainingGravatar Enrico Tassi2013-12-24
| | | | | | If a Future.computation is already a value v or an exception and is chained in a greedy way with a function f, then f v is executed immediately (or the exception is raised).
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
|
* Fix CoqIDE on windowsGravatar Enrico Tassi2013-12-10
|
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
|
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
| | | | | | | | | | | | | | | | | refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
* Old message Interp returns the state id so that one can BackTo itGravatar Enrico Tassi2013-11-27
|
* New option --help-XML-protocol to document the XML procol used by -ideslaveGravatar Enrico Tassi2013-11-27
| | | | | | Serialize.ml spits out its own documentation. Not everything is statically checked, so it risks to get outdated. Ideas on how to statically/dynamically check that the doc is in sync are welcome.
* First stab at retrocompatible INTERP messageGravatar Enrico Tassi2013-11-27
|
* Adding a generic Int.Map using persistent arrays.Gravatar Pierre-Marie Pédrot2013-11-26
|
* Adding fold_left / fold_right function to maps.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Hardening the reading function of vo files.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Tweaking arity & allocation of some basic functions.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Using hashes instead of strings in dynamic tags. In case of collision, anGravatar Pierre-Marie Pédrot2013-11-22
| | | | | | | | anomaly is raised. As there are very few tags defined in Coq code, this is very unlikely to appear, and can be fixed by tweaking the name of the dynamic argument. This should be more efficient, as we did compare equal strings each time.
* Better implementation for stores.Gravatar ppedrot2013-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding an unsafe mapping function to maps.Gravatar ppedrot2013-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Useless array manipulation in Rtrees.Gravatar ppedrot2013-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17070 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not compute formatter UTF8 length at creation time.Gravatar ppedrot2013-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial application hunt.Gravatar ppedrot2013-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17067 85f007b7-540e-0410-9357-904b9bb8a0f7
* better IStream.concatGravatar ppedrot2013-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding closure-preventing functions in CArray. These functions are allGravatar ppedrot2013-11-04
| | | | | | | | | | | | | | | | | higher-order functions like map and iter, and they are modified so that they take one additional argument, thus saving a cloure allocation. Compare the following. Array.iter: ('a -> unit) -> 'a array -> unit Array.Fun1.iter: ('r -> 'a -> unit) -> 'r -> 'a array -> unit Basically, Array.Fun1.iter f x v = Array.iter (f x) v, though it does not allocate a closure. For now only the most critical functions are recoded. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allocation friendly version of Util.iterate.Gravatar ppedrot2013-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an update function in CMap. It has the same signature as Map.add, butGravatar ppedrot2013-11-04
| | | | | | expects the given key to be present, and thus is faster. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Manual coding of Int.Map.find. We use unsafe features, but this functionGravatar ppedrot2013-11-04
| | | | | | | is quite critical indeed, as it is one of the most used throughout Coq executions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
| | | | | | Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
| | | | | | The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
| | | | | | | | | | | This optimization was undone because the kernel type checking was not a pure functions (it was accessing the conv_oracle state imperatively). Now that the conv_oracle state is part of env, the optimization can be restored. This was the cause of the increase in memory consumption, since it was forcing to keep a copy of the system state for every proof, even the ones that are not delayed/delegated to slaves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
| | | | | | | | | | | To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
| | | | | | | | | * Using generic fold functions was unecessarily obscure * No more List.mem and hence indirect use of ocaml generic comparison * Rtree.equiv (former Rtree.compare_rtree) has now a less cryptic semantic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the semantic of the new List.remove_assoc_fGravatar letouzey2013-10-24
| | | | | | | Unlike Ocaml's stdlib List.remove_assoc, I was raising Not_found when the key to remove wasn't there... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16931 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ephemeron: add a function to run a collection cycleGravatar gareuselesinge2013-10-24
| | | | | | | | | | | | This is necessary if one wants to check how much memory Coq uses after a collection. The idiom is: Gc.full_major (); Ephemeron.clear (); Gc.full_major (); since the first collection may just put collected ephemerons in a to_be_cleared list that is processed by Ephemeron.get/create/clear. Processing the list may create new garbage (the content of the ephemeron), Hence a new Gc cycle has to be run afterwards. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 11:52:41 +0000