aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* 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).
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
| | | | (hopefully), and forbids generic equality. Still, it allows generic hash.
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
| | | | | | | | | | | the provided type to come with a hashing function. The internal representation is changed, such that values are first compared w.r.t. to their hash. This effectively saves a lot of comparisons which may be far more expensive than O(1), as in the string case, hence resulting in an overall speedup. CAVEAT: everything is not implemented yet, and order-sensitive functions now do not respect the provided order anymore.
* 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.
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
|
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
|
* votour: better error messagesGravatar Enrico Tassi2014-02-26
|
* checker: less useless error messagesGravatar Enrico Tassi2014-02-26
|
* fix checker w.r.t. mutual_inductive_body and constant_bodyGravatar Enrico Tassi2014-02-26
| | | | discrepancy introduced in commit d3eac3d5fc8e5af499eb8750ca08ead8562dac6f
* fix checker w.r.t. Dyn.t validationGravatar Enrico Tassi2014-02-26
| | | | discrepancy introduced in commit 400327165edcba667ebb70ebb89052455656b719
* Fixing checker compilation, which was broken by the following commit:Gravatar Pierre-Marie Pédrot2014-01-19
| | | | 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
* 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
|
* .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
* 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
* Get rid of polymorphic equality in "checker/subtyping.ml".Gravatar xclerc2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16926 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.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
* 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
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
| | | | | | removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 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
* Adding dynamic value printing to votour through a registering mechanism.Gravatar ppedrot2013-08-23
| | | | | | TODO: register the desired dynamic types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16733 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
| | | | | | | | | | | | | | | | | | | - Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 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
* Fixing votourGravatar ppedrot2013-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation of coqcheckGravatar gareuselesinge2013-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16716 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
* Repair coqcheck : constant_body constraints are also futureGravatar letouzey2013-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16706 85f007b7-540e-0410-9357-904b9bb8a0f7
* checker validation fixed w.r.t. FuturesGravatar gareuselesinge2013-08-09
| | | | | | | still not working, it complains about the universe constraint set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16691 85f007b7-540e-0410-9357-904b9bb8a0f7
* checker validation made a bit more verboseGravatar gareuselesinge2013-08-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16690 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
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | | | | When refering to a module / module type, or when doing an include, we do not duplicate and substitution original libobjects immediatly. Instead, we store the module path, plus a substitution. The libobjects are retrieved later from this module path and substituted, typically during a Require. This allows to vastly decrease vo size (up to 50% on some files in the stdlib). More work is done during load (some substitutions), but the extra time overhead appears to be negligible. Beware: all subst_function operations should now be environment-insensitive, since they may be arbitrarily delayed. Apparently only subst_arguments_scope had to be adapted. A few more remarks: - Increased code factorisation between modules and modtypes - Many errors and anomaly are now assert - One hack : brutal access of inner parts of module types (cf handle_missing_substobjs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a generic notion of hook. Hooks are functions to be setGravatar ppedrot2013-05-12
| | | | | | | exactly once at runtime, often to reduce the mutual dependency of modules. This module permits to track them more easily. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
| | | | | | it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove deprecated option -no-hash-consing (currently doing nothing)Gravatar letouzey2013-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: vo validation checks the absence of Var/Evar/MetaGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker : a md5-based way to ensure checker/values.ml is always in syncGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16404 85f007b7-540e-0410-9357-904b9bb8a0f7
* votour: a small tool for guided tours of .voGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: vo validation is now done in check.ml (and always)Gravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: get rid of code handling section variablesGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: empty sections hardcoded in cb and mindGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: reified encoding of .vo types in values.mlGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Get rid of the LightenLibrary hack : no more last-minute collect of opaque terms and Obj.magic tricks. Instead, we make coqc accumulate the opaque terms as soon as constant_bodies are created outside sections. In these cases, the opaque terms are placed in a special table, and some (DirPath.t * int) are used as indexes in constant_body. In an interactive session, the local opaque terms stay directly stored in the constant_body. The structure of .vo file stays similar : magic number, regular library structure, digest of the first part, array of opaque terms. In addition, we now have a final checksum for checking the integrity of the whole .vo file. The other difference is that lazy_constr aren't changed into int indexes in .vo files, but are now coded as (substitution list * DirPath.t * int). In particular this approach allows to refer to opaque terms from another library. This (and accumulating substitutions in lazy_constr) seems to greatly help decreasing the size of opaque tables : -20% of vo size on the standard library :-). The compilation times are slightly better, but that can be statistic noise. The -force-load-proofs isn't active anymore : it behaves now just like -lazy-load-proofs. The -dont-load-proofs mode has slightly changed : opaque terms aren't seen as axioms anymore, but accessing their bodies will raise an error. Btw, API change : Declareops.body_of_constant now produces directly a constr option instead of a constr_substituted option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst.force: avoid using join when only one substGravatar letouzey2013-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16381 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 13:55:25 +0000