aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Merge PR #6277: Qualified import in coqchkGravatar Maxime Dénès2017-12-07
|\
* \ Merge PR #6266: Safe unmarshalling in the checkerGravatar Maxime Dénès2017-12-05
|\ \
| | * Forbid implicitly relative names in the checker.Gravatar Pierre-Marie Pédrot2017-11-29
| |/ |/| | | | | | | | | | | | | | | | | Before this patch, passing a mere identifier (without dots) to the checker would make it consider it as implicitly referring to a relative name. For instance, if passed "foo", it would have looked for "Bar.foo.vo" and "Qux.foo.vo" if those files were in the loadpath. This was quite ad-hoc. We remove this "feature" and require the user to always give either a filename or a fully qualified logical name.
* | Allow to pass physical files to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
| |
* | Adding an interface file for checker/check.ml.Gravatar Pierre-Marie Pédrot2017-11-28
| |
| * Use safe demarshalling in the checker.Gravatar Pierre-Marie Pédrot2017-11-28
|/ | | | | | Instead of relying on the OCaml demarshaller, which is not resilient against ill-formed data, we reuse the safe demarshaller from votour. This ensures that garbage files do not trigger memory violations.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | Suggested by @ppedrot
* | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
| * [checker] Fix/fine tune printing.Gravatar Emilio Jesus Gallego Arias2016-08-18
|/ | | | | | | | | | | | | | | | | | | | | In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct access to the console, recommending instead to provide information to the user by means of the `Feedback.msg_*` facilities. However, we introduced a display bug in the checker printer as it is special and doesn't use the Pp facilities (likely for trust reasons), spotted by @herbelin This patch fixes this bug and performs a couple more of fine tunings in the input. However, it could be desirable to port the `checker/printer.ml` to `Pp` and use the feedback mechanism; this would allow IDEs to use the checker in a more convenient way, at the cost of trusting `Pp` (which is already a bit trusted currently) A start of that idea can be found at: https://github.com/ejgallego/coq/tree/fix_checker_printing
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\
| * Fix incorrect checking of library checksums.Gravatar Maxime Dénès2016-06-05
| | | | | | | | | | | | Since d09def34, only the summary of libraries was included in the checksum, not the actual content of the library. This quick fix performs the checking of the checksum immediately, even if the loading is delayed.
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/ | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
| | | | proofs.
* Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
| | | | | | There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures.
* On-demand Require.Gravatar Pierre-Marie Pédrot2015-06-24
| | | | | | Marshalled libraries are only loaded when needed and dropped thereafter. This might be costly for Require inside modules, but such a practice is discouraged anyway.
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
| | | | | The first part only contains the summary of the library, while the second one contains the effective content of it.
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Fix sigsegv in checkerGravatar Enrico Tassi2014-12-19
|
* 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).
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
|
* .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
* 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
* 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
* 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: 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 23:33:49 +0000