aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2013-11-08Useless array manipulation in Rtrees.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17070 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-08Do not compute formatter UTF8 length at creation time.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17069 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-07Partial application hunt.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17067 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-06better IStream.concatppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17064 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Adding closure-preventing functions in CArray. These functions are allppedrot
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
2013-11-04Allocation friendly version of Util.iterate.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17052 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Added an update function in CMap. It has the same signature as Map.add, butppedrot
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
2013-11-04Manual coding of Int.Map.find. We use unsafe features, but this functionppedrot
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
2013-11-02Adds a tactic give_up.aspiwack
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
2013-11-02Adds a shelve tactic.aspiwack
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
2013-10-31Future: better doc + restore ~pure optimizationgareuselesinge
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
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
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
2013-10-24Rtree : cleanup of the comparing codeletouzey
* 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
2013-10-24Specializing hash functions for widely used types.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Fix the semantic of the new List.remove_assoc_fletouzey
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
2013-10-24Ephemeron: add a function to run a collection cyclegareuselesinge
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
2013-10-24Turn many List.assoc into List.assoc_fletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23CList.factorize_left with a parametric equalityletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16923 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23CList.prefix_of and CList.drop_prefix with a parametric equalityletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16922 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList.index is now cList.index_f, same for index0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23Small optimizations in unification.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Removing some generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
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
2013-10-22More efficient operations in CArray.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16910 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22New feedback message: SlaveStatusgareuselesinge
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
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
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
2013-10-18Ephemeron: marshaling friendly keysgareuselesinge
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
2013-10-14Some more hand-written comparison functions to avoid polymorphic comparison.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11Vcs: the gc method returns the set of nodes that were collectedgareuselesinge
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
2013-10-11Dag: some comments on the concept of clustergareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16876 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10Clib: fold_left_until added to CListgareuselesinge
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
2013-10-07cStack: make it just a Stack with some extra APIgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16855 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06Added a [modify] function to maps.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16853 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
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
2013-10-03STM: number of slaves passed by the command linegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01typogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16833 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE protocol/serialization revisedgareuselesinge
- both requests and responses are serialized using the same generic code - no more interp message. Replaced by: - query: performs a query (Search/Check...) at a given state - add: adds to the document a new sentence at the current edit point - edit_at: changes the edit point. the result could be a rewind _or_ a focus to a specific zone that can be edited without rewinding the whole document git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16812 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/cstack: various improvementsgareuselesinge
- renaming reflecting the semantic of functions - ability to edit the stack at the top of a _focused_zone_ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16811 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/vcs: various improvementsgareuselesinge
- gc function to clear unreferenced nodes - utility function to get the ancestors of a commit - utility function to edit a merge commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16810 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/dag: various improvementsgareuselesinge
- clusters can hold some data - edges and nodes can be deleted git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16809 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/future: computations that are Exn can be replacedgareuselesinge
A computation that is an exception morally holds no value hence can be replaced by an type-equivalent computation. This mechanism is used to edit broken proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16808 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-27Removing a bunch of generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12CoqIDE: show number of proofs being checked in backgroundgareuselesinge
good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12Fix bug in CStack introduced by refactoringgareuselesinge
Refactorings should be tested, right? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16768 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02* lib/Unicode:regisgia
Workaround. Some characters seems to be missing in Camomile's category tables. We add them manually. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16755 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30recdef: restore old semantics (pre STM)gareuselesinge
The Stm commit switched from an home made handling of failures to a with_state_protection. This was wrong, since in case of success the global state has to be left altered. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 05:02:17 +0000