aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2018-12-05Add test for #8951.Gaëtan Gilbert
Close #8951.
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
Namely, it does not explicitly open a scope, but we remember that we don't need the %type delimiter when in type position.
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
This modifies the strategy in previous commits so that priorities are as before in case of non-open scopes with delimiters. Additionally, we document the rare situation of overlapping applicative notations (maybe this is too rare and ad hoc to be worth being documented though).
2018-12-04Using scope for printing: more tests.Hugo Herbelin
2018-12-04Fixing #8551 (missing delimiters when notation exists both lonely and in scope).Hugo Herbelin
2018-12-04Addressing issues with PR#873: performance and use of abbreviation for printing.Hugo Herbelin
We do a couple of changes: - Splitting notation keys into more categories to make table smaller. This should (a priori) make printing faster (see #6416). - Abbreviations are treated for printing like single notations: they are pushed to the scope stack, so that in a situation such as Open Scope foo_scope. Notation foo := term. Open Scope bar_scope. one looks for notations first in scope bar_scope, then try to use foo, they try for notations in scope foo_scope. - We seize the opportunity of this commit to simplify availability_of_notation which is now integrated to uninterp_notation and which does not have to be called explicitly anymore.
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
See discussion on coq-club starting on 23 August 2016.
2018-12-04Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2018-11-28Add a couple more printing tests for byte/asciiJason Gross
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
We encode the conversion to bits with little-endian right-associative tuples to ensure that the head of the tuple (the `fst` element) is the least significant bit. We still enforce that the ordering of bits matches the order of the `bool`s in the `ascii` inductive type.
2018-11-28Speed up ByteJason Gross
We could move another ~ 1s from Init.Byte to Strings.Byte by moving `of_bits_to_bits` and `to_bits_of_bits`, but I figured it's probably not worth it. After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------- 1m16.75s | Total | 1m21.45s || -0m04.70s | -5.77% ---------------------------------------------------------------------------------- 0m08.95s | Strings/Byte | 0m12.41s || -0m03.46s | -27.88% 0m07.24s | Byte | 0m08.76s || -0m01.51s | -17.35% 0m06.37s | plugins/setoid_ring/Ring_polynom | 0m06.24s || +0m00.12s | +2.08% 0m03.14s | Numbers/Integer/Abstract/ZBits | 0m03.20s || -0m00.06s | -1.87% 0m02.44s | ZArith/BinInt | 0m02.44s || +0m00.00s | +0.00% 0m02.24s | Numbers/Natural/Abstract/NBits | 0m02.20s || +0m00.04s | +1.81% 0m01.97s | Lists/List | 0m01.93s || +0m00.04s | +2.07% 0m01.85s | Numbers/NatInt/NZLog | 0m01.82s || +0m00.03s | +1.64% 0m01.78s | PArith/BinPos | 0m01.78s || +0m00.00s | +0.00% 0m01.74s | plugins/setoid_ring/InitialRing | 0m01.63s || +0m00.11s | +6.74% 0m01.73s | Strings/Ascii | 0m01.58s || +0m00.14s | +9.49% 0m01.39s | NArith/BinNat | 0m01.34s || +0m00.04s | +3.73% 0m01.32s | Numbers/NatInt/NZPow | 0m01.24s || +0m00.08s | +6.45% 0m01.22s | Numbers/NatInt/NZSqrt | 0m01.15s || +0m00.07s | +6.08% 0m01.11s | Arith/PeanoNat | 0m01.16s || -0m00.04s | -4.31% 0m01.10s | Numbers/Integer/Abstract/ZDivTrunc | 0m01.11s || -0m00.01s | -0.90% 0m01.02s | Specif | 0m01.04s || -0m00.02s | -1.92% 0m00.96s | Numbers/NatInt/NZMulOrder | 0m00.84s || +0m00.12s | +14.28% 0m00.95s | Numbers/Integer/Abstract/ZDivFloor | 0m00.97s || -0m00.02s | -2.06% 0m00.85s | plugins/setoid_ring/Ring_theory | 0m00.86s || -0m00.01s | -1.16% 0m00.82s | Structures/GenericMinMax | 0m00.85s || -0m00.03s | -3.52% 0m00.72s | Numbers/Integer/Abstract/ZLcm | 0m00.82s || -0m00.09s | -12.19% 0m00.69s | Numbers/NatInt/NZParity | 0m00.69s || +0m00.00s | +0.00% 0m00.68s | Numbers/NatInt/NZDiv | 0m00.71s || -0m00.02s | -4.22% 0m00.68s | Strings/String | 0m00.65s || +0m00.03s | +4.61% 0m00.64s | Numbers/Integer/Abstract/ZSgnAbs | 0m00.64s || +0m00.00s | +0.00% 0m00.64s | ZArith/Zeven | 0m00.48s || +0m00.16s | +33.33% 0m00.63s | ZArith/Zorder | 0m00.61s || +0m00.02s | +3.27% 0m00.57s | Numbers/Integer/Abstract/ZMulOrder | 0m00.67s || -0m00.10s | -14.92% 0m00.56s | Classes/Morphisms | 0m00.58s || -0m00.01s | -3.44% 0m00.55s | Numbers/NatInt/NZOrder | 0m00.51s || +0m00.04s | +7.84% 0m00.48s | ZArith/BinIntDef | 0m00.48s || +0m00.00s | +0.00% 0m00.46s | Classes/CMorphisms | 0m00.48s || -0m00.01s | -4.16% 0m00.46s | Numbers/Integer/Abstract/ZGcd | 0m00.46s || +0m00.00s | +0.00% 0m00.46s | Numbers/Natural/Abstract/NSub | 0m00.48s || -0m00.01s | -4.16% 0m00.45s | Logic | 0m00.44s || +0m00.01s | +2.27% 0m00.45s | Numbers/Natural/Abstract/NGcd | 0m00.48s || -0m00.02s | -6.24% 0m00.42s | Numbers/Natural/Abstract/NLcm | 0m00.40s || +0m00.01s | +4.99% 0m00.42s | Structures/OrdersFacts | 0m00.48s || -0m00.06s | -12.50% 0m00.41s | ZArith/Zbool | 0m00.38s || +0m00.02s | +7.89% 0m00.38s | Numbers/Integer/Abstract/ZPow | 0m00.34s || +0m00.03s | +11.76% 0m00.36s | Bool/Bool | 0m00.36s || +0m00.00s | +0.00% 0m00.36s | Numbers/NatInt/NZGcd | 0m00.35s || +0m00.01s | +2.85% 0m00.36s | ZArith/ZArith_dec | 0m00.38s || -0m00.02s | -5.26% 0m00.34s | Numbers/Integer/Abstract/ZAdd | 0m00.33s || +0m00.01s | +3.03% 0m00.34s | PArith/Pnat | 0m00.31s || +0m00.03s | +9.67% 0m00.32s | Numbers/Natural/Abstract/NOrder | 0m00.32s || +0m00.00s | +0.00% 0m00.32s | PArith/BinPosDef | 0m00.31s || +0m00.01s | +3.22% 0m00.32s | ZArith/Zcompare | 0m00.28s || +0m00.03s | +14.28% 0m00.30s | Classes/RelationClasses | 0m00.29s || +0m00.01s | +3.44% 0m00.30s | NArith/Nnat | 0m00.30s || +0m00.00s | +0.00% 0m00.29s | Numbers/Natural/Abstract/NAxioms | 0m00.26s || +0m00.02s | +11.53% 0m00.28s | Numbers/Integer/Abstract/ZAddOrder | 0m00.28s || +0m00.00s | +0.00% 0m00.28s | Structures/Orders | 0m00.30s || -0m00.01s | -6.66% 0m00.27s | Numbers/Integer/Abstract/ZAxioms | 0m00.23s || +0m00.04s | +17.39% 0m00.27s | Numbers/NatInt/NZAxioms | 0m00.26s || +0m00.01s | +3.84% 0m00.26s | Numbers/Integer/Abstract/ZMaxMin | 0m00.25s || +0m00.01s | +4.00% 0m00.26s | Numbers/NatInt/NZAdd | 0m00.28s || -0m00.02s | -7.14% 0m00.26s | Numbers/Natural/Abstract/NMaxMin | 0m00.24s || +0m00.02s | +8.33% 0m00.26s | Numbers/Natural/Abstract/NParity | 0m00.31s || -0m00.04s | -16.12% 0m00.26s | plugins/setoid_ring/ArithRing | 0m00.22s || +0m00.04s | +18.18% 0m00.26s | plugins/setoid_ring/Ring_tac | 0m00.24s || +0m00.02s | +8.33% 0m00.25s | Logic/Decidable | 0m00.26s || -0m00.01s | -3.84% 0m00.25s | Structures/OrdersTac | 0m00.25s || +0m00.00s | +0.00% 0m00.24s | Classes/Equivalence | 0m00.25s || -0m00.01s | -4.00% 0m00.24s | Datatypes | 0m00.27s || -0m00.03s | -11.11% 0m00.24s | Numbers/NatInt/NZMul | 0m00.25s || -0m00.01s | -4.00% 0m00.24s | plugins/setoid_ring/Ring | 0m00.20s || +0m00.03s | +19.99% 0m00.23s | Numbers/NatInt/NZAddOrder | 0m00.33s || -0m00.10s | -30.30% 0m00.23s | Numbers/Natural/Abstract/NAdd | 0m00.17s || +0m00.06s | +35.29% 0m00.22s | Arith/Compare_dec | 0m00.22s || +0m00.00s | +0.00% 0m00.22s | Classes/CRelationClasses | 0m00.25s || -0m00.03s | -12.00% 0m00.22s | Logic/EqdepFacts | 0m00.19s || +0m00.03s | +15.78% 0m00.22s | NArith/BinNatDef | 0m00.25s || -0m00.03s | -12.00% 0m00.22s | plugins/setoid_ring/Ring_base | 0m00.23s || -0m00.01s | -4.34% 0m00.21s | Arith/Arith | 0m00.19s || +0m00.01s | +10.52% 0m00.21s | Numbers/Natural/Abstract/NDiv | 0m00.19s || +0m00.01s | +10.52% 0m00.20s | Numbers/Integer/Abstract/ZProperties | 0m00.23s || -0m00.03s | -13.04% 0m00.20s | Relations/Relation_Operators | 0m00.17s || +0m00.03s | +17.64% 0m00.19s | Arith/Between | 0m00.22s || -0m00.03s | -13.63% 0m00.18s | Arith/Wf_nat | 0m00.24s || -0m00.06s | -25.00% 0m00.17s | Arith/Plus | 0m00.16s || +0m00.01s | +6.25% 0m00.17s | Nat | 0m00.18s || -0m00.00s | -5.55% 0m00.17s | Numbers/Natural/Abstract/NProperties | 0m00.22s || -0m00.04s | -22.72% 0m00.17s | Relations/Relation_Definitions | 0m00.08s || +0m00.09s | +112.50% 0m00.16s | Numbers/Integer/Abstract/ZLt | 0m00.16s || +0m00.00s | +0.00% 0m00.16s | Numbers/Natural/Abstract/NBase | 0m00.19s || -0m00.03s | -15.78% 0m00.16s | Numbers/Natural/Abstract/NPow | 0m00.15s || +0m00.01s | +6.66% 0m00.15s | Classes/Morphisms_Prop | 0m00.18s || -0m00.03s | -16.66% 0m00.14s | Arith/Mult | 0m00.12s || +0m00.02s | +16.66% 0m00.14s | Arith/Peano_dec | 0m00.16s || -0m00.01s | -12.49% 0m00.14s | Numbers/NatInt/NZBase | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | Numbers/Natural/Abstract/NMulOrder | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | Relations/Operators_Properties | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | plugins/setoid_ring/BinList | 0m00.16s || -0m00.01s | -12.49% 0m00.13s | Arith/EqNat | 0m00.18s || -0m00.04s | -27.77% 0m00.13s | Structures/Equalities | 0m00.17s || -0m00.04s | -23.52% 0m00.12s | Arith/Lt | 0m00.11s || +0m00.00s | +9.09% 0m00.12s | Arith/Minus | 0m00.13s || -0m00.01s | -7.69% 0m00.12s | Decimal | 0m00.16s || -0m00.04s | -25.00% 0m00.12s | Numbers/Integer/Abstract/ZBase | 0m00.09s || +0m00.03s | +33.33% 0m00.12s | Numbers/Integer/Abstract/ZMul | 0m00.12s || +0m00.00s | +0.00% 0m00.12s | Numbers/Integer/Abstract/ZParity | 0m00.11s || +0m00.00s | +9.09% 0m00.12s | Numbers/Natural/Abstract/NAddOrder | 0m00.12s || +0m00.00s | +0.00% 0m00.11s | Arith/Factorial | 0m00.11s || +0m00.00s | +0.00% 0m00.11s | Lists/ListTactics | 0m00.13s || -0m00.02s | -15.38% 0m00.11s | Logic/Eqdep_dec | 0m00.12s || -0m00.00s | -8.33% 0m00.11s | Numbers/Natural/Abstract/NLog | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Peano | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Program/Basics | 0m00.07s || +0m00.03s | +57.14% 0m00.10s | Arith/Gt | 0m00.13s || -0m00.03s | -23.07% 0m00.10s | Bool/Sumbool | 0m00.10s || +0m00.00s | +0.00% 0m00.10s | Numbers/Natural/Abstract/NSqrt | 0m00.12s || -0m00.01s | -16.66% 0m00.10s | Wf | 0m00.11s || -0m00.00s | -9.09% 0m00.09s | Arith/Arith_base | 0m00.09s || +0m00.00s | +0.00% 0m00.09s | Logic_Type | 0m00.08s || +0m00.00s | +12.49% 0m00.08s | Arith/Le | 0m00.11s || -0m00.03s | -27.27% 0m00.08s | Numbers/BinNums | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Numbers/NatInt/NZBits | 0m00.12s || -0m00.03s | -33.33% 0m00.08s | Numbers/NatInt/NZProperties | 0m00.09s || -0m00.00s | -11.11% 0m00.08s | Program/Tactics | 0m00.08s || +0m00.00s | +0.00% 0m00.07s | Tactics | 0m00.10s || -0m00.03s | -30.00% 0m00.06s | Classes/SetoidTactics | 0m00.06s || +0m00.00s | +0.00% 0m00.06s | Numbers/NumPrelude | 0m00.06s || +0m00.00s | +0.00% 0m00.05s | Classes/Init | 0m00.04s || +0m00.01s | +25.00% 0m00.05s | Prelude | 0m00.09s || -0m00.03s | -44.44% 0m00.05s | Setoids/Setoid | 0m00.08s || -0m00.03s | -37.50% 0m00.04s | Relations/Relations | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Tauto | 0m00.09s || -0m00.05s | -55.55% 0m00.02s | Notations | 0m00.04s || -0m00.02s | -50.00%
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
Users can now register string notations for custom inductives. Much of the code and documentation was copied from numeral notations. I chose to use a 256-constructor inductive for primitive string syntax because (a) it is easy to convert between character codes and constructors, and (b) it is more efficient than the existing `ascii` type. Some choices about proofs of the new `byte` type were made based on efficiency. For example, https://github.com/coq/coq/issues/8517 means that we cannot simply use `Scheme Equality` for this type, and I have taken some care to ensure that the proofs of decidable equality and conversion are fast. (Unfortunately, the `Init/Byte.v` file is the slowest one in the prelude (it takes a couple of seconds to build), and I'm not sure where the slowness is.) In String.v, some uses of `0` as a `nat` were replaced by `O`, because the file initially refused to check interactively otherwise (it complained that `0` could not be interpreted in `string_scope` before loading `Coq.Strings.String`). There is unfortunately a decent amount of code duplication between numeral notations and string notations. I have not put too much thought into chosing names; most names have been chosen to be similar to numeral notations, though I chose the name `byte` from https://github.com/coq/coq/issues/8483#issuecomment-421671785. Unfortunately, this feature does not support declaring string syntax for `list ascii`, unless that type is wrapped in a record or other inductive type. This is not a fundamental limitation; it should be relatively easy for someone who knows the API of the reduction machinery in Coq to extend both this and numeral notations to support any type whose hnf starts with an inductive type. (The reason for needing an inductive type to bottom out at is that this is how the plugin determines what constructors are the entry points for printing the given notation. However, see also https://github.com/coq/coq/issues/8964 for complications that are more likely to arise if inductive type families are supported.) N.B. I generated the long lists of constructors for the `byte` type with short python scripts. Closes #8853
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-28Merge PR #9089: Fix #9076 (warning appears when running test suite)Emilio Jesus Gallego Arias
2018-11-27Fix #9076 (warning appears when running test suite)Maxime Dénès
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
When making a universe a variable we iterate through the universes we're equal to and if we find one we update the substitution accordingly. NB: The bug called make_flexible_variable on Top.15 and ~~~ {Top.15 Top.14} |= Top.11 < Top.6 Top.14 < Top.5 Top.11 = Top.15 ALGEBRAIC UNIVERSES:{Top.17 Top.16} UNDEFINED UNIVERSES:Top.17 := Top.14+1 Top.16 := Top.14+1 WEAK CONSTRAINTS: ~~~ so now we would add [Top.15 := Top.11].
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
This introduces the warning “not-a-class” in the “typeclasses” category.
2018-11-24Merge PR #8996: Fix #8937: inductive conversion in coqchk subtypingHugo Herbelin
2018-11-23Merge PR #8890: Looking for notation both before or after removal of top ↵Emilio Jesus Gallego Arias
coercion
2018-11-23Merge PR #8995: Don't redeclare constraints of fields in IncludeMaxime Dénès
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23Fix #8937: inductive conversion in coqchk subtypingGaëtan Gilbert
As far as I can tell this is similar to what coqtop does. Delta resolvers are complicated so I may be mistaken. The important part is to avoid losing the modified delta resolver returned by strengthen_and_subst in check_mexpr.
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-20Notations: Trying using a notation with or w/o removal of coercions.Hugo Herbelin
Preferring a notation which does require a delimiter, depending on whether the coercion is removed or not, was done for primitive tokens. We do it for all notations.
2018-11-20Merge PR #9016: PRINT_LOGS=1 in appveyor test suite runEnrico Tassi
2018-11-20Rename gh->bug_ test filesGaëtan Gilbert
2018-11-19Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.Pierre-Marie Pédrot
2018-11-19Merge PR #9001: [options] Remove deprecated option automatic introduction.Pierre-Marie Pédrot
2018-11-19Merge PR #9013: Do not Export the init modulesPierre-Marie Pédrot
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Print logs in appveyor test suite runGaëtan Gilbert
It seems we forgot to export when moving the script to a separate file.
2018-11-16Print Universes SubgraphGaëtan Gilbert
This adds an optional [Subgraph] part to the Print Universes command, eg [Print Universes Subgraph(i j)] to print only constraints related to i and j (and Prop/Set).
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
Use of boxes to ensure locality of formatting + use of a prlist_with_sep so that there are breaking points only inbetween the elements and not at the end of the list.
2018-11-16Add test for Include in -quick modeGaëtan Gilbert
2018-11-16Do not Export the init modulesGaëtan Gilbert
It seems we started doing the export silently in 47804492bd09c8b13b5aac45800d067dbdf04d00.
2018-11-15Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"Vincent Laporte
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
Allow for new goals that don't map to old goals Include background_goals in all_goals return value Fix incorrect change to raw diffs in shorten_diff_span Fixes #8922
2018-11-14Merge PR #8966: coq_makefile: Fix ocamldep ignoring mlg filesEmilio Jesus Gallego Arias
2018-11-14ssr: add another test for elim + TCEnrico Tassi
2018-11-14ssrmatching: unify_HO does not resolve type classesEnrico Tassi
2018-11-13Merge PR #8886: [VM] Fix compilation of int31 eliminatorsMaxime Dénès
2018-11-13Merge PR #8760: Automatically generate names for universes.Pierre-Marie Pédrot
2018-11-13coq_makefile: Fix ocamldep ignoring mlg filesGaëtan Gilbert
If you have file1.mlg and file2.ml, with file2 depending on file1, ocamldep was before generating file1.ml so wouldn't generate [file2.cmx: file1.cmx] (ocamldep is silent on non-found dependencies). This has been causing nondeterministic failures in quickchick recently. I guess it didn't come up in the past because ml4 files tend to be at the end of the dependency chain.
2018-11-13Merge PR #8957: Fix -top for univbinders output test.Emilio Jesus Gallego Arias
2018-11-13Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes.Pierre-Marie Pédrot
2018-11-12Automatically generate names for universes.Gaëtan Gilbert
The names are `uXXX` with `XXX` some number avoiding collision. Note that there may be some collisions with polymorphic binders, eg something like ~~~ Set Universe Polymorphism. Section foo. Universe u0. Definition bar := Type. (* bar@{u0} = Type@{u0} but this isn't the section u0 *) Definition baz := Type@{u0}. (* this one is the section u0 *) Definition foobar := Eval compute in baz -> Type. (* Type@{u0} -> Type@{u0} but these aren't the same u0 *) ~~~ So maybe we should do a nametab lookup too. This is strictly a printing issue (polymorphic binder names have no other use). In the monomorphic case names are qualified by the parent definition so it should be fine (barring module/definition collision but we already have those). Note that there are still unnamed universes as they didn't go through UState (eg schemes).
2018-11-12Do not qualify universe names by section path.Gaëtan Gilbert
2018-11-12Fix incorrect coq-prog-args in unideclsGaëtan Gilbert
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
Otherwise ~~~ Unset Strict Universe Declaration. Section bar. Let baz := Type@{u}. Definition k := baz. End bar. Section bar. Let baz := Type@{u}. Definition k' := baz. End bar. ~~~ is broken (and has been since we stopped checking for repeated section names).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 03:35:34 +0000