aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* 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
* CList.factorize_left with a parametric equalityGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16923 85f007b7-540e-0410-9357-904b9bb8a0f7
* CList.prefix_of and CList.drop_prefix with a parametric equalityGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16922 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small optimizations in unification.Gravatar ppedrot2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing some generic equalities.Gravatar ppedrot2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing evar filters. It seems to cost quite a lot in unification,Gravatar ppedrot2013-10-22
| | | | | | | as witnessed by profiling on time-consuming files. I suspect we can do better by using a smarter representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16912 85f007b7-540e-0410-9357-904b9bb8a0f7
* More efficient operations in CArray.Gravatar ppedrot2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16910 85f007b7-540e-0410-9357-904b9bb8a0f7
* New feedback message: SlaveStatusGravatar gareuselesinge2013-10-22
| | | | | | To tell the gui what a slave is doing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
| | | | | | | | | | | | | | | | A future always carries a fix_exn with it: a function that enriches an exception with the state in which the error occurs and also a safe state close to it where one could backtrack. A future can be in two states: Ongoing or Finished. The latter state is obtained by Future.join and after that the future can be safely marshalled. An Ongoing future can be marshalled, but its value is lost. This makes it possible to send the environment to a slave process without pre-processing it to drop all unfinished proofs (they are dropped automatically in some sense). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* Some more hand-written comparison functions to avoid polymorphic comparison.Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vcs: the gc method returns the set of nodes that were collectedGravatar gareuselesinge2013-10-11
| | | | | | | In this way one can post-process them. Stm can for example cancel the ongoing jobs related to nodes that are no more there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dag: some comments on the concept of clusterGravatar gareuselesinge2013-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clib: fold_left_until added to CListGravatar gareuselesinge2013-10-10
| | | | | | | CStack just calls it to implement fold_until. CSig.seek renamed CSig.until, since there is no seek function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
* cStack: make it just a Stack with some extra APIGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16855 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a [modify] function to maps.Gravatar ppedrot2013-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16853 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: add options to disable fallbacks to ease regression testingGravatar gareuselesinge2013-10-03
| | | | | | | | | | STM falls back to local, lazy, evaluation if the slave dies badly or if there is a marshalling error. Both things should never occur, but is nice to have the system recover if a bug pops up. Nevertheless during regression testing these fallbacks should be disabled not to hide a new bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16841 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: number of slaves passed by the command lineGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar gareuselesinge2013-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16833 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 15:09:28 +0000