-
Notifications
You must be signed in to change notification settings - Fork 4
/
meta.yml
149 lines (123 loc) · 4.21 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
fullname: Trajectories
shortname: trajectories
organization: math-comp
opam_name: coq-mathcomp-trajectories
community: false
action: true
nix: false
coqdoc: false
synopsis: >-
Trajectories
description: |-
TODO
authors:
- name: Reynald Affeldt
initial: true
- name: Yves Bertot
initial: true
opam-file-maintainer: Reynald Affeldt <reynald.affeldt@aist.go.jp>
opam-file-version: dev
license:
fullname: CeCILL-C
identifier: CECILL-C
file: LICENSE
supported_coq_versions:
text: Coq >= 8.17, MathComp >= 2.2.0
opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }'
tested_coq_opam_versions:
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp ssreflect 2.2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp fingroup 2.2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp algebra 2.2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-solvable
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp solvable 2.2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-field
version: '{ (>= "2.2.0") | (= "dev") }'
description: |-
[MathComp field 2.2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-real-closed
version: '{ (>= "2.0.0") | (= "dev") }'
description: |-
[Mathcomp real closed 2.0.0 or later](https://github.com/math-comp/real-closed/)
- opam:
name: coq-mathcomp-algebra-tactics
version: '{ (>= "1.2.0") | (= "dev") }'
description: |-
[Algebra tactics 1.2.0 or later](https://github.com/math-comp/algebra-tactics)
- opam:
name: coq-mathcomp-analysis
version: '{ (>= "1.0.0") }'
description: |-
[MathComp analysis 1.0.0 or later](https://github.com/math-comp/analysis)
- opam:
name: coq-infotheo
version: '{ >= "0.7.0"}'
description: |-
[Infotheo 0.7.0 of later](https://github.com/affeldt-aist/infotheo)
namespace: mathcomp.trajectories
keywords:
- name: trajectories
categories:
- name: Mathematics/Real Calculus and Topology
publications:
- pub_url: https://inria.hal.science/hal-04312815
pub_title: Safe Smooth Paths between Straight Line Obstacles
pub_doi: https://doi.org/10.1007/978-3-031-61716-4_3
documentation: |-
## Disclaimer
TODO
## Documentation
tentative update of https://gitlab.inria.fr/bertot/cadcoq
references:
- Root Isolation for one-variable polynomials (2010)
https://wiki.portal.chalmers.se/cse/uploads/ForMath/rootisol
- A formal study of Bernstein coefficients and polynomials (2010)
https://hal.inria.fr/inria-00503017v2/document
- Theorem of three circles in Coq (2013)
https://arxiv.org/abs/1306.0783
- Safe Smooth Paths between straight line obstacles
https://inria.hal.science/hal-04312815
https://link.springer.com/chapter/10.1007/978-3-031-61716-4_3
## Development information
On April 2, 2023, a file `smooth_trajectories.v` was added to illustrate a
program to compute smooth trajectories for a "point" between obstacles given
by straight edges.
The example can be played with by changing the contents of variables
`example_bottom`, `example_top`, `example_edge_list`, and changing
the coordinates of points given as argument to `example_test` in the
`Compute` command that appears at the end of the file. This compute
commands produces text that should be placed in a postscript file and
can be displayed with any postscript enabled viewer. A perl-script is
provided to produce this, so that the following command is a handy
way to produce example outputs:
```
(cd theories; ./run_tests.sh)
```
At the time of writing this paragraph, the code seems complete but
many bugs have been found in parts of the code that have not been proved
formally.
If you play with this code and you obtain a trajectory that obviously
crosses the given edges, please report.
## Previous work reused at the time of the first releases
TODO
## Acknowledgments
TODO