-
Notifications
You must be signed in to change notification settings - Fork 2
/
meta.yml
146 lines (125 loc) · 4.38 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
fullname: Formal Foundations for Modeling Robot Manipulators
shortname: robot
organization: affeldt-aist
opam_name: coq-robot
community: false
action: true
coqdoc: false
synopsis: >-
Formal Foundations for Modeling Robot Manipulators
description: |-
This repository contains an experimental library for the mathematics
of rigid body transformations using the Coq proof-assistant and the
Mathematical Components library.
authors:
- name: Reynald Affeldt, AIST
initial: true
- name: Cyril Cohen, Inria
initial: true
- name: Laurent Théry, Inria
initial: false
opam-file-maintainer: Reynald Affeldt <reynald.affeldt@aist.go.jp>
#opam-file-version: dev
license:
fullname: LGPL-2.1-or-later
identifier: LGPL-2.1-or-later
file: LICENSE
supported_coq_versions:
text: Coq 8.14 to Coq 8.18
opam: '{ (>= "8.14" & < "8.19~") | (= "dev") }'
tested_coq_opam_versions:
- 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.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.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.14.0" & < "1.19~") }'
description: |-
[MathComp ssreflect](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
version: '{ (>= "1.14.0" & < "1.19~") }'
description: |-
[MathComp fingroup](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
version: '{ (>= "1.14.0" & < "1.19~") }'
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-mathcomp-solvable
version: '{ (>= "1.14.0" & < "1.19~") }'
description: |-
[MathComp solvable](https://math-comp.github.io)
- opam:
name: coq-mathcomp-field
version: '{ (>= "1.14.0" & < "1.19~") }'
description: |-
[MathComp field](https://math-comp.github.io)
- opam:
name: coq-mathcomp-analysis
version: '{ (>= "0.6.0" & < "0.7~") }'
description: |-
[MathComp analysis](https://github.com/math-comp/analysis)
- opam:
name: coq-mathcomp-real-closed
version: '{ (>= "1.1.3") }'
description: |-
[MathComp real closed](https://github.com/math-comp/real-closed)
namespace: robot
keywords:
- name: robotics
- name: 3D geometry
publications:
- pub_url: https://staff.aist.go.jp/reynald.affeldt/documents/robot_cpp_long.pdf
pub_title: Formal foundations of 3D geometry to model robot manipulators
pub_doi: 10.1145/3018610.3018629
documentation: |-
## Acknowledgments
Contribution by Damien Rouhling (9b7badc25bf6492f6b84611c7f9d32594b345308)
Grant-in-Aid for Scientific Research Number 15H02687
## Disclaimer
This library is still at an experimental stage. Contents may change
and definitions and theorems may be renamed. Use at your own risk.
## Documentation
This library can be used to address the forward kinematics problem
of robot manipulators. It contains theories for angles,
three-dimensional geometry (including three-dimensional rotations,
skew-symmetric matrices, quaternions), rigid body transformations
(isometries, homogeneous representation, Denavit-Hartenberg
convention, screw motions), and an application to the SCARA robot
manipulator.
Each file is documented more precisely in its header.
Some references used in this work:
- [murray] Murray, Li, Shankar Sastry: A Mathematical Introduction to Robotic Manipulation
- [springer] Siciliano, Khatib (Eds.): Springer Handbook of Robotics
- [angeles] Angeles: Fundamentals of Robotic Mechanical Systems, Springer 2014
- [oneill] O'Neill: Elementary Differential Geometry
- [spong] Spong, Hutchinson, Vidyasagar: Robot Modeling and Control
- [sciavicco] Sciavicco, L., Siciliano, B.: Modelling and Control of Robot Manipulators, Springer 2000
- [bottema] Bottema, O., Roth, B.: Theoretical Kinematics, Dover 1990
## Original License
Before [2021-04-29], coq-robot was distributed under the terms of the
`LGPL-3.0` license.