Skip to content

math-comp/trajectories

Repository files navigation

Trajectories

Docker CI

TODO

Meta

Building and installation instructions

The easiest way to install the latest released version of Trajectories is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-trajectories

To instead build and install manually, do:

git clone https://github.com/math-comp/trajectories.git
cd trajectories
make   # or make -j <number-of-cores-on-your-machine> 
make install

Disclaimer

TODO

Documentation

tentative update of https://gitlab.inria.fr/bertot/cadcoq

references:

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