aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
...
| | | * [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Emilio Jesus Gallego Arias2017-05-18
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | In non-interactive mode, `edit_at` seems to do very weird things, for instance will try to recompute all the previous states which seems weird. We better avoid that to approximate 8.6 behavior while we investigate more.
| | * [toplevel] Restore 8.6 goal printing behavior.Gravatar Emilio Jesus Gallego Arias2017-05-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When porting the toplevel to the STM, the logic for goal printing was simplified too much under optimistic assumptions. The idea was not to rely on the `vernac_classifier` which is an internal and complicated beast. However, it seems there are many cases to consider other than `is_query`, so at the risk of reimplementing the classifier we revert to the old approach of using the full classification. This gives maximum 8.6 compatibility, with the pitfall of having to call the classifier. Indeed, due to the dynamic nature of the "undo classifier", we cannot call it after `Stm.add`, as the document tree will be not the right one, making the classification of undo commands incorrect (actually raising an error "Cannot undo").
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
| |\ \ | | |/ | |/|
| | * Removing a variable warned unused.Gravatar Hugo Herbelin2017-05-14
| | |
| | * Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in ↵Gravatar Maxime Dénès2017-05-10
| | |\ | | | | | | | | | | | | "Print Assumptions".
| * | \ Merge PR#615: coqtop -help: don't die if coqlib can't be foundGravatar Maxime Dénès2017-05-09
| |\ \ \
| * | | | [toplevel] Fix a couple of logical errors in error printing.Gravatar Emilio Jesus Gallego Arias2017-05-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use exceptions for error printing. However a couple of mistakes were present in that commit: - We wrongly absorbed the exception on `Vernac.compile`. However, it should be propagated as the caller will correctly print the error now. This introduced a critical bug as now `coqc` return the wrong exit status on error, breaking all sort of things. - We printed parsing exceptions twice; now it is not necessary to print the exception in the parsing handler as it will be propagated. I've checked this commit versus all previously reported bugs and it seems to work; we should definitively add a test-suite case to check that the exit code of `coqc` is correct, plus several other cases such as bugs https://coq.inria.fr/bugs/show_bug.cgi?id=5467 https://coq.inria.fr/bugs/show_bug.cgi?id=5485 https://coq.inria.fr/bugs/show_bug.cgi?id=5484 etc... See also PR #583
| | | * | Fix bug #3659: -time should understand multibyte encodings.Gravatar Pierre-Marie Pédrot2017-05-05
| | | | | | | | | | | | | | | | | | | | | | | | | We assume Coq always outputs UTF-8 (is it really the case?) and cut strings after 30 UTF-8 characters instead of using the standard String function.
| | * | | coqtop -help: don't die if coqlib can't be foundGravatar Gaetan Gilbert2017-05-05
| |/ / /
| * | | Adding an option "Printing Unfocused".Gravatar Pierre Courtieu2017-05-04
| | | | | | | | | | | | | | | | | | | | | | | | Off by default. + small refactoring of emacs hacks in printer.ml.
| | | * FIx bug #5300: uncaught exception in "Print Assumptions".Gravatar Cyprien Mangin2017-05-03
| | |/
| * | Warning 29: non escaped end of line may be non portableGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | |
| * | [toplevel] Remove unused parameter from `Vernac.process_expr`.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | |
| * | [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a partial backtrack on 63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we disregarded exception and tried to print error messages just by listening to feedback. However, feedback error messages are not always emitted due to https://coq.inria.fr/bugs/show_bug.cgi?id=5479 Thus meanwhile it is safer to go back to printing the information present in exceptions until we tweak the STM. This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many other glitches not reported, such errors in nested proofs.
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | Now it is a private field, locations are optional.
| * | [toplevel] Don't check proofs in -quick mode.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | This fixes a logical error introduced in ce2b2058587224ade9261cd4127ef4f6e94d356b Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484
| * | [toplevel] Don't mask critical exceptions in vernac interpretation.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/ / | | | | | | | | | | | | | | | | Indeed we were not correctly backtracking in the case of StackOverflow. It makes sense to remove the inner handler which is a leftover of a previous attempt, and handle interpretation errors in load as non-recoverable. This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \
| * | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
* | | [toplevel] Fix printing of parsing errors + corner case.Gravatar Emilio Jesus Gallego Arias2017-04-19
|/ / | | | | | | | | | | | | | | | | | | | | | | | | PR #441 and #530 had an interesting interaction creating two bugs: - #441 stopped emitting feedback for the parser, however #530 changed the mechanism to print parser errors to the feedback, thus when the two patches were applied, parsing errors were not printed in batch_mode. - Additionally, #530 contains an error: prior to `Stm.init` we must take care of exceptions `require ()`/etc... otherwise they won't get printed.
| * Fixing bug #5470 (anomaly on notations with misused "binder" type).Gravatar Hugo Herbelin2017-04-14
| |
| * Fixing bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-04-14
| |
* | [toplevel] Don't print goals if there is no pending proof.Gravatar Emilio Jesus Gallego Arias2017-04-13
| |
* | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \
| * | [toplevel] [stm] cleanup in module openGravatar Emilio Jesus Gallego Arias2017-04-12
| | |
| * | [vernac] vernacentries.mli cleanupGravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | This header file had accumulated quite a bit of cruft over the years, we clean it up while we are at it. No functional change as all the removed variables/methods were noops long time ago.
| * | [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled.
* | | Merge PR#547: [toplevel] Remove the feedback printer only on exit.Gravatar Maxime Dénès2017-04-10
|\ \ \
| | * | [stm] remove process_error_hookGravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| | | | | | | | | | | `process_error_hook` seems unnecesary, we just call the proper error interpretation.
* | | Merge PR#461: [camlpX] Remove camlp4 compat layer.Gravatar Maxime Dénès2017-04-07
|\ \ \
| | * | [toplevel] Remove the feedback feeder printing only on exit.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| | | | | | | | | | | | | | This fixes the bug in `Drop` reported by @mattam82: after performing a `Drop`, the feeder was lost and no further message from Coq was printed.
* | | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Gravatar Matthieu Sozeau2017-04-07
| | |
| * | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
|/ / | | | | | | | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
| * Fix a few programming pearls related to Time, Fail and Redirect.Gravatar Maxime Dénès2017-04-06
| | | | | | | | | | | | | | | | | | This fixes a few clear bugs, but the STM code handling Time, Fail and Redirect before par: still needs to be rewritten. It does not implement the same semantics as the vernac interpreter for Fail Fail [c] and ignores Redirect. This commit was already reviewed with Enrico and tested on Travis.
| * Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| |\ | | | | | | | | | Was needed to be done for a while.
* | | [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429
* | | Merge PR#502: [pp] Add anomaly header to error messages.Gravatar Maxime Dénès2017-04-04
|\ \ \
| | * | Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
| | | |
* | | | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
| | | |
| * | | [pp] Add anomaly header to anomaly error messages.Gravatar Emilio Jesus Gallego Arias2017-03-22
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch restores the proper printing of anomalies in coqtop / coqc / coqide. Currently, they are printed with an `Error` header, whereas they should be printed with an `Anomaly" header. This reopens an unfinished debate started in #390 , about how to properly do "message" headers. Prior to #390, headers were handled inconsistently, sometimes, `Error` or `Anomaly` were added in `CErrors`, which lives below of the tagging system, thus some times we got no coloring (c.f. https://coq.inria.fr/bugs/show_bug.cgi?id=4789), but some other times the headers were added by the message handlers in Feedback. PR #390 takes the position of identifying the messages with the `Feedback.level` tag, and letting the backends to the tagging. This makes sense as the backends may want to interpret the "headers" in any way they'd like. For instance, instead of printing: `Error: foo` they may want to insert an image. Note that this implies that CoqIDE doesn't currently insert an error header on the first error case. This could be easily solved, but for anomalies we could do in any of the ways explained below. There are thus two natural ways to handle anomalies here: One is to tag them as errors, but add a text header, this is done now, with the small optimization in the case the handled has access to the exception itself. The second way is to add a new `Feedback.level` category and tag the anomalies appropriately. We would need also to modify Fail in this case, or to completely remove it from the protocol. I guess feedback from the rest of developers is needed before committing to a strategy, for now this patch should be good.
* | | Merge PR#390: Updates to the Pretty Printing InfrastructureGravatar Maxime Dénès2017-03-22
|\ \ \
* \ \ \ Merge PR#482: [toplevel] Remove unusable option -notopGravatar Maxime Dénès2017-03-22
|\ \ \ \
| | * | | [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`.
| | * | | [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For legacy reasons, pretty printing required to provide a "tag" interpretation function `pp_tag`. However such function was not of much use as the backends (richpp and terminal) hooked at the `Format.tag` level. We thus remove this unused indirection layer and annotate expressions with their `Format` tags. This is a step towards moving the last bit of terminal code out of the core system.
| | * | | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent.
| | * | | [error] Move back fatal_error to toplevelGravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09 (the mllib dependencies that should be surely tweaked more). The logic for `fatal_error` has no place in `CErrors`, this is coqtop-specific code. What is more, a libobject caller should handle the exception correctly, I fail to see why the fix was needed on the first place.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 10:47:26 +0000