aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Missing equalities in Names-like structures.Gravatar Pierre-Marie Pédrot2014-03-20
|
* STM: make -async-proofs on work from coqc tooGravatar Enrico Tassi2014-03-18
|
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
| | | | no particular purpose.
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
| | | | | | | | | | | | | | | | | | Universes that are computed in the vi2vo step are not part of the outermost module stocked in the vo file. They are part of the Library.seg_univ segment and are hence added to the safe env when the vo file is loaded. The seg_univ has been augmented. It is now: - an array of universe constraints, one for each constant whose opaque body was computed in the vi2vo phase. This is useful only to print the constants (and its associated constraints). - a union of all the constraints that come from proofs generated in the vi2vo phase. This is morally the missing bits in the toplevel module body stocked in the vo file, and is there to ease the loading of a .vo file (obtained from a .vi file). - a boolean, false if the file is incomplete (.vi) and true if it is complete (.vo obtained via vi2vo).
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
|
* Fix lookup of native files when option -R is missing.Gravatar Guillaume Melquiond2014-03-07
| | | | | | | | | | Testcase: mkdir a echo "Definition t := O." > a/a.v coqc -R a a a/a.v echo "Require Import a.a. Definition u := t." > b.v coqc -I . b.v rm -rf a b.*
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Goptions do not rely anymore on generic equality.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
|
* Fixing a Pervasive.compare.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Library: when compiling multiple files, reset the opaque tablesGravatar Enrico Tassi2014-02-26
| | | | | That was a bug. coqc a b was generating (for b) an opaque table containing also the proofs of a.
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
| | | | | Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
* 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).
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
|
* STM: modules do not prevent proofs from being ASyncGravatar Enrico Tassi2014-01-05
|
* coqtop: -check-vi-tasks and -schedule-vi-checkingGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2, in this precise order, stored in a.vi. The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi and .{a,b,c}.aux and spits 4 command lines to check all the tasks in {a,b,c}.vi trying to equally partition the job between the 4 workers, that can indeed be run in parallel. The aux file contains the time that it took to check the proofs stored in the .vi files last time the file was fully checked. This user interface is still very rough, it should probably run the workers instead of just printing their command line.
* .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
* 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.
* Patch for supporting [From Xxx Require Yyy Zzz.]Gravatar Gregory Malecha2013-12-12
| | | | | | | | | | | | When using libraries I find it convenient (and future proof) to use fully qualified paths in many places. It would be nice to have a convenient short-hand for this so that you can: From Xxx Require Yyy Zzz. instead of having to type: Require Xxx.Yyy Xxx.Zzz. Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
* Print logical name rather than path (thus allowing reproducible tests).Gravatar xclerc2013-12-02
|
* Better implementation of summary unfreezing.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Using hashes in Summary, like the previous commit did with Dyn.Gravatar Pierre-Marie Pédrot2013-11-22
|
* 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.
* 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
* Partial application in Globnames.Gravatar ppedrot2013-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17066 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
* 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 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
* 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.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
* 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
* 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
* Summary: if an unfreeze function fails, print an error messageGravatar gareuselesinge2013-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minimal implementation of `Shallow marshalling of LibGravatar gareuselesinge2013-09-12
| | | | | | Just sufficient to make abstract work in such an (empty) lib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16772 85f007b7-540e-0410-9357-904b9bb8a0f7
* summary for ML modules made correctGravatar gareuselesinge2013-08-30
| | | | | | | | | This summary entry is special because its unfreeze may load ML code that in turns adds summary entries. Hence it is the first summary piece to be unfreezed, otherwise some summaries may get lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16752 85f007b7-540e-0410-9357-904b9bb8a0f7
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
| | | | | | | | | | | | | | If a constant is defined as transparent, not only its side effects (opaque sub proofs as in abstract, and transparent ind schemes) are declared globally, but the ones that are schemes are also declared as such. The only sub optimal thing is that the code handling in a special way the side effects of transparent constants is in declare.ml that does not see ind_tables.ml, hence a forward ref to a function is used. IMO, ind_tables has no reason to stay in toplevel/. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
* recdef: restore old semantics (pre STM)Gravatar gareuselesinge2013-08-30
| | | | | | | | 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
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
| | | | | | | | | | The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
| | | | | | | | | | | Since digests are strings (of size 16), we just dump them now in vo files (cf. Digest.output) instead of using Marshal on them : this is cleaner and saves a few bytes. Increased VOMAGIC to clearly identify this change in the format. Please rerun ./configure after this commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The earlier type [struct_expr_body] was far too broad, leading to code with unclear invariants, many "assert false", etc etc. Its replacement [module_alg_expr] has only three constructors: * MEident * MEapply : note the module_path as 2nd arg, no more constraints here * MEwith : no more constant_body inside, constr is just fine But no more SEBfunctor or SEBstruct constructor here (see below). This way, this datatype corresponds to algebraic expressions, i.e. anything that can appear in non-interactive modules. In fact, it even coincides now with [Entries.module_struct_entry]. - Functor constructors are now necessarily on top of other structures thanks to a generic [functorize] datatype. - Structures are now separated from algebraic expressions by design : the [mod_type] and [typ_expr] fields now only contain structures (or functorized structures), while [mod_type_alg] and [typ_expr_alg] are restricted to algebraic expressions only. - Only the implementation field [mod_expr] could be either algebraic or structural. We handle this via a specialized datatype [module_implementation] with four constructors: * Abstract : no implementation (cf. for instance Declare Module) * Algebraic(_) : for non-interactive modules, e.g. Module M := N. * Struct(_) : for interactive module, e.g. Module M : T. ... End M. * FullStruct : for interactive module with no type restriction. The [FullStruct] is a particular case of [Struct] where the implementation need not be stored at all, since it is exactly equal to its expanded type present in [mod_type]. This is less fragile than hoping as earlier that pointer equality between [mod_type] and [mod_expr] will be preserved... - We clearly emphasize that only [mod_type] and [typ_expr] are relevant for the kernel, while [mod_type_alg] and [typ_expr_alg] are there only for a nicer extraction and shorter module printing. [mod_expr] is also not accessed by the kernel, but it is important for Print Assumptions later. - A few implicit invariants remain, for instance "no MEwith in mod_expr", see the final comment in Declarations - Heavy refactoring of module-related files : modops, mod_typing, safe_typing, declaremods, extraction/extract_env.ml ... - Coqchk has been adapted accordingly. The code concerning MEwith in Mod_checking is now gone, since we cannot have any in mod_expr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_typing code refactoringGravatar letouzey2013-08-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - No more modinfo sub-record in the safe_environment record, this was a syntactic pain. senv.modinfo.modpath --> senv.modpath senv.modinfo.variant --> senv.modvariant senv.modinfo.resolver --> senv.modresolver senv.modinfo.resolver_of_param --> senv.paramresolver senv.modinfo.label : removed (can be inferred from modpath) - No more systematic chaining of safe_environment ('old' field). Instead, earlier safe_environment is stored in the modvariant field when necessary (STRUCT and SIG case). - Improved sharing between end_module and end_modtype - More qualified names instead of open, better comments, ... - Some user errors are now checked earlier elsewhere (see for instance vernac_end_segment), so we can turn these errors into asserts. The user error about higher-order include is now algebraic. - Highlight the idea of a state monad in Safe_typing : type 'a safe_transformer = safe_environment -> 'a * safe_environment More systematic code in Global, thanks to 'globalize' function. - Declaremods : less informations stored in openmod_info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16708 85f007b7-540e-0410-9357-904b9bb8a0f7
* abstract+Defined: create opaque sub proofs (as pre-ParalITP)Gravatar gareuselesinge2013-08-19
| | | | | | | | | | | | | | | Non-opaque-constant's side effects are processed before the constant enters the kernel and global constants are generated for them (as before, but not by side effect in the middle of the proof construction). This makes sense because proofs ending with Defined have to be run immediately, so the list of side effects is immediately available. These side effects are type checked again. To fix that the idea of kernel signatures could be employed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16702 85f007b7-540e-0410-9357-904b9bb8a0f7
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
| | | | | | | | | It can be: `Yes Full data, in a state that can be marshalled `No Full data, good for Undo only `Shallow Partial data, marshallable, good for slave processes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simple machinery to detect EXTEND that interpret during parsingGravatar gareuselesinge2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 85f007b7-540e-0410-9357-904b9bb8a0f7
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 10:31:40 +0000