aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* 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
* Minor cleanup concerning Mod_subst.MBImapGravatar letouzey2013-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
| | | | | | Very little space saved this way, but it would hurt either... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing mandatory suffixes for library files.Gravatar ppedrot2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: simplify a bit its exception handlerGravatar letouzey2013-03-17
| | | | | | | | We use Errors.print for anomalies and other uncaught exceptions in the checker: this should print the same message, it is shorter this way, and we avoid using Errors.is_anomaly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation of coqchk (broken by commit 16268), bis repetitaGravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation of coqchk (broken by commit 16268)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 2)Gravatar letouzey2013-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16277 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
| | | | | | | | | | | | | | | | | | | | | | | | | | Why? : avoid catching (and probably ignoring) exceptions such as Sys.Break, anomalies, assertions, leading to undetected bugs and ignored Ctrl-C. How? : when the precise exception(s) concerned by the try is known, use them explicitely in the "with". Otherwise, let's use the pattern "with e when Errors.noncritical e -> " Particular case : when an exception is catched and reraised immediately after some adjustments, we leave it untouched. Simply, for easily identifying these situations later, the name of the exception variable is changed to "reraise". Please also adopt this coding style. Automatic checks based on the "mascot" tool of X. Clerc will be runned regularly. If you want to avoid to check a particular try...with, use the variable name "any" after the "with". All these changes have been tested using the standard library and the test-suite, but unfortunately this is far from ensuring that coqtop behaves as before. We'll see after the nightly bench... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphization.Gravatar ppedrot2013-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dir_path --> DirPathGravatar letouzey2013-02-19
| | | | | | | | Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
| | | | | | | | | - a module KernelPair for improving sharing between constant and mind - shorter representation than a pair when possible - exports comparisions on constant and mind and ... - a kn_equal function instead of Int.equal (kn_ord ...) 0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing Exc_located and using the new exception enrichementGravatar ppedrot2013-02-18
| | | | | | mechanism to retrieve the same information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added exception enrichment. Now one can define additional arbitraryGravatar ppedrot2013-02-18
| | | | | | | | | | | information worn by exceptions. The implementation is quite hackish but it should work nonetheless. Basically, it adds an additional cell to exceptions arguments, in which you can put whatever you want. By typing invariants, you may not reach this cell by normal means, so it should be safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
* make validate repaired via a temporary fix for #2949Gravatar letouzey2013-02-13
| | | | | | | | | | The offending functor in NZOrder wasn't actually used, so I've commented it for now. Btw, the Not_found in coqchk is now turned into something slightly more informative git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: re-sync vo structures after Maxime's commit 16136Gravatar letouzey2013-02-12
| | | | | | | make validate still fails, but that's another issue (#2949) we're still working on... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing coqchk compilation after commit r16183Gravatar ppedrot2013-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added backtrace primitives.Gravatar ppedrot2013-01-28
| | | | | | | | | | | | | | | | | | | | | | Using OCaml 3.11+ builtin facilities to record stack frames during exception raising, we can now recover at runtime the backtrace of an uncaught toplevel exception and display it to the user, without the infamous OCaml debugger. The backtrace is displayed when using the [-debug] flag. This requires a bit of discipline, as each time we reraise an exception we need to keep track of those frames we discarded between the previous raise and the current [try-with] branch. Currently, only [Anomaly] is handled, but this can be ported to any exception as long as we add the backtrace info into the exception, and we provide the corresponding handler to [Backtracke.register_backtrace_handler]. Hopefully this should not be to costly, as we only do little work when reraising, and only with the [-debug] flag set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added backtrace information to anomaliesGravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Array.create is deprecatedGravatar pboutill2012-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of LabelGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of dir_pathGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning and small optimization in CList.Gravatar ppedrot2012-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a CString module.Gravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an Int module with dummy utility functions.Gravatar ppedrot2012-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15956 85f007b7-540e-0410-9357-904b9bb8a0f7
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
* still some more dead code removalGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Compat in the checker.Gravatar ppedrot2012-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15849 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 19:58:51 +0000