add Coq.8.20 and MathComp 2.3.0 to the CI

math-comp · Feb 19, 2025 · 0f7590b · 0f7590b
1 parent 46e028f
commit 0f7590b
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 21 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -18,15 +18,15 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v2
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-mathcomp-trajectories.opam'
           custom_image: ${{ matrix.image }}
 
-
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/README.md b/README.md
@@ -6,31 +6,21 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/math-comp/trajectories/actions/workflows/docker-action.yml/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/trajectories/actions/workflows/docker-action.yml
+[docker-action-shield]: https://github.com/math-comp/trajectories/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/trajectories/actions?query=workflow:"Docker%20CI"
 
-This directory contain a variety of developments that were  thought to be
-useful for the computation of trajectories between obstacles.
 
-The leading example relies on a decomposition of a plane area in vertical
-cells, which gives a graph whose nodes are the cells.  The next step is to
-compute a path in this graph, from which a piecewise straight line
-trajectory is computed, which is guaranted to stay inside the safe cells, or
-to go from one cell to a neighbor only through a safe crossing.  The final
-step is to smoothen the trajectory, by using Bezier curves for which checks
-are performed to verify that they stay within the safe part of the area.
 
-A demonstration version is available at 
-[this page](https://stamp.gitlabpages.inria.fr/trajectories.html).
 
+TODO
 
 ## Meta
 
 - Author(s):
   - Reynald Affeldt (initial)
   - Yves Bertot (initial)
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq >= 8.17, MathComp >= 2.2.0
+- Compatible Coq versions: Coq >= 8.19, MathComp >= 2.2.0
 - Additional dependencies:
   - [MathComp ssreflect 2.2.0 or later](https://math-comp.github.io)
   - [MathComp fingroup 2.2.0 or later](https://math-comp.github.io)
@@ -65,6 +55,19 @@ make install
 ```
 
 
+This directory contain a variety of developments that were  thought to be
+useful for the computation of trajectories between obstacles.
+
+The leading example relies on a decomposition of a plane area in vertical
+cells, which gives a graph whose nodes are the cells.  The next step is to
+compute a path in this graph, from which a piecewise straight line
+trajectory is computed, which is guaranted to stay inside the safe cells, or
+to go from one cell to a neighbor only through a safe crossing.  The final
+step is to smoothen the trajectory, by using Bezier curves for which checks
+are performed to verify that they stay within the safe part of the area.
+
+A demonstration version is available at [this page](https://stamp.gitlabpages.inria.fr/trajectories.html).
+
 ## Disclaimer
 
 TODO

diff --git a/coq-mathcomp-trajectories.opam b/coq-mathcomp-trajectories.opam
@@ -14,10 +14,10 @@ synopsis: "Trajectories"
 description: """
 TODO"""
 
-build: [make "-j%{jobs}%"]
+build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.17" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") }

diff --git a/meta.yml b/meta.yml
@@ -27,12 +27,14 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq >= 8.17, MathComp >= 2.2.0
-  opam: '{ (>= "8.17" & < "8.21~") | (= "dev") }'
+  text: Coq >= 8.19, MathComp >= 2.2.0
+  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
@@ -95,8 +97,21 @@ publications:
   pub_doi: https://doi.org/10.1007/978-3-031-61716-4_3
 
 documentation: |-
-  ## Disclaimer
+  This directory contain a variety of developments that were  thought to be
+  useful for the computation of trajectories between obstacles.
  
+  The leading example relies on a decomposition of a plane area in vertical
+  cells, which gives a graph whose nodes are the cells.  The next step is to
+  compute a path in this graph, from which a piecewise straight line
+  trajectory is computed, which is guaranted to stay inside the safe cells, or
+  to go from one cell to a neighbor only through a safe crossing.  The final
+  step is to smoothen the trajectory, by using Bezier curves for which checks
+  are performed to verify that they stay within the safe part of the area.
+
+  A demonstration version is available at [this page](https://stamp.gitlabpages.inria.fr/trajectories.html).
+
+  ## Disclaimer
+
   TODO
 
   ## Documentation