aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
|\
* | [pp] Hide the internal representation of `std_ppcmds`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | Following a suggestion by @ppedrot in #390, we require `Pp` clients to be aware that they are using a "view" on the `std_ppcmds` type. This is not extremely useful as people caring about the documents will indeed have to follow changes in the view, but it costs little to play on the safe side here for now. We also introduce a more standard notation, `Pp.t` for the main type.
* | [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics.
* | [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] Debug feeder is not needed anymore.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | -> Candidate to be merge with the main feedback commit.
* | [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.
* | [feedback] Allow to remove feedback listeners.Gravatar Emilio Jesus Gallego Arias2017-03-21
| |
* | [pp] Remove redundant white spacing pp construct.Gravatar Emilio Jesus Gallego Arias2017-03-21
| |
* | [pp] Force well-formed boxes by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | We replace open/close box commands in favor of the create box ones.
* | [pp] Force well-tagged docs by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | We replace open/close tag commands by a well-balanced "tag" wrapper.
* | [pp] Implement n-ary glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| |
* | [pp] Make pp public to allow serialization.Gravatar Emilio Jesus Gallego Arias2017-03-21
| |
* | [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
* | [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | Mostly unused, we ought to limit spacing in the boxes themselves.
* | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags.
* | Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
|\ \
| | * [future] Use eager evaluation for chaining values.Gravatar Emilio Jesus Gallego Arias2017-03-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The current future system is lazy when "chaining" (*) a resolved future, which implies that chaining with a resolved future will produce a non-resolved one. This misfeature interacts badly with the "purification" optimization, which in turn provokes a swarm of spurious state setting calls in real use. To solve this problem, we revert to the more natural semantics of respecting the evaluation semantics when mapping over a future, indeed respecting the previous resolution status. This commit solves a kind of _critical_ bug in the current system, with the particular bad path origination in `Future.split2` due to the following accumulation of circumstances: ``` split2 x -> chain x (fun x -> fst x) => let y = chain ~pure x (fun x -> fst x) in if is_over x && greedy then ignore(force ~pure y); y => [y <- Closure (fun x -> fst x)] ignore(force (Closure (fun x -> fst x))) => purify_future (force ~pure) (Closure (fun x -> fst x)) ``` and then, the test in `purify_future` fails, triggering the spurious state reset operation. This problem was first noted at https://sympa.inria.fr/sympa/arc/coqdev/2016-02/msg00081.html , and seems related to https://coq.inria.fr/bugs/show_bug.cgi?id=5382 We fix the problem by making chaining eager, but other solutions would be possible. Given that the main user of `chain` is `split2` which does `snd/fst`, I recommend this solution. The difference in calls to `unfreeze_state` is dramatic: ``` | File | Freeze Calls After | Freeze Calls Before | |----------------------------------------+--------------------+---------------------| | theories/Init/Notations.v | 0 | 0 | | theories/Init/Logic.v | 57 | 614 | | theories/Init/Datatypes.v | 13 | 132 | | theories/Init/Logic_Type.v | 7 | 57 | | theories/Init/Specif.v | 5 | 35 | | theories/Init/Nat.v | 0 | 0 | | theories/Init/Peano.v | 22 | 264 | | theories/Init/Wf.v | 8 | 89 | | theories/Init/Tactics.v | 2 | 24 | | theories/Init/Tauto.v | 0 | 0 | | theories/Init/Prelude.v | 0 | 0 | | Bool/Bool.v | 104 | 1220 | | Program/Basics.v | 0 | 0 | | Classes/Init.v | 0 | 0 | | Program/Tactics.v | 0 | 0 | | Relations/Relation_Definitions.v | 0 | 0 | | Classes/RelationClasses.v | 21 | 341 | | Classes/Morphisms.v | 47 | 689 | | Classes/CRelationClasses.v | 18 | 245 | | Classes/CMorphisms.v | 50 | 587 | | Classes/Morphisms_Prop.v | 3 | 127 | | Classes/Equivalence.v | 6 | 105 | | Classes/SetoidTactics.v | 0 | 0 | | Setoids/Setoid.v | 4 | 33 | | Structures/Equalities.v | 8 | 93 | | Relations/Relation_Operators.v | 0 | 0 | | Relations/Operators_Properties.v | 35 | 627 | | Relations/Relations.v | 2 | 24 | | Structures/Orders.v | 12 | 148 | | Numbers/NumPrelude.v | 0 | 0 | | Structures/OrdersTac.v | 13 | 234 | | Structures/OrdersFacts.v | 73 | 931 | | Structures/GenericMinMax.v | 82 | 1294 | | Numbers/NatInt/NZAxioms.v | 0 | 0 | | Numbers/NatInt/NZBase.v | 7 | 87 | | Numbers/NatInt/NZAdd.v | 14 | 168 | | Numbers/NatInt/NZMul.v | 12 | 144 | | Logic/Decidable.v | 28 | 336 | | Numbers/NatInt/NZOrder.v | 81 | 1174 | | Numbers/NatInt/NZAddOrder.v | 24 | 288 | | Numbers/NatInt/NZMulOrder.v | 46 | 552 | | Numbers/NatInt/NZParity.v | 35 | 420 | | Numbers/NatInt/NZPow.v | 29 | 348 | | Numbers/NatInt/NZSqrt.v | 54 | 673 | | Numbers/NatInt/NZLog.v | 64 | 797 | | Numbers/NatInt/NZDiv.v | 49 | 588 | | Numbers/NatInt/NZGcd.v | 36 | 432 | | Numbers/NatInt/NZBits.v | 0 | 0 | | Numbers/Natural/Abstract/NAxioms.v | 0 | 0 | | Numbers/NatInt/NZProperties.v | 0 | 0 | | Numbers/Natural/Abstract/NBase.v | 14 | 177 | | Numbers/Natural/Abstract/NAdd.v | 6 | 72 | | Numbers/Natural/Abstract/NOrder.v | 29 | 349 | | Numbers/Natural/Abstract/NAddOrder.v | 5 | 60 | | Numbers/Natural/Abstract/NMulOrder.v | 8 | 96 | | Numbers/Natural/Abstract/NSub.v | 36 | 432 | | Numbers/Natural/Abstract/NMaxMin.v | 18 | 216 | | Numbers/Natural/Abstract/NParity.v | 4 | 48 | | Numbers/Natural/Abstract/NPow.v | 26 | 312 | | Numbers/Natural/Abstract/NSqrt.v | 9 | 108 | | Numbers/Natural/Abstract/NLog.v | 0 | 0 | | Numbers/Natural/Abstract/NDiv.v | 50 | 600 | | Numbers/Natural/Abstract/NGcd.v | 14 | 168 | | Numbers/Natural/Abstract/NLcm.v | 29 | 348 | | Numbers/Natural/Abstract/NBits.v | 168 | 2016 | | Numbers/Natural/Abstract/NProperties.v | 0 | 0 | | Arith/PeanoNat.v | 77 | 990 | | Arith/Le.v | 2 | 57 | | Arith/Lt.v | 14 | 168 | | Arith/Plus.v | 20 | 269 | | Arith/Gt.v | 17 | 248 | | Arith/Minus.v | 11 | 132 | | Arith/Mult.v | 14 | 168 | | Arith/Between.v | 19 | 299 | | Logic/EqdepFacts.v | 26 | 539 | | Logic/Eqdep_dec.v | 13 | 361 | | Arith/Peano_dec.v | 3 | 26 | | Arith/Compare_dec.v | 35 | 360 | | Arith/Factorial.v | 3 | 36 | | Arith/EqNat.v | 10 | 111 | | Arith/Wf_nat.v | 18 | 173 | | Arith/Arith_base.v | 0 | 0 | | Numbers/BinNums.v | 0 | 0 | | PArith/BinPosDef.v | 0 | 0 | | PArith/BinPos.v | 229 | 2810 | | NArith/BinNatDef.v | 0 | 0 | | NArith/BinNat.v | 107 | 1330 | | PArith/Pnat.v | 51 | 688 | | NArith/Nnat.v | 30 | 360 | | setoid_ring/Ring_theory.v | 43 | 756 | | Lists/List.v | 195 | 2908 | | setoid_ring/BinList.v | 6 | 90 | | Numbers/Integer/Abstract/ZAxioms.v | 0 | 0 | | Numbers/Integer/Abstract/ZBase.v | 3 | 36 | | Numbers/Integer/Abstract/ZAdd.v | 46 | 552 | | Numbers/Integer/Abstract/ZMul.v | 8 | 96 | | Numbers/Integer/Abstract/ZLt.v | 21 | 252 | | Numbers/Integer/Abstract/ZAddOrder.v | 45 | 543 | | Numbers/Integer/Abstract/ZMulOrder.v | 24 | 288 | | Numbers/Integer/Abstract/ZMaxMin.v | 22 | 264 | | Numbers/Integer/Abstract/ZSgnAbs.v | 41 | 492 | | Numbers/Integer/Abstract/ZParity.v | 6 | 72 | | Numbers/Integer/Abstract/ZPow.v | 10 | 120 | | Numbers/Integer/Abstract/ZDivTrunc.v | 68 | 816 | | Numbers/Integer/Abstract/ZDivFloor.v | 70 | 840 | | Numbers/Integer/Abstract/ZGcd.v | 29 | 348 | | Numbers/Integer/Abstract/ZLcm.v | 50 | 600 | | Numbers/Integer/Abstract/ZBits.v | 205 | 2460 | | Numbers/Integer/Abstract/ZProperties.v | 0 | 0 | | ZArith/BinIntDef.v | 0 | 0 | | ZArith/BinInt.v | 212 | 2839 | |----------------------------------------+--------------------+---------------------| ``` (*) I would call it `Future.map` better than chain.
| * | [safe-string] lib/miscelaneaGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | No functional change.js
| * | [safe-string] lib/cUnixGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | No functional change.
| * | [safe_string] lib/cThreadGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | No functional changes.
* | | [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
|/ / | | | | | | It was always set to `greedy:true`.
* | Merge PR#189: Remove tabulation support from pretty-printing.Gravatar Maxime Dénès2017-02-20
|\ \
* | | [unicode] Address comments in PR#314.Gravatar Emilio Jesus Gallego Arias2017-02-15
| | |
* | | [safe-string] Use `String.init` to build string.Gravatar Emilio Jesus Gallego Arias2017-02-14
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\ \ \ | | |/ | |/|
* | | Merge PR#355: Remove unused feedback_content: GoalsGravatar Maxime Dénès2017-01-30
|\ \ \
| | * \ Merge PR#383: fix #5244: set printing width ignored when given enough spaceGravatar Maxime Dénès2017-01-24
| | |\ \
* | | \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Fix race condition in STM DAG generation (in debug mode).Gravatar Maxime Dénès2017-01-13
| | | | | | | | | | | | | | | | | | | | The same file name for .dot graphs could be used by concurrent processes.
| * | | | Fix broken .aux machinery.Gravatar Guillaume Melquiond2017-01-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Coq expects aux_file_name_for to give the aux file corresponding to the input file whichever its Coq-related extension, be it .v or .vo or .vio. Commit 3e6fa1c broke this contract when fixing bug #5183. As a consequence, depending on the execution path, Coq would try to save or load from either .foo.aux or .foo.vo.aux or .foo.vio.aux. This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call chain by not initializing hints when the input file does not end with .v. This also restores 8.5 behavior with respect to aux file naming.
* | | | | Avoid using the deprecated Scanf.fscanf function.Gravatar Maxime Dénès2017-01-09
| | | | |
* | | | | Merge remote-tracking branch 'github/pr/351' into trunkGravatar Maxime Dénès2016-12-19
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Was PR#351: Complete a truncated comment
* \ \ \ \ \ Merge remote-tracking branch 'github/pr/363' into trunkGravatar Maxime Dénès2016-12-19
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#363: lib/Unicodetable: Update.
| | | | | * | [pp] Set printing width for richpp formatter (bug #5244)Gravatar Emilio Jesus Gallego Arias2016-12-04
| | | | |/ / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Richpp output depends on printing width, thus its internal formatter should be seeded with the proper width value. While we are at it, we increase the default buffer size to a more sensible value.
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\ \ \ \ \ \ | | |_|/ / / | |/| | | |
| * | | | | Fix #5183 - Two CoqIDE crash errorsGravatar Maxime Dénès2016-11-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When opening a file without extension, an uncaught exception was occurring. Note that this fix is not complete, since the "Compile Buffer" command still fails. This is because of a limitation of coqc which appends the ".v" extension to its argument even if it already existed (and even if it doesn't exist with the extension!).
| * | | | | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| | | | |
| | * | | | lib/Unicodetable: Update. This code has been generated from the latestGravatar Yann Régis-Gianas2016-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unicode tables using UUCD, an OCaml library to parse the official Unicode tables.
| * | | | | Fix bug in warnings: -w foo was silent when foo did not exist.Gravatar Maxime Dénès2016-11-14
| | | | | |
| | | | * | Remove unused feedback_content: GoalsGravatar CJ Bell2016-11-10
| |_|_|/ / |/| | | |
| | | * | Complete a truncated commentGravatar Arnaud Spiwack2016-11-08
| |_|/ / |/| | | | | | | | | | | | | | | Introduce by myself, I'm afraid, in #308. Noticed by PMP during the review, but I forgot to fix it before merge.
| * | | Removing a special treatment for empty lines in comments.Gravatar Hugo Herbelin2016-11-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This made the whole pp code complicated only for the purpose of the beautifier, while it is not clear when this was useful. Removing the code for simplicity, not excluding to later address beautifier issues when they show up.
| * | | Fix #4837: ./configure -local makes coqdep issue many warningsGravatar Maxime Dénès2016-11-04
| | | | | | | | | | | | | | | | | | | | | | | | We simply remove the warnings about paths mixing Win32 and Unix separators, since that situation does not seem problematic (c.f. discussion on the bug tracker).
| * | | Remove an OCaml 4.02 construct.Gravatar Maxime Dénès2016-11-03
| | | | | | | | | | | | | | | | | | | | This was not detected by running coq-contribs, so it probably means that we are not testing with the right version of OCaml.
| * | | Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The flags are now interpreted from left to right, without any other precedence rule. The previous one did not make much sense in interactive mode. - Set Warnings and Set Warnings Append are now synonyms, and have the "append" semantics, which is the most natural one for warnings. - Warnings on unknown warnings are now printed only once (previously the would be repeated on further calls to Set Warnings, sections closing, module requiring...). - Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced to "-foo" (if foo exists, "" otherwise).
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | |
| * | | Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ \ | | | | | | | | | | | | | | | Was PR#319: More error tagging, try to fix bug 5135
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 23:54:06 +0000