aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Search.out
AgeCommit message (Collapse)Author
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
For nonsquashed: Either - 0 constructors - primitive record
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
2017-04-21Remove VernacErrorGaetan Gilbert
2017-02-14Test-suite: output of SearchArnaud Spiwack
Fix the ordering of the results in the output of Search to correspond to the "priority" ordering.
2014-12-15Tests for Searchxxx commands added and modified.Pierre Courtieu
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Update output/Search.out after hint-related extra defs in Peanoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15980 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-16test-suite: no more ..._beq in the output of the search testsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14128 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-16Fix order in Search tests.letouzey
Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14127 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11Minimal test suite for search commandspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12860 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:36:10 +0000