| Age | Commit message (Collapse) | Author |
|---|
|
remove deprecated use of `if ... return`
|
|
Replace improper use of non-dependent `return` clause in `if` with a
type cast; an upcoming coq-side PR will discontinue support for this,
in order to support dependent return clauses with an implicit `as`
annotation.
|
|
Remove unused `Require`s and a hint directive from interval.v
|
|
|
|
ssrnum doesn't use zmodp theory
|
|
|
|
[ci] Extend the test-suite
|
|
Refactor CI with separate deploy jobs
|
|
- coq-mathcomp-odd-order.dev + coq.dev
- coq-mathcomp-bigenough.dev, coq-{8.7, 8.8, 8.9, dev}
- coq-mathcomp-finmap.dev, coq-{8.7, 8.8, 8.9, dev}
The configs below are commented-out as the upstream repos' opam is not
yet marked as compatible with mathcomp.dev (and Travis CI doesn't test
it with mathcomp-dev images)
# - coq-mathcomp-real-closed.dev, coq-{8.7, 8.8, 8.9, dev}
# - coq-mathcomp-analysis.dev, coq-{8.8, 8.9, dev}
Close math-comp/math-comp#245
|
|
|
|
|
|
so the images:
- mathcomp/mathcomp-dev:coq-8.7
- mathcomp/mathcomp-dev:coq-8.8
- mathcomp/mathcomp-dev:coq-8.9
- mathcomp/mathcomp-dev:coq-dev
will be pushed to Docker Hub even if a third-party library CI fails.
|
|
|
|
* The latter template job is trusted and only runs:
- in branch master,
- if all build *and* test jobs were successful
(major change in the deployment's condition)
* The other jobs are not tagged with "environment: name: deployment",
so they won't be able to read scoped protected variables.
* href: https://gitlab.com/help/ci/variables/README.md#limiting-environment-scopes-of-variables-premium
|
|
|
|
switching to opam 2.0 format
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Least common childen
|
|
Seq refactoring; adding `permutations`, extending `allpairs`
|
|
Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an
intermediate file for `hierarchy_test.py`. So the typical usage is:
$ python3.5 etc/utils/hierarchy_test.py \
<(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \
> mathcomp/test_suite/hierarchy_test.v
|
|
- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet
in #299 (except the link to the coq lib `Permutation` predicate).
Use insertions to construct permutations. This definition is closer
to the one proposed by @MrSet, than one using rotations (it adds one
line to the definition of `permutations` but the proofs become a
little simpler.)
- Added support for casts on `map` comprehension general terms.
- Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with
equational proofs; changed `allpairs_comp` to its converse
`map_allpairs` for consistency.
- Add three `allpairs` extensionality lemmas: for the non-localised,
dependent localised and non-dependent localised cases; as per
`eq_in_map`, the latter two are equivalences.
- Documented the `all2` predicate added in #224, and the view
combinators added in #202.
- Renamed `seq2_ind` to `seq_ind2`, and weakened the induction
hypothesis, adding a `size` equality assumption.
- Corrected the header to use `<=>` for `bool` predicate
documentation, and `<->` for `Prop` predicates, following the
library’s general convention.
- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
directive, making it possible to merge the `Rev` section into the
main `Sequences` section.
- Miscellaneous improvements to proof scripts and file organisation.
- Correct maximal implicits of `constant`.
- Fixes omitted `Prenex Implicit` declaration.
- Other implicits fixes.
- Fix apparent `done` regression It appears `done` now does a weaker
form of intros, and this broke the `dtuple_onP` proof. Updated the
proof to eliminate the issue.
(Commit log edited by @CohenCyril during the squash.)
|
|
|
|
|
|
|
|
|
|
remove support for Coq 8.6
|
|
|
|
rename test-suite -> test_suite to make coq happy
|
|
|
|
Fix inheritances from countalg to finalg
|
|
|
|
|
|
|
|
|
|
Dependent positive finfun
|
|
Describe extension and warn about incompatibilities.
|
|
Line 426 in `integral.v` diverged to over 40 minutes with the new
`finfun.v`, because matching `mod_Iirr` to `quo_Iirr` goes into
exponential backtracking. This is currently averted by limiting the
repetition of `mod_IirrE` in this `rewrite` line.
Making `finfun` mixing opaque brings this down to 40 seconds, and
locking `cfIirr` to a tractable 0.15 seconds, hopefully improving the
instances. This line also takes 47 seconds to execute in the master
branch, so this is likely an undetected Coq performance regression.
|
|
Coq currently fails to resolve Miller patterns against open evars
(issue coq/#9663), in particular it fails to unify `T -> ?R` with
`forall x : T, ?dR x` even when `?dR` does not have `x` in its context.
As a result canonical structures and constructor notations for the
new generalised dependent `finfun`s fail for the non-dependent use
cases, which is an unacceptable regression.
This commit mitigates the problem by specialising the canonical
instances and most of the constructor notation to the non-dependent
case, and introducing an alias of the `finfun_of` type that has
canonical instances for the dependent case, to allow experimentation
with that feature.
With this fix the whole `MathComp` library compiles, with a few
minor changes. The change in `integral_char` fixes a performance issue
that appears to be the consequence of insufficient locking of both
`finfun_eqType` and `cfIirr`; this will be explored in a further commit.
|
|
Clarified that the sample use provided is an example rather than a
misplaced unit test.
Added the definition of generic recursors to the examples, for both
non-dependent and dependent use cases.
|
|
Construct `finfun_of` directly from a bespoke indexed inductive type,
which both makes it structurally positive (and therefore usable as a
container in an `Inductive` definition), and accommodates naturally
dependent functions.
This is still WIP, because this PR exposed a serious shortcoming of
the Coq unification algorithm’s implantation of Miller patterns. This
bug defeats the inference of `Canonical` structures for `{ffun S -> T}`
when the instances are defined in the dependent case!
This causes unmanageable regressions starting in `matrix.v`, so I
have not been able to check for any impact past that. I’m pushing this
commit so that the Coq issue may be addressed.
Made `fun_of_fin` structurally decreasing: Changed the primitive
accessor of `finfun_of` from `tfgraph` to the `Funclass` coercion
`fun_of_fin`. This will make it possible to define recursive functions
on inductive types built using finite functions. While`tfgraph` is
still useful to transport the tuple canonical structures to
`finfun_of`, it is no longer central to the theory so its role has
been reduced.
|
|
As per @ejgallego ’s suggestion.
|
|
Add extra eta lemmas for the under tactic
|
|
Refactoring allpairs to handle the dependent version as well
|
|
|
|
compat sumn with bigop
|
