aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/checker.ml
Commit message (Collapse)AuthorAge
* Merge PR #1075: Re-enable checker error messagesGravatar Maxime Dénès2017-09-25
|\
| * Adapt checker to change in locations.Gravatar Maxime Dénès2017-09-21
| |
| * [checker] Add missing Feedback printer (BZ#5587)Gravatar Emilio Jesus Gallego Arias2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes longstanding bug likely introduced in the first `pp` to `Feedback` migration, namely the checker didn't register a feedback printer, thus no calls to `Feedback.msg_*` were printed in the checker. This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587 We fix this by adding a custom printer to the checker, this is correct as the checker owns now the full console, however a cleanup should happen in any of these two directions: - all the calls to feedback are removed, and the checker always uses its own printing mechanism. - all the calls to `Format/Printf` are removed and the checker always uses the `Feedback` mechanism. Currently, I have no opinion on this.
* | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/ | | | | | | | | | | An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info`
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [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.
* Remove uses of [Flags.make_silent]Gravatar Gaetan Gilbert2017-04-27
|
* Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
|
* 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
* | | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ / | | | | | | Suggested by @ppedrot
| * [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
* 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 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).
* | 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
| |
* | Remove unused function Checker.print_loc.Gravatar Guillaume Melquiond2015-12-31
|/ | | | There is no location to print anyway, so it will never be useful.
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| | | | | | | | | | in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk?
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| | | | | | Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
|
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
| | | | This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
|
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
| | | | | | | In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Exit with code 129 when an anomaly occurs.Gravatar Xavier Clerc2014-11-14
|
* Removing explanations of universe inconsistencies from the checker. TheyGravatar Pierre-Marie Pédrot2014-06-10
| | | | were never used and were responsible for code duplication.
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
|
* printer for coqchkGravatar Enrico Tassi2014-04-08
|
* Printing backtraces in coqchk while in debug mode.Gravatar Pierre-Marie Pédrot2014-03-18
|
* checker: less useless error messagesGravatar Enrico Tassi2014-02-26
|
* 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
* 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: 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-17 21:21:41 +0000