aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* Merge remote-tracking branch 'github/pr/257' into v8.6Gravatar Maxime Dénès2016-09-30
|\ | | | | | | Was PR#257: [checker] Fix/fine tune printing.
* | fix bug 3683 : adds references to the web site for the bug trackerGravatar Yves Bertot2016-09-29
| | | | | | | | in error messages
| * [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
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\
| * Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
| |
* | 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
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
| * Remove extraction-specific code from the checker.Gravatar Guillaume Melquiond2016-06-23
| | | | | | | | | | | | It seems like this code was copy-pasted from kernel/inductive.ml. It was already dubious enough in the kernel. It feels completely wrong in the checker.
* | Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-18
| | | | | | | | | | | | | | I had to remove code handling the -type-in-type option introduced by commit 9c732a5. We should fix it at some point, but I am not sure that using the checker with a system known to be blatantly inconsistent makes much sense anyway.
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | | | | | | | | | | | | | | This is a stupid fix that only allows to take into account the change in memory layout. The check will simply fail when encountering a unguarded inductive or (co)fixpoint.
* | | Preventive compatibility fixes for flushing.Gravatar Emilio Jesus Gallego Arias2016-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In pre 8.6, `Pp` provided its own reimplementation of `Pervasives.flush_all`, with different semantics. Unfortunately, with the removal of `Pp.flush_all` in #179, a couple of points were silently switched to the `Pervasives` version, which may lead to some subtle printing differences. As a preventive measure, we restore the same semantics for these parts of the codebase. Note that we don't re-introduce Coq's `flush_all` for several reasons: - Consumers of the logging API should not mess with flushing and Formatters as this is backend dependent (i.e: when in IDEs). Use of `Format` should be fully encapsulated if we want some hope of IDEs taking full control. - As used, the old semantics of `flush_all` were fragile.
* | | configure: use ln on linux and cp on windowsGravatar Enrico Tassi2016-06-14
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ | | |/ | |/|
| * | Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).Gravatar Guillaume Melquiond2016-06-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The COQLIBS variable contains some -Q and -I options, which are not supported by the checker. So this commit introduces a COQCHKLIBS variable that contains the proper options for coqchk. For the sake of homogeneity, the COQDOCLIBS variable is also preprocessed in the same way. This means that both variables have the same value, but they are kept separate in case the user would like to override one and not the other. This commit also removes some deprecated options from "coqchk --help". They are not removed from coqchk itself to preserve backward compatibility in the branch. An open question is whether coqchk should support dummy options such as -Q (interpreted as -R) or -I (ignored).
| * | 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.
* | | Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
|\ \ \
| * | | Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Coqdep_boot has almost no dependencies, and hence can be compiled very early during the build, without relying on .ml.d files. Some code of system.ml is now in a separate file minisys.ml, which is also included in system.ml for compatibility.
* | | | 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.
* | | Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
| | |
* | | Checker: no more -I kernel via a few symlinks (for Names and Esubst)Gravatar Pierre Letouzey2016-05-31
| | | | | | | | | | | | | | | | | | | | | In particular, no more warning about ocamldep finding stuff both in checker/ and kernel/. A 'make clean' is mandatory after this commit
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Make votour a bit more robust/forgiving with respect to user commands (bug ↵Gravatar Guillaume Melquiond2016-05-02
| | | | | | | | | | | | #4702).
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\| |
| * | Fix missing newline in coqchk engagement (bug #4694).Gravatar Guillaume Melquiond2016-04-28
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\| |
| * | A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
| | | | | | | | | | | | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
* | | Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\| |
| * | Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
| | | | | | | | | | | | Fixes compilation of Coq with OCaml 4.03 beta 1.
* | | CLEANUP: Simplifying the changes done in "checker/*"Gravatar Matej Kosik2016-02-15
| | |
* | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update cic.mli MD5 after header update.Gravatar Maxime Dénès2016-01-20
| | |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
* | | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
| | |
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\| | | | | | | | | | | | | | Conflicts: lib/cSig.mli
| * | Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
| | | | | | | | | | | | | | | | | | The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps.
| * | Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
| | | | | | | | | | | | | | | | | | | | | | | | CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places.
* | | Remove unused function Checker.print_loc.Gravatar Guillaume Melquiond2015-12-31
| | | | | | | | | | | | There is no location to print anyway, so it will never be useful.
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
| | | | | | | | | | | | | | | | | | For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read.
* | | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
| | |
* | | Displaying the object identifier in votour.Gravatar Pierre-Marie Pédrot2015-11-15
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\| |
| * | Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
| | | | | | | | | | | | proofs.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\| |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\ \ \
| | * | Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02
| | | |