From b1e910ba0de6bbbe8f2f9f28d7188a2a6e728a31 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 1 Jan 2024 17:27:13 +0900 Subject: [PATCH] update --- .github/workflows/docker-action.yml | 23 ++++++++++- README.md | 2 +- coq-robot.opam | 14 +++---- derive_matrix.v | 19 ++------- differential_kinematics.v | 4 +- meta.yml | 62 +++++++++++++++++++++++------ 6 files changed, 84 insertions(+), 40 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index ce2f37d..26d0309 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,12 +17,31 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.13.0-coq-8.14' - - 'mathcomp/mathcomp:1.13.0-coq-8.15' - 'mathcomp/mathcomp:1.14.0-coq-8.14' - 'mathcomp/mathcomp:1.14.0-coq-8.15' + - 'mathcomp/mathcomp:1.14.0-coq-8.16' + - 'mathcomp/mathcomp:1.14.0-coq-8.17' + - 'mathcomp/mathcomp:1.14.0-coq-8.18' - 'mathcomp/mathcomp:1.15.0-coq-8.14' - 'mathcomp/mathcomp:1.15.0-coq-8.15' + - 'mathcomp/mathcomp:1.15.0-coq-8.16' + - 'mathcomp/mathcomp:1.15.0-coq-8.17' + - 'mathcomp/mathcomp:1.15.0-coq-8.18' + - 'mathcomp/mathcomp:1.16.0-coq-8.14' + - 'mathcomp/mathcomp:1.16.0-coq-8.15' + - 'mathcomp/mathcomp:1.16.0-coq-8.16' + - 'mathcomp/mathcomp:1.16.0-coq-8.17' + - 'mathcomp/mathcomp:1.16.0-coq-8.18' + - 'mathcomp/mathcomp:1.17.0-coq-8.14' + - 'mathcomp/mathcomp:1.17.0-coq-8.15' + - 'mathcomp/mathcomp:1.17.0-coq-8.16' + - 'mathcomp/mathcomp:1.17.0-coq-8.17' + - 'mathcomp/mathcomp:1.17.0-coq-8.18' + - 'mathcomp/mathcomp:1.18.0-coq-8.14' + - 'mathcomp/mathcomp:1.18.0-coq-8.15' + - 'mathcomp/mathcomp:1.18.0-coq-8.16' + - 'mathcomp/mathcomp:1.18.0-coq-8.17' + - 'mathcomp/mathcomp:1.18.0-coq-8.18' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index 322d8bd..f38ba8f 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,7 @@ Mathematical Components library. - Cyril Cohen, Inria (initial) - Laurent Théry, Inria - License: [LGPL-2.1-or-later](LICENSE) -- Compatible Coq versions: Coq 8.14 to Coq 8.15 +- Compatible Coq versions: Coq 8.14 to Coq 8.18 - Additional dependencies: - [MathComp ssreflect](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) diff --git a/coq-robot.opam b/coq-robot.opam index caad4fe..760c09c 100644 --- a/coq-robot.opam +++ b/coq-robot.opam @@ -19,13 +19,13 @@ Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.14" & < "8.16~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-field" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-analysis" { (>= "0.5.0" & < "0.6~") } + "coq" { (>= "8.14" & < "8.19~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-field" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-analysis" { (>= "0.6.0" & < "0.7~") } "coq-mathcomp-real-closed" { (>= "1.1.3") } ] diff --git a/derive_matrix.v b/derive_matrix.v index 2efe6f1..35ea089 100644 --- a/derive_matrix.v +++ b/derive_matrix.v @@ -2,9 +2,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat. From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp. From mathcomp Require Import realalg complex fingroup perm. -From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed. -From mathcomp.analysis Require Import topology normedtype landau forms derive. -From mathcomp.analysis Require Import functions. +From mathcomp Require Import boolp reals Rstruct classical_sets signed. +From mathcomp Require Import topology normedtype landau forms derive. +From mathcomp Require Import functions. Require Import ssr_ext euclidean rigid skew. (******************************************************************************) @@ -22,19 +22,6 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. -(* NB: PR to analysis in progress *) -Lemma derive1_cst (R : numFieldType) (V : normedModType R) (k : V) t : - (cst k)^`() t = 0. -Proof. by rewrite derive1E derive_val. Qed. - -(* TODO: see coord_continuous in normedtype.v *) -Lemma coord_continuous (R : numDomainType) (K : normedModType R) m n i j : - continuous (fun M : 'M[K]_(m, n) => M i j). -Proof. -move=> /= M s /= /nbhs_normP => -[e e0 es]. -by apply/nbhs_ballP; exists e => //= N MN; exact/es/MN. -Qed. - Lemma mx_lin1N (R : ringType) n (M : 'M[R]_n) : mx_lin1 (- M) = -1 \*: mx_lin1 M :> ( _ -> _). Proof. by rewrite funeqE => v /=; rewrite scaleN1r mulmxN. Qed. diff --git a/differential_kinematics.v b/differential_kinematics.v index 7831a5b..5c0328c 100644 --- a/differential_kinematics.v +++ b/differential_kinematics.v @@ -2,8 +2,8 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat. From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp. From mathcomp Require Import realalg complex fingroup perm. -From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed. -From mathcomp.analysis Require Import topology normedtype landau forms derive. +From mathcomp Require Import boolp reals Rstruct classical_sets signed. +From mathcomp Require Import topology normedtype landau forms derive. From mathcomp Require Import functions. Require Import ssr_ext derive_matrix euclidean frame rot skew rigid. diff --git a/meta.yml b/meta.yml index 9b72129..40144c2 100644 --- a/meta.yml +++ b/meta.yml @@ -30,52 +30,90 @@ license: file: LICENSE supported_coq_versions: - text: Coq 8.14 to Coq 8.15 - opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }' + text: Coq 8.14 to Coq 8.18 + opam: '{ (>= "8.14" & < "8.19~") | (= "dev") }' tested_coq_opam_versions: -- version: '1.13.0-coq-8.14' - repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.15' - repo: 'mathcomp/mathcomp' - version: '1.14.0-coq-8.14' repo: 'mathcomp/mathcomp' - version: '1.14.0-coq-8.15' repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.18' + repo: 'mathcomp/mathcomp' - version: '1.15.0-coq-8.14' repo: 'mathcomp/mathcomp' - version: '1.15.0-coq-8.15' repo: 'mathcomp/mathcomp' +- version: '1.15.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.15.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.15.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '1.16.0-coq-8.14' + repo: 'mathcomp/mathcomp' +- version: '1.16.0-coq-8.15' + repo: 'mathcomp/mathcomp' +- version: '1.16.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.16.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.16.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.14' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.15' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.14' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.15' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.18' + repo: 'mathcomp/mathcomp' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp ssreflect](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp fingroup](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp algebra](https://math-comp.github.io) - opam: name: coq-mathcomp-solvable - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp solvable](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-analysis - version: '{ (>= "0.5.0" & < "0.6~") }' + version: '{ (>= "0.6.0" & < "0.7~") }' description: |- [MathComp analysis](https://github.com/math-comp/analysis) - opam: