aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-28Fix string notation docJason Gross
As per https://github.com/coq/coq/pull/8965/files#r237225852
2018-11-28Proofs to ensure that conversions round-tripJason Gross
We already have roundtrip proofs for byte<->nat, byte<->N, byte<->ascii, N<->nat, ascii<->N, ascii<->nat, and this commit shows that all roundtrips involving byte commute appropriately. This ensures, e.g., that we don't mess up and reverse the bits in conversion between byte and ascii.
2018-11-28Factor out common code in numeral/string notationsJason Gross
As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
2018-11-28Add extraction directives for nicer extraction of bytesJason Gross
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 #9041: [Windows CI] Do not build any addon if WINDOWS is not ↵Michael Soegtrop
enabled_all_addons.
2018-11-28Merge PR #7153: Make OrderedTypeFullFacts a module functorGaëtan Gilbert
2018-11-28Remove Windows from allow_failure now that addons are not tested on PRs.Théo Zimmermann
2018-11-28[Windows CI] Do not build any addon if WINDOWS is not enabled_all_addons.Théo Zimmermann
Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
2018-11-28Merge PR #9094: [lib] Remove leftover flag `print_mod_uid`Maxime Dénès
2018-11-28Merge PR #8727: [options] New helper for creation of boolean options plus ↵Pierre-Marie Pédrot
reference.
2018-11-28Merge PR #8826: [toplevel] Allow to specify default options.Pierre-Marie Pédrot
2018-11-28Merge PR #9089: Fix #9076 (warning appears when running test suite)Emilio Jesus Gallego Arias
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
This makes setting the option outside of the synchronized summary impossible.
2018-11-27Merge PR #8854: Fix #8364: making univ algebraic when already equal to another.Matthieu Sozeau
2018-11-27Merge PR #9072: Clean stm flagsEnrico Tassi
2018-11-27[lib] Remove leftover flag `print_mod_uid`Emilio Jesus Gallego Arias
The whole `native_name_from_filename` business seems quite strange tho.
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a ↵Emilio Jesus Gallego Arias
write_function
2018-11-27Make `-async-proofs on` effective with `coqc`Maxime Dénès
Before this patch, it had no effect.
2018-11-27Remove -async-proofs-full flagMaxime Dénès
The semantics of this flag was not clear, it had several rather orthogonal effects. Also, it should probably have been another value of `-async-proofs-mode`, rather than a separate flag, as its combination with e.g. `-async-proofs-mode off` is unclear.
2018-11-27Merge PR #7033: Remove obsolete files from dev/docThéo Zimmermann
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-27Merge PR #7696: Remove some univ_flexible_alg from casesPierre-Marie Pédrot
2018-11-27Merge PR #8255: Fast typing of application nodesMaxime Dénès
2018-11-27Merge PR #8986: Put -indices-matter in typing_flagsMaxime Dénès
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-27Record.declare_class: remove unused “finite” parameterVincent Laporte
2018-11-27Merge PR #8686: [toplevel] Move compilation-related functions to their own ↵Pierre-Marie Pédrot
module.
2018-11-26Merge PR #9075: [ci] Set windows jobs to allow_failure: trueGaëtan Gilbert
2018-11-26Merge PR #9057: [nix-ci] Add a README in dev/ci/nixThéo Zimmermann
2018-11-26Merge PR #9063: [checker] Remove duplicated code from checker / clibPierre-Marie Pédrot
2018-11-26[ci] Set windows jobs to allow_failure: trueEmilio Jesus Gallego Arias
Windows jobs have been polluting the CI for quite a few days, allow them to fail.
2018-11-26Merge PR #9074: Fix ocamldebug-coq for packed gramlibEmilio Jesus Gallego Arias
2018-11-26Fix ocamldebug-coq for packed gramlibGaëtan Gilbert
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-26[nix-ci] Add a README in dev/ci/nixVincent Laporte
2018-11-26[nix-ci] Use master version of UnicoqVincent Laporte
2018-11-25Merge PR #9036: Add bodies to sphinx objects.Clément Pit-Claudel
2018-11-24[toplevel] Allow to specify default options.Emilio Jesus Gallego Arias
In some cases, toplevel ML clients may want to modify the default set of flags that is passed to the main initalization routine. This is for example useful for `idetop` to suppress some undesired printing at startup. I would say that clients ought to have more control, but I do expect that PRs such as #8690 will help providing a better separation thus a mode orthogonal API.
2018-11-24[toplevel] Move compilation-related functions to their own module.Emilio Jesus Gallego Arias
We move compilation-specific functions to their own module. This helps isolating `.vo` compile-time functionality from interactive, toplevel-like processing. cc: #8683
2018-11-24[toplevel] Move command line path processing to CoqargsEmilio Jesus Gallego Arias
We move the processing of path-related arguments to `Coqargs`, and following experience from `SerAPI` we stored already-processed `coq_paths` in the `opts` record. This has proven to be very convenient as to avoid duplication of code in the presence of several clients of the `Coqargs` parsing functionality.
2018-11-24Merge PR #8996: Fix #8937: inductive conversion in coqchk subtypingHugo Herbelin
2018-11-24Merge PR #8950: [topfmt] Add phase attribute for toplevel printing.Hugo Herbelin
2018-11-24[checker] Remove duplicated from checker / clibEmilio Jesus Gallego Arias
Now that we link lib we can do this.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:11:41 +0000