| Age | Commit message (Collapse) | Author |
|---|
|
We replace open/close tag commands by a well-balanced "tag" wrapper.
|
|
|
|
|
|
We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.
|
|
Mostly unused, we ought to limit spacing in the boxes themselves.
|
|
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.
|
|
Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.
The printers now tag unconditionally, it is up to the backends to
interpreted the tags.
Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.
Tested, test-suite passes.
Notes:
- We remove the `Richprinter` module. It was only used in the
`annotate` IDE protocol call, its output was identical to the normal
printer (or even inconsistent if taggers were not kept manually in
sync).
- Note that Richpp didn't need a single change. In particular, its
main API entry point `Richpp.rich_pp` is not used by anyone.
|
|
The miscellaneous `msg_*` cleanup patches have finally enforced this
invariant.
|
|
We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
|
|
|
|
|
|
|
|
|
|
(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.
|
|
The `a.[i] <- x` notation is deprecated and we were getting a couple
of warnings.
|
|
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.
|
|
|
|
|
|
The "theories/Logic/PropExtensionalityFacts.v" file was:
- compiled
- used in several places
but not actually installed.
This commit fixes that.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
|
Coq.
|
|
|
|
We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.
- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
|
|
No functional changes.
|
|
No functional change, one extra copy introduced but it seems hard to
avoid.
|
|
No functional change.
|
|
No functional change, one extra copy introduced but it seems hard to
avoid.
|
|
No functional changes, only a minor copy on a deprecated output
option.
|
|
No functional change, even if we could optimize `blanch_utf8_string` a
bit more by using `String.init`.
|
|
No functional change.
|
|
No functional change.
|
|
We add a more convenient API to create identifiers from mutable
strings. We cannot solve the `String.copy` deprecation problem until
we enable `-safe-string`.
|
|
The `emitcodes` string type was used in both a functional and an
imperative way, so we have to handle it with care in order to preserve
the previous optimizations and semantics.
|
|
Maxime points out that -notop cannot be used as the kernel requires
all constants to belong into a module. Indeed:
```
$ rlwrap ./bin/coqtop -notop
Coq < Definition foo := True.
Toplevel input, characters 0-23:
> Definition foo := True.
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: No session module started (use -top dir)
Coq < Module M. Definition foo := True. End M.
Module M is defined
Coq < Locate foo.
Constant If you see this, it's a bug.M.foo
(shorter name to refer to it in current context is M.foo)
```
My rationale for the removal is that this kind of incomplete features
are often confusing to newcomers ─ it has happened to me many times ─
as it can be seen for example in #397 .
|
|
|
|
Augments "A fully applied tactic is expected" with the list of missing
arguments to the tactic. Addresses [bug
5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
|
|
No functional change.
|
|
No functional change, we create the new string beforehand and
`id_of_string` will become a noop with `-safe-string`.
|
|
No functional change.js
|
|
No functional change.
|
|
No functional changes.
|
|
|
|
|
