aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\
* \ Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\ \
* | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | |
| * | Remove uses of [Flags.make_silent]Gravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
|/ /
| * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/ | | | Also remove obvious comments.
* [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself.
* Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
| | | | | | | Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\
| * 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
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
| * | | 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.
| * | | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
| | * [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
* / remove checker/MakefileGravatar Pierre Letouzey2016-07-26
|/ | | | | | This historical Makefile was used during the development of coqcheck, but was unused since then : the checker is built via Coq's main Makefile. So let's remove this one to avoid any risk of confusion.
* 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.