aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-06-07coq_makefile: List.iteri is now standard since OCaml 4.00Pierre Letouzey
2016-06-07coq_makefile : short display of commands executed by makePierre Letouzey
This purely cosmetic effect is obtained by the same variables $(SHOW) and $(HIDE) as in the main Makefile of Coq. If you prefer the earlier raw output : make VERBOSE=1
2016-06-07coq_makefile: add some -ml-synonym to the ocamldep rulesPierre Letouzey
Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled correctly.
2016-06-07typoMatej Kosik
2016-06-07typographyMatej Kosik
2016-06-07printing.mllib: remove some other .mli-only from a .mllibPierre Letouzey
2016-06-07Test for #4787.Hugo Herbelin
2016-06-07Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).Hugo Herbelin
2016-06-07DocumentationEnrico Tassi
2016-06-07Adding an only printing flag to notations.Pierre-Marie Pédrot
2016-06-07Removing the use to Egramcoq.recover_constr_grammar.Pierre-Marie Pédrot
2016-06-06Relying instead on the Coq85 inclusion!Hugo Herbelin
2016-06-06Mode "Bracketing Last Introduction Pattern" is on for 8.4Hugo Herbelin
and global for 8.4 and 8.5.
2016-06-06Mode "Regular Subst Tactic" is on in 8.6.Hugo Herbelin
2016-06-06Merge remote-tracking branch 'github/pr/118' into trunkMaxime Dénès
2016-06-06Renaming: ErrorBlock -> ProofBlockEnrico Tassi
Since this is really what they are. Squashing this renaming back to the root of the feature branch is hard.
2016-06-06STM: each proof block can be enabled separatelyEnrico Tassi
By default we enable only {} and par: that are detectable in a complete way.
2016-06-06Error box detection run only on errorEnrico Tassi
Advantage: 0 cost if no error occurs Disadvantage: a box *must* end with the error absorbing command
2016-06-06STM: proof block detection for indentationEnrico Tassi
2016-06-06rebase on trunkEnrico Tassi
2016-06-06STM: fix error reporting of par:Enrico Tassi
2016-06-06STM: proof block detection made optional + simple testEnrico Tassi
2016-06-06Fixing problems introduced in 8.5 with Ltac trace report. E.g.Hugo Herbelin
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. g I. (* Was printing Top.Top#<>#1 *) idtac; f I. (* Was not properly locating error *) This is a "a minima" fix. This a different fix than in trunk, so the merge will have to take the trunk version.
2016-06-06About printing of traces of failures while calling ltac code.Hugo Herbelin
An Ltac trace printing mechanism was introduced in 8.4 which was inadvertedly modified by a series of commits such as 8e10368c3, 91f44f1da7a, ... It was also sometimes buggy, iirc, when entering ML tactics which themselves were calling ltac code. It got really bad in 8.5 as in: Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. idtac; f I. (* bad location reporting *) g I. (* was referring to tactic name "Top.Top#<>#1" *) which this commit fixes. I don't have a clear idea of what would be the best ltac tracing mechanism, but to avoid it to be broken without being noticed, I started to add some tests. Eventually, it might be worth that an Ltac expert brainstrom on it!
2016-06-06STM: proof block detection for par:Enrico Tassi
"par: tac" is a terminator, if it fails we can admit all focused goals and continue.
2016-06-06STM: proof block detection for bullets and { block }Enrico Tassi
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time.
2016-06-06STM: carry AST and indentation of document commandsEnrico Tassi
This paves the way to detecting error boundaries via indentation
2016-06-06STM: support for nested boxes of nodes to model error boundariesEnrico Tassi
Dag extended to support arbitrary clusters, renamed to Property. Vcs generalized to not impose the data hold by a Property. Stm(VCS) names a property "a box" and imposes a topological invariant (no overlap). It defines 2 kind of boxes: ProofTasks (the old cluster notion) and ErrorBound (meant to confine errors to sub-proofs). In the meanwhile more equations added to Make(..) functors in order to have just one Stateid.Set module around.
2016-06-06STM: invalid states are first class citizensEnrico Tassi
A state in the cache (document node) is now one of "Empty | Error | Valid". This paves the way to commands/blocks-of-commands resilient-to/confining errors: one can catch and "ignore" the exception obtained by reaching the previous state and do something sensible, like running anyway the command or skipping until the end of an error-confining block is reached. Invalid states carry an enriched exception with the safe_id attached, so that if one edits_at or observe them gets a safe place to land (CoqIDE needs such piece of info). Little API change in Stm.state_of_id now returning a `Error variant for the new kind of state.
2016-06-06xmlprotocol: fix unmarshaling of Feedback.MessageEnrico Tassi
2016-06-06xmlprotocol: uncomment marshalling code for custom messageEnrico Tassi
2016-06-06xmlprotocol: Marshal_error carries the reasonEnrico Tassi
2016-06-05Improve a comment in the test suiteJason Gross
2016-06-05Make Ltac Profiling an settingJason Gross
2016-06-05Synchronize the profiler state with the documentJason Gross
This is suboptimal, because mutation leaves room for subtle bugs, but rewriting @tebbi's code to be functional was a pain, and not something I could figure out how to do easily. I'm working under the assumption that there is no sharing in a single treenode, which I'm not completely sure is valid. That said, a few simple tests seem to indicate that this works as expected.
2016-06-05-profileltac -> -profile-ltac, as per @herbelinJason Gross
https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ```
2016-06-05Remove a spurious tclFINALLY when not profilingJason Gross
Implement the suggestion of @mattam82 to check whether or not we're profiling before inserting the tclFINALLY. Timing stats: Using: ```bash make clean && git clean -xfd && ./configure -local -with-doc no -coqide no && /usr/bin/time -f "all coq (real: %e, user: %U, sys: %S, mem: %M ko)" make STDTIME='/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 -j4 2>&1 ``` Without LtacProf (4c078b0362542908eb2fe1d63f0d867b339953fd), two runs: ``` real: 147.96, user: 467.93, sys: 30.80, mem: 820468 ko real: 148.04, user: 467.92, sys: 30.49, mem: 820680 ko ``` With LtacProf, two runs: ``` real: 148.32, user: 469.09, sys: 30.57, mem: 818588 ko real: 148.38, user: 469.71, sys: 30.56, mem: 816720 ko ``` Overall overhead on building Coq: about 0.24% Differences in the slowest files: ``` After | File Name | Before || Change --------------------------------------------------------------------------- 7m07.32s | Total | 7m05.16s || +0m02.15s --------------------------------------------------------------------------- 0m44.90s | Numbers/Rational/BigQ/QMake | 0m44.11s || +0m00.78s 0m15.94s | plugins/setoid_ring/Ncring_polynom | 0m15.72s || +0m00.21s 0m14.04s | Numbers/Cyclic/DoubleCyclic/DoubleCyclic | 0m14.05s || -0m00.01s 0m10.65s | Numbers/Cyclic/DoubleCyclic/DoubleSqrt | 0m10.45s || +0m00.20s 0m09.57s | FSets/FMapAVL | 0m09.53s || +0m00.04s 0m09.51s | MSets/MSetRBT | 0m09.45s || +0m00.06s 0m07.00s | Numbers/Cyclic/DoubleCyclic/DoubleDiv | 0m07.05s || -0m00.04s 0m06.88s | Numbers/Cyclic/Int31/Cyclic31 | 0m06.94s || -0m00.06s 0m05.82s | plugins/setoid_ring/Field_theory | 0m05.87s || -0m00.04s 0m05.74s | FSets/FMapFullAVL | 0m05.71s || +0m00.03s 0m05.37s | Reals/Ratan | 0m05.42s || -0m00.04s 0m05.36s | plugins/setoid_ring/Ring_polynom | 0m05.37s || -0m00.00s 0m05.09s | plugins/micromega/EnvRing | 0m04.96s || +0m00.12s ```
2016-06-05Add LtacProf documentationJason Gross
2016-06-05LtacProf for Coq trunkJason Gross
This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
2016-06-05Strip some trailing spacesJason Gross
2016-06-05Adding the Print Ltac Signatures command.Pierre-Marie Pédrot
2016-06-05Adding the Print Ltac Signature command.Pierre-Marie Pédrot
2016-06-05Remove Q_constr from grammar folder.Pierre-Marie Pédrot
2016-06-05Removing the Q_constr file.Pierre-Marie Pédrot
2016-06-05Moving Hipattern to a regular ML file.Pierre-Marie Pédrot
2016-06-05Removing PATTERN uses in Hipattern.Pierre-Marie Pédrot
2016-06-05Fix incorrect checking of library checksums.Maxime Dénès
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.
2016-06-04Merge remote-tracking branch 'github/pr/184' into trunkMaxime Dénès
2016-06-03Remove a few tactics from the Tacexpr AST.Pierre-Marie Pédrot
Note that this breaks a few badly written scripts using intro in strict mode without providing an existing identifier.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-30 11:44:40 +0000