Coq 8.20, rm infra.v, minor fixes

.github/workflows/docker-action.yml

@@ -17,16 +17,15 @@ jobs:
     strategy:
       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

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)
@@ -39,8 +29,8 @@ A demonstration version is available at
   - [MathComp field 2.2.0 or later](https://math-comp.github.io)
   - [Mathcomp real closed 2.0.0 or later](https://github.com/math-comp/real-closed/)
   - [Algebra tactics 1.2.0 or later](https://github.com/math-comp/algebra-tactics)
-  - [MathComp analysis 1.0.0 or later](https://github.com/math-comp/analysis)
-  - [Infotheo 0.7.0 of later](https://github.com/affeldt-aist/infotheo)
+  - [MathComp analysis 1.9.0 or later](https://github.com/math-comp/analysis)
+  - [Infotheo 0.9.1 of later](https://github.com/affeldt-aist/infotheo)
 - Coq namespace: `mathcomp.trajectories`
 - Related publication(s):
   - [Safe Smooth Paths between Straight Line Obstacles](https://inria.hal.science/hal-04312815) doi:[https://doi.org/10.1007/978-3-031-61716-4_3](https://doi.org/https://doi.org/10.1007/978-3-031-61716-4_3)

_CoqProject

@@ -9,7 +9,6 @@ theories/civt.v
 theories/desc.v
 theories/desc1.v
 theories/desc2.v
-theories/infra.v
 theories/bern.v
 theories/bern5.v
 theories/casteljau.v

coq-mathcomp-trajectories.opam

@@ -14,19 +14,19 @@ synopsis: "Trajectories"
 description: """
 TODO"""
 
-build: [make "-j%{jobs}%"]
+build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.17" & < "8.20~") | (= "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") }
   "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-real-closed" { (>= "2.0.0") | (= "dev") }
   "coq-mathcomp-algebra-tactics" { (>= "1.2.0") | (= "dev") }
-  "coq-mathcomp-analysis" { (>= "1.0.0") }
-  "coq-infotheo" { >= "0.7.0"}
+  "coq-mathcomp-analysis" { (>= "1.9.0") }
+  "coq-infotheo" { >= "0.9.1"}
 ]
 
 tags: [

meta.yml

@@ -27,11 +27,11 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq >= 8.17, MathComp >= 2.2.0
-  opam: '{ (>= "8.17" & < "8.20~") | (= "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'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
@@ -72,14 +72,14 @@ dependencies:
     [Algebra tactics 1.2.0 or later](https://github.com/math-comp/algebra-tactics)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.0.0") }'
+    version: '{ (>= "1.9.0") }'
   description: |-
-    [MathComp analysis 1.0.0 or later](https://github.com/math-comp/analysis)
+    [MathComp analysis 1.9.0 or later](https://github.com/math-comp/analysis)
 - opam:
     name: coq-infotheo
-    version: '{ >= "0.7.0"}'
+    version: '{ >= "0.9.1"}'
   description: |-
-    [Infotheo 0.7.0 of later](https://github.com/affeldt-aist/infotheo)
+    [Infotheo 0.9.1 of later](https://github.com/affeldt-aist/infotheo)
 
 namespace: mathcomp.trajectories
 

theories/cells_alg.v

@@ -4959,7 +4959,7 @@ Record common_invariant bottom top edge_set s
      lexePt (point (head dummy_event events)) (right_pt g)}
 }.
 
-Record common_non_gp_invariant bottom top edge_set s 
+Record common_non_gp_invariant bottom top edge_set s
   (all_events processed_events events : seq event) :=
   { ngcomm : common_invariant bottom top edge_set s all_events
     processed_events events;