aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* STM: when batch compiling a vo, assert we behave conservativelyGravatar Enrico Tassi2014-02-26
| | | | | This meas that the list of future_constraints in safe_env is empty, meaning that nothing was delayed.
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
| | | | | Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
| | | | | When you resume the compilation of a .vi file, you want to avoid collisions on fresh names.
* univ: removing dead codeGravatar Enrico Tassi2014-02-26
|
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To obtain a.vo one can now: 1) coqtop -quick -compile a 2) coqtop -vi2vo a.vi To make that possible the .vo structure has been complicated. It is now made of 5 segments. | vo | vi | vi2vo | contents --------------+------+-----+-------+------------------------------------ lib | Yes | Yes | Yes | libstack (modules, notations,...) opauqe_univs | No | Yes | Yes | constraints coming from opaque proofs discharge | No | Yes | No | data needed to close sections tasks | No | Yes | No | STM tasks to produce proof terms opaque_proofs | Yes | Yes | Yes | proof terms --------------+------+-----+-------+------------------------------------ This means one can load only the strictly necessay parts. Usually one does not load the tasks segment of a .vi nor the opaque_proof segment of a .vo, unless one is turning a .vi into a .vo, in which case he load all the segments. Optional segments are marshalled as None. But for lib, all segments are Array.t of: | type --------------+--------------------------------------------------------- lib | a list of Libobject.obj (n'importe quoi) opauqe_univs | Univ.consraints Future.computation discharge | what Cooking.cook_constr needs tasks | Stm.tasks (a task is system_state * vernacexpr list) opaque_proofs | Term.constr Future.computation --------------+------+-----+-------+------------------------------------ Invariant: all Future.computation in a vo file (obtained by a vi2vo compilation or not) have been terminated with Future.join (or Future.sink). This means they are values (inside a box). This invariant does not hold for vi files. E.g. opauqe_proofs can be dangling Future.computation (i.e. NotHere exception). The vi2vo compilation step will replace them by true values. Rationale for opaque_univs: in the vi2vo transformation we want to reuse the lib segment. Hence the missing pieces have to be put on the side, not inside. Opaque proof terms are already in a separte segment. Universe constraints are not, hence the new opauqe_univs segment. Such segment, if present in a .vo file, is always loaded, and Declare.open_constant will add to the environment the constraints stored there. For regular constants this is not necessay since the constraints are already in their enclosing module (and also in the constant_body). With vi2vo the constraints coming from the proof are not in the constant_body (hence not in the enclosing module) but there and are added to the environment explicitly by Declare.open_constant. Rationale for discharge: vi2vo produces a proof term in its original context (in the middle of a section). Then it has to discharge the object. This segment contains the data that is needed in order to do so. It is morally the input that Lib.close_section passes to Cooking (via the insane rewinding of libstack, GlobalRecipe, etc chain). Checksums: the checksum of .vi and a .vo obtain from it is the same. This means that if if b.vo has been compiled using a.vi, and then a.vi is compiled into a.vo, Require Import b works (and recursively loads a.vo).
* Optimization in kernel/vars.ml: directly allocate a fixed-size block in theGravatar Pierre-Marie Pédrot2014-02-20
| | | | subst1 case.
* Made Pre_env.lazy_val opaque.Gravatar Pierre-Marie Pédrot2014-02-11
|
* Small optimizations in Closure:Gravatar Pierre-Marie Pédrot2014-02-09
| | | | | 1. Only apply last Zupdates 2. Better smartmap with state.
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Relaxing the sort elimination check to allow for let-bindings in arities.Gravatar Maxime Dénès2014-01-18
| | | | | | | I restored this in the kernel, and added it to the checker. There is one last source of non-uniformity, which is the Sort case in the checker (was not present in the kernel). I don't know what this case covers, so it should be reviewed.
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 19:45:12 +0000