aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Christmas is over...Gravatar Maxime Dénès2014-01-15
|
* STM: additional fix for STM + vm_computeGravatar Enrico Tassi2014-01-07
| | | | | | | Thanks again Maximes. This time the C value was stored in the env_(named|rel)_val of the environment
* STM: fix worker crash when doing vm_computeGravatar Enrico Tassi2014-01-06
| | | | | | | | | | Kudos to Maximes for finding the culprit in no time! Values of type 'Pre_env.key' store in the OCaml state the 'address' of an already evaluated constant in the VM's C state. Such values are not sent to work processes. The worker is going to re-evaluate the constant, but just once, since the cache is cleared only when the env is marshalled (via ephemerons).
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | Proof using can be followed by: - All : all variables - Type : all variables occurring in the type - expr: - (a b .. c) : set - expr + expr : set union - expr - expr : set difference - -expr : set complement (All - expr) Exceptions: - a singleton set can be written without parentheses. This also allows the implementation of named sets sharing the same name space of section hyps ans write - bla - x : where bla is defined as (a b .. x y) elsewhere. - if expr is just a set, then parentheses can be omitted This module also implements some AI to tell the user how he could decorate "Proof" with a "using BLA" clause. Finally, one can Set Default Proof Using "str" to any string that is used whenever the "using ..." part is missing. The coding of this sucks a little since it is the parser that applies the default.
* Environ: export API to transitively close a set of section variablesGravatar Enrico Tassi2014-01-05
|
* 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
* kernel: save in aux the list of section variables usedGravatar Enrico Tassi2014-01-04
| | | | | This has nothing to do with the kernel itself, but it is the place where this piece of data is inferred.
* Remove obsolete comment about Let being processed synchronouslyGravatar Enrico Tassi2014-01-04
| | | | | Let proof terms are stocked in the named_context that is used directly everywhere, hence there is no way to stock a Future proof term there.
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
| | | | | | | | | | | | | | | | Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM.
* Avoid generating .ml files in native compiler.Gravatar Maxime Dénès2013-12-29
|
* Got rid of unused lazy flag in the native compiler.Gravatar Maxime Dénès2013-12-29
|
* Revert "Partial revert of r16711"Gravatar Maxime Dénès2013-12-28
| | | | | | | The sharing introduced by this commit is now correct, since a reference used by the native compiler has been removed from constant_body. This reverts commit 413f5fcd4bf581ff3ea4694c193d637589c7d54f.
* Removing native_name reference from constant_body.Gravatar Maxime Dénès2013-12-28
| | | | | | For now, this reference (renamed to link_info) has been moved to the environment (for constants and inductive types). But this is only a first step towards making the native compiler more functional.
* STM: capture type checking error (Closes: 3195)Gravatar Enrico Tassi2013-12-24
| | | | | Also, the future chain that reaches the kernel is greedy. If the user executes step by step, then the error is raised immediately.
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
| | | | | | To make this possible the state id has to reach the kernel. Hence definition_entry has an extra field, and many files had to be fixed.
* Tentative fix of the guardedness checker by Christine and me. All stdlib and ↵Gravatar Matthieu Sozeau2013-12-17
| | | | test-suite pass.
* A few fixes to the build system (mostly for ocamlbuild)Gravatar Pierre Letouzey2013-12-16
| | | | | | | | | | | | | | * vars.mli was mentionning Term instead of Constr, leading to a dep cycle * Having a file named toplevel/toplevel.ml isn't a good idea when we also have a toplevel/toplevel.mllib that ought to produce a toplevel.cma. We rename toplevel.ml into Coqloop.ml * Extra cleanup of toplevel.mllib : - Ppextra isn't anywhere around (?!) - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway - Vernacexpr is a .mli and shouldn't appear in an .mllib * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml) * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread for coqchk).
* Do not overallocate closures' named environments in infos. Modifying the accessGravatar Pierre-Marie Pédrot2013-12-15
| | | | function is sufficient to skip the undefined variables.
* Reduction: every n iterations a slaves process checks for interruptionGravatar Enrico Tassi2013-11-27
| | | | | | | I chose n to be 10000 iterations. It might be big, but a slave, to check for a termination request, has to pass the ball to the thread that sends "regularly" Ticks to the master process. Thread.yield is a system call, so we have to do it very rarely.
* Slightly more efficient zip function in Closure.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Small allocation improvement in Closure.Gravatar Pierre-Marie Pédrot2013-11-23
|
* Revert "Fast lookup_named in environments, based on maps instead of lists."Gravatar ppedrot2013-11-15
| | | | | | | Contrarily to my machine results, it seems that it tore down the performance of Coq on benchmarks. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fast lookup_named in environments, based on maps instead of lists.Gravatar ppedrot2013-11-13
| | | | | | | | | This was quite a severe performance bottleneck. Ideally, this data structure should be put into contexts, but the relevant type is transparent... For now, we stick to this inelegant workaround. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17086 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less partial applications in Vars, as well as better memory allocation.Gravatar ppedrot2013-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using allocation-free version of Array higher-order function in criticalGravatar ppedrot2013-11-04
| | | | | | cases, which are precisely term manipulation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17054 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar module now uses default Int maps and sets.Gravatar ppedrot2013-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Closure: fix an issue with r16959 spotted by MatthieuGravatar letouzey2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)Gravatar letouzey2013-10-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit should fix the contrib ProjectiveGeometry This update_delta_resolver is in fact a sequential composition (resolver1 then resolver2). The earlier version was strangely favoring the bindings coming from resolver2 over the bindings coming from (resolver1 chained with resolver2). So any inlining information stored in resolver1 could be discarded savagely. Apparently, this situation wasn't occurring in practice until recently, when I started to do lots of Mod_subst.join for improving the size of modular libobjects in the vo's. So, when combining two resolvers now : - Inline(_,None) is the weakest information, it's just a declaration that we intend to inline this kn someday if possible (i.e. when we'll have a transparent implementation for it). This kind of Inline is only relevant inside a module type. - Equiv(_) should only appear in modules (after some Include) so it should be ok if it takes precedence over any Inline(_,None) remaining in the other resolver. - Inline(_,Some _) is there after functor application (cf inline_delta_resolver) : we've done the inlining, so we don't care anymore about other Equiv(_) or Inline(_,None) informations about this kn, since we have anyway a new body for it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Kerpair.hash. Since the beginning, it dit not respect the typeGravatar ppedrot2013-10-31
| | | | | | equality, maybe impeding hashconsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16964 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
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
| | | | | | But for vm, the kernel should be functional now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoiding useless allocations in Closure.Gravatar ppedrot2013-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allocation-friendly version of [Pre_env.push_named].Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing universes: tail-rec, allocation friendly [compare_leq].Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16946 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: library compilation errors are now non fatal.Gravatar mdenes2013-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
* More sharing in Constr.map_with_binders.Gravatar ppedrot2013-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16938 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
* inductive.ml : get rid of some obvious (Lazy.force (lazy t))Gravatar letouzey2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16935 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
* 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.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
* Optimizing Vars.replace_varsGravatar ppedrot2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16916 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
* Various optimizations in Constr, such as term sharing and allocationGravatar ppedrot2013-10-22
| | | | | | avoiding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16911 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 05:18:12 +0000