aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-14Merge PR#563: add XML protocol doc for 8.6Maxime Dénès
2017-04-14[travis] Use the lite target for fiat-crypto.Maxime Dénès
2017-04-13update XML protocol doc to 8.6Paul Steckler
2017-04-13add XML protocol doc for 8.5Paul Steckler
2017-04-12Merge PR#510: Correctly identify [Time Defined.] as a definedMaxime Dénès
2017-04-08Fixing #5460 (limitation in computing deps in pattern-matching compilation).Hugo Herbelin
This was assuming dependencies occurring in configurations of the form x:A, y:B x, z:C x y |- match x, y, z with ... end". But still work to do for better management of dependencies in general...
2017-04-06Fix a few programming pearls related to Time, Fail and Redirect.Maxime Dénès
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.
2017-04-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
Was needed to be done for a while.
2017-04-05Fixing #5454 (an assert false with 'pat).Hugo Herbelin
Note: Apparently not easy to make a test file as the error is raised in "G_vernac.fresh_var" at parsing time (not captured by Fail).
2017-04-04Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Test file for #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Fix bug #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously avoided by a safeguard I put in nativecode.ml. But other kernel changes in this commit should probably be reviewed carefully.
2017-04-03Merge PR#533: Instances should obey universe binders even when defined by ↵Maxime Dénès
tactics.
2017-04-03Instances should obey universe binders even when defined by tactics.Gaetan Gilbert
2017-04-03Add test file for #4957.Maxime Dénès
Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly".
2017-03-30Merge PR#463: Run non-tactic comands without resilient_commandMaxime Dénès
2017-03-29Merge PR#514: [travis] Backport from trunk: VSTMaxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-24[travis] Backport from trunk: VSTEmilio Jesus Gallego Arias
2017-03-24Merge PR#476: [future] Be eager when "chaining" already resolved future values.Maxime Dénès
2017-03-24Merge PR#475: Opaque side effectsMaxime Dénès
2017-03-23Correctly identify [Time Defined.] as a definedTej Chajed
Need to check inside control expressions. Also fixes handling of [Redirect "file" Defined.] and [Timeout n Defined.]. Fixes Coq bug 5411 (https://coq.inria.fr/bugs/show_bug.cgi?id=5411): coqc -quick hangs on [Time Defined.]
2017-03-23Merge PR#507: Intern names bound in match patternsMaxime Dénès
2017-03-23Documenting the API of side-effects.Pierre-Marie Pédrot
2017-03-23Using a dedicated datastructure for side effect ordering.Pierre-Marie Pédrot
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.
2017-03-23Making the side_effects type opaque.Pierre-Marie Pédrot
We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module.
2017-03-23Intern names bound in match patternsTej Chajed
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345): Cannot use names bound in matches inside Ltac definitions.
2017-03-23Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Maxime Dénès
2017-03-23Merge PR#495: funind: Ignore missing info for current functionMaxime Dénès
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
2017-03-23Merge PR#491: Do not typecheck twice the type of opaque constants.Maxime Dénès
2017-03-22Merge PR#480: show unused intro pattern warningMaxime Dénès
2017-03-22[travis] [8.6.only] Backport latest changes from trunk.Emilio Jesus Gallego Arias
2017-03-22funind: Ignore missing info for current functionTej Chajed
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".
2017-03-21Add a few comments in term_typing.ml.Maxime Dénès
2017-03-21Do not typecheck twice the type of opaque constants.Maxime Dénès
I believe an unwanted shadowing was introduced by a4043608f704f0.
2017-03-20Merge PR#430: make `emit' tail recursiveMaxime Dénès
2017-03-20In the Kami project, that causes a stack overflow in one of the example filesPaul Steckler
(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.
2017-03-20[future] Use eager evaluation for chaining values.Emilio Jesus Gallego Arias
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.
2017-03-17Merge PR#429: Don't require printing-only notation to be productiveMaxime Dénès
2017-03-14Merge PR#465: Fix #5132: coq_makefile generates incorrect install goalMaxime Dénès
2017-03-14Fix #5132: coq_makefile generates incorrect install goalVadim Zaliva
2017-03-14Fix 3 unused-intro-pattern warnings in stdlib.Théo Zimmermann
2017-03-14Show unused-intro-pattern warning.Théo Zimmermann
This warning was shown in CoqIDE but not by coqc.
2017-03-10Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals ↵Maxime Dénès
correctly as…
2017-03-10[travis] Move GeoCoq to allow fail.Emilio Jesus Gallego Arias
We need to agree a bit more with upstream.
2017-03-07Merge PR#452: [ltac] Move dummy plugin to plugins folder.Maxime Dénès
2017-03-07Merge PR#453: [travis] Backport trunk's travis support.Maxime Dénès
2017-03-03[ltac] Move dummy plugin to plugins folder.Emilio Jesus Gallego Arias
This is needed to fix `Declare ML Module "ltac_plugin".
2017-03-02[travis] Backport trunk's travis support.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 20:34:49 +0000