aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Run non-tactic comands without resilient_commandGravatar Tej Chajed2017-03-29
|
* Merge PR#476: [future] Be eager when "chaining" already resolved future values.Gravatar Maxime Dénès2017-03-24
|\
* \ Merge PR#475: Opaque side effectsGravatar Maxime Dénès2017-03-24
|\ \
* \ \ Merge PR#507: Intern names bound in match patternsGravatar Maxime Dénès2017-03-23
|\ \ \
| | * | Documenting the API of side-effects.Gravatar Pierre-Marie Pédrot2017-03-23
| | | |
| | * | Using a dedicated datastructure for side effect ordering.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We were doing fishy things in the Term_typing file, where side-effects were not considered in the right uniquization order because of the uniq_seff_rev function. It probably did not matter after a9b76df because effects were (mostly) uniquize upfront, but this is not clear because of the use of the transparente API in the module. Now everything has to go through the opaque API, so that a proper dependence order is ensured.
| | * | Making the side_effects type opaque.Gravatar Pierre-Marie Pédrot2017-03-23
| |/ / |/| | | | | | | | | | | We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module.
| * | Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| | | | | | | | | | | | | | | Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345): Cannot use names bound in matches inside Ltac definitions.
* | | Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Gravatar Maxime Dénès2017-03-23
|\ \ \
* \ \ \ Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
|\ \ \ \ | |_|/ / |/| | |
* | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | | | | | | This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
* | | | Merge PR#491: Do not typecheck twice the type of opaque constants.Gravatar Maxime Dénès2017-03-23
|\ \ \ \
* \ \ \ \ Merge PR#480: show unused intro pattern warningGravatar Maxime Dénès2017-03-22
|\ \ \ \ \
| | | | * | [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
| |_|_|/ / |/| | | |
| | | * | funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| |_|/ / |/| | | | | | | | | | | | | | | | | | | Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372) "Anomaly: Not a valid information when defining mutual fixpoints that are not mutual with Function".
| | * | Add a few comments in term_typing.ml.Gravatar Maxime Dénès2017-03-21
| | | |
| | * | Do not typecheck twice the type of opaque constants.Gravatar Maxime Dénès2017-03-21
| |/ / |/| | | | | | | | I believe an unwanted shadowing was introduced by a4043608f704f0.
* | | Merge PR#430: make `emit' tail recursiveGravatar Maxime Dénès2017-03-20
|\ \ \
| * | | In the Kami project, that causes a stack overflow in one of the example filesGravatar Paul Steckler2017-03-20
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (ProcThreeStInl.v, when the final "Defined" runs). I've verified that the change here fixes the stack overflow there with Coq 8.5pl2. In this version, all the recursive calls are in tail position. Instead of taking a single list of instructions, `emit' here takes a curent list and a remaining list of lists of instructions. That means the two calls elsewhere in the file now add an empty list argument. The algorithm works on the current list until it's empty, then works on the remaining lists. The most complex case is for Ksequence, where one of the pieces becomes the new current list, and the other pieces are consed onto the remaining sub-lists.
| | * [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.
* | Merge PR#429: Don't require printing-only notation to be productiveGravatar Maxime Dénès2017-03-17
|\ \
* \ \ Merge PR#465: Fix #5132: coq_makefile generates incorrect install goalGravatar Maxime Dénès2017-03-14
|\ \ \
| * | | Fix #5132: coq_makefile generates incorrect install goalGravatar Vadim Zaliva2017-03-14
| | | |
| | | * Fix 3 unused-intro-pattern warnings in stdlib.Gravatar Théo Zimmermann2017-03-14
| | | |
| | | * Show unused-intro-pattern warning.Gravatar Théo Zimmermann2017-03-14
| | | | | | | | | | | | | | | | This warning was shown in CoqIDE but not by coqc.
* | | | Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals ↵Gravatar Maxime Dénès2017-03-10
|\ \ \ \ | | | | | | | | | | | | | | | correctly as…
* | | | | [travis] Move GeoCoq to allow fail.Gravatar Emilio Jesus Gallego Arias2017-03-10
| | | | | | | | | | | | | | | | | | | | We need to agree a bit more with upstream.
* | | | | Merge PR#452: [ltac] Move dummy plugin to plugins folder.Gravatar Maxime Dénès2017-03-07
|\ \ \ \ \
* \ \ \ \ \ Merge PR#453: [travis] Backport trunk's travis support.Gravatar Maxime Dénès2017-03-07
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
| | * | | | [ltac] Move dummy plugin to plugins folder.Gravatar Emilio Jesus Gallego Arias2017-03-03
| |/ / / / |/| | | | | | | | | | | | | | This is needed to fix `Declare ML Module "ltac_plugin".
| * | | | [travis] Backport trunk's travis support.Gravatar Emilio Jesus Gallego Arias2017-03-02
|/ / / /
* | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-22
|\ \ \ \
* | | | | Add empty ltac_plugin file for forward compatibility.Gravatar Maxime Dénès2017-02-21
| | | | | | | | | | | | | | | | | | | | This is in preparation for landing of PR#309: Ltac as a plugin
* | | | | Fixing #5339 (anomaly with 'pat in record parameters).Gravatar Hugo Herbelin2017-02-16
| | | | |
| | | * | reject notations that are both 'only printing' and 'only parsing'Gravatar Ralf Jung2017-02-16
| | | | |
| | | * | don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
| |_|/ / |/| | |
* | | | Turning an anomaly on 'pat into a proper "unsupported" error message.Gravatar Hugo Herbelin2017-02-09
| | | |
* | | | Fixing bug #5346 (an unimplemented application of 'pat).Gravatar Hugo Herbelin2017-02-09
| | | |
* | | | Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
| * | | Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
* | | | fix Emacs compiler warning on '(lambda...)Gravatar Hendrik Tews2017-02-06
| | | | | | | | | | | | | | | | | | | | lambda is self-quoting, see elisp manual, section 12.7 Anonymous Functions
* | | | Fixing an anomaly with 'pat after cofix.Gravatar Hugo Herbelin2017-02-02
| | | |
* | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
|\| | |
| * | | Fixing #5311 (anomaly on unexpected intro pattern).Gravatar Hugo Herbelin2017-01-31
| | | | | | | | | | | | | | | | | | | | This was introduced in 8.5 while reorganizing the structure of intro-patterns.
| * | | Merge PR#408: [native comp] Improve error message on linking error.Gravatar Maxime Dénès2017-01-30
| |\ \ \
* | | | | Fix a typo in STM universe communications.Gravatar Maxime Dénès2017-01-30
| | | | |
* | | | | Fix bug #5262: Error should tell me which name is duplicated.Gravatar Pierre-Marie Pédrot2017-01-28
| | | | |
* | | | | Fix documentation typos.Gravatar Guillaume Melquiond2017-01-27
| | | | |
| | * | | [native comp] Improve error message on linking error.Gravatar Emilio Jesus Gallego Arias2017-01-26
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The native compiler doesn't support `Require` inside `Module` sections in some cases, we improve the error message. See: https://coq.inria.fr/bugs/show_bug.cgi?id=4335 This patch improves the error message and gives the user some feedback.
* | | | Fixing #5326 (anomaly on some unsupported case of 'pat).Gravatar Hugo Herbelin2017-01-26
| | | | | | | | | | | | | | | | | | | | We complete the support of 'pat in this particular case (a 'pat under a binder in a notation).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 12:05:18 +0000