| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
missing lemma in seq.v
|
|
|
|
|
|
adding ffun0
|
|
|
|
Related: coq/coq#9651
|
|
[doc] Mention that "connect" computes the reflexive transitive closure
|
|
while some refs (see e.g. [1]) don't assume that the "transitive closure" is
reflexive; so one won't need to look at lemma "connect0" to figure this out.
[1] https://en.wikipedia.org/wiki/Transitive_closure
[ci skip]
|
|
|
|
A tool to draw the hierarchy diagram
|
|
remove dependency on hidden case branch types
|
|
Anticipating coq/coq#9170, remove numeric occurrence selector affected
by the (invisible) presence of explicit types for variables bound in
`match` branch patterns. The proof could be further simplified if this
change is implemented.
|
|
Export addrKA and subrKA from GRing.Theory
|
|
|
|
|
|
|
|
|
|
|
|
pmap_cat, pmap_perm and perm_map_inj added
|
|
* Update README.md
|
|
itv_intersection, redefine prev_of_itv and itv_decompose using lersif, extend itv_rewrite, simplify proofs (#271)
|
|
Namely:
-projection-no-head-constant
-redundant-canonical-projection
-notation-overridden
|
|
|
|
* Add some theorems on lersif and intervals
* Add more theorems on lersif
* Remove needless parens
* ChangeLog
* Move lersifN
* Add lersif_anti
|
|
* Update INSTALL.md for installing mathcomp as local opam packages
This patch documents the change 1046da99d22462d6aeb23dd12043c2537f47abf1
that was required by the GitLab CI setup to be able to rely on opam 2.0.
Close #251
* Propose to bump the required version of coq in coq-mathcomp-ssreflect.opam
so the CI could use the Docker image coqorg/coq:8.9 (which is already available
albeit it currently is a synonymous of coqorg/coq:8.9-beta1 with the opam repos
coq-released + coq-core-dev + coq-extra-dev)
* [ci] Add math-comp/odd-order and coq-community/lemma-overloading jobs
Related: math-comp/math-comp#245 and math-comp/math-comp#256
|
|
|
|
Setup Docker-based configuration for GitLab CI
|
|
|
|
* This job is only instantiated with coqorg/coq:latest
* Add the associated Dockerfile.make
|
|
|
|
* Install coq-mathcomp-character in only 1 switch (cf. the build-arg $compiler)
* Remove the other switch
* Base the final image on coqorg/base:bare (which has no OCaml compiler layers)
|
|
* Design:
- build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.6 .)
- choice of the OCaml compiler: var OPAM_SWITCH in {base, edge}
(Dockerfile containing: "opam switch set $compiler && eval $(opam env)")
- master (protected branch) => push on GitLab registry and Docker Hub
- other branches (not tags) => push on GitLab registry
- Todo: GitHub PRs => push on GitLab
- test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.6)
- script template foreach project (custom CONTRIB_URL, script)
- jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION)
* Config for protected branches:
- set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN
* Remark:
- The name chosen for branches should ideally yield different values
of CI_COMMIT_REF_SLUG.
- But this is not mandatory as image tags start with "${CI_PIPELINE_IID}_".
cf. doc:
- CI_COMMIT_REF_NAME: The branch or tag name for which project is built.
- CI_COMMIT_REF_SLUG: $CI_COMMIT_REF_NAME lowercased, shortened to 63 bytes,
and with everything except 0-9 and a-z replaced with -.
No leading / trailing -. Use in URLs, host names and domain names.
- CI_PIPELINE_IID: The unique id of the current pipeline scoped to project.
|
|
|
|
|
|
"""
Failed checks on coq-mathcomp-ssreflect package definition from source
at file:///home/coq/mathcomp/ssreflect:
error 57: Synopsis and description must not be both empty
"""
|
|
* (Update make's path accordingly)
* This patch is required for opam 2.0 pinning
* As a result, these *.opam files are now similar to the opam files in
https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-mathcomp-*/coq-mathcomp-*.dev/
|
|
swap mingroup / maxgroup arguments
|
|
|
|
Moved set argument before predicate argument for mingroup and maxgroup
because Coq only displays notation with identifier parameters that are
both bound and free if there is at least one free occurrence to the
left of the binder.
|
|
Correct and improve implicits and documentation of MatrixGenField; also corrects changes in #262 to allow for a compatible fix in `odd-order`.
|
|
Refactored and completed implicit and scope signatures of constants of
MatrixGenField, the module that contains the construction of an
extension field for an irreducible representation, and for decidability
definitions.
Completed and corrected some errors in the corresponding header
documentation.
|
