diff --git a/INSTALL.md b/INSTALL.md new file mode 100644 index 0000000000000000000000000000000000000000..1d7367e4b0694976bd6ebbc2c51f603f6dacffaf --- /dev/null +++ b/INSTALL.md @@ -0,0 +1,117 @@ + +# Requirements + +- Coq 8.19 or 8.20 (including the executable `coqc`, `codep`, `coq_makefile`) +- GNU `make` + +# Configuration + +You should perform once the following command to generate the Makefile: + +```bash +coq_makefile -f _CoqProject -o Makefile +``` + +# Compilation + +To compile the whole projet including case studies: + +``` bash +make +``` + +# Use in your coq development + +Suppose you have compiled Pactole in a directory calle `pactole` and +you want to use it in your own development called `myproject`. You +should use a `_CoqProject` file containing: + +``` +-Q pactole Pactole +.. # your own project options +``` + +and use `coq_makefile -f _CoqProject -o Makefile` to generate your +makefile. Note that ProofGeneral and other IDE also read the +`_CoqProject`. + +From now on you can use Pactole in your coq files by importing the +relevant modules, e.g.: + +``` coq +Require Import Pactole.Core.Formalism. +``` + +See the file README.md for the directory structure of the library. + +# NOTES FOR DEVELOPPERS + +Pactole provides fast (and unsafe) compilation target. This is +explained in this section. + + +## build (slow) + +The default makefile target may take more than 10mn to compile due to +some case studies. You may want to comment them in the _CoqProject +file before the configure step above if you are not interested in +these case studies. Another solution is to follow the fast compilation +recipes below. + +Doing this once a week when developing is good practice. This is the +only way to make a really safe compilation including all +xxx_Assumption.v. You should always do this once in a while to make +sure some universe constraints aren't failing and to check if you did +not miss any remaining axiom. + +But during the development process this makes the compilation when +switching between files too slow. Hence the following less safe +compilation processes: + +## unsafe builds when developing + +During development you can benefit from coq's "vos/vok" generation to +speed up compilation. The only specificity of Pactole concerns +compilation of the files named xxx_Assumptions.v. This files print the +sets of assumptions used in the proofs of final lemmas in Case +studies. Compiling these files for vos/vok target would raise errors. +We provide adapted targets below. + +## build (slow, almost safe, but very parallelisable) + +``` +make [-j] vok +``` +or better when developing +``` +make [-j] vok-nocheck +``` +Doing this once a day when developing is good practice. + +## build (Very fast, unsafe) + +``` +make [-j] vos +``` +or better when developing +``` +make [-j] vos-nocheck +``` + +This should be your prefered way of compiling when developing. It is +much faster. It is unsafe but in most situations no bad surprise is to +be expected. + +You should do real compilations from time to time as explained above. + +## Proofgeneral + +For easy use of this feature (vos) you can use the auto compilation +feature of proofgeneral. menu: + +menu: Coq / Auto Compilation / Compile Before Require +and then: Coq / Auto Compilation / vos compilation + +Now you can transparently script in any buffer, all needed file will +be compiled quickly. Don't forget to make a big fat "make" from time +to time. diff --git a/README.md b/README.md index 2d061f24ae3280865bd97cebe60979ac9251ab70..79eb9c6973f11af768edde8823595f882a5fb121 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,10 @@ # Content -This repository stores the Coq code of the Pactole project, dedicated -to formal verification of mobile robotic swarm protocols in many -variants of the model initially proposed by Suzuki and Yamashita [1] -and sometimes called the "look-compute-move model". +This repository stores the Coq code of the Pactole +(https://pactole.liris.cnrs.fr/) project, dedicated to formal +verification of mobile robotic swarm protocols in many variants of the +model initially proposed by Suzuki and Yamashita [1] and sometimes +called the "look-compute-move model". It contains a very abstract and parametrized formal model and a lot of case studies. The structure of the repository is describe below. @@ -12,10 +13,10 @@ case studies. The structure of the repository is describe below. It was financially supported by the following propject: -- The Pactole project started as Digiteo Project #2009-38HD. -- SAPPORO is funded by the French National Research Agency (ANR) under - the reference 2019-CE25-0005 - +- [The Pactole project](https://pactole.liris.cnrs.fr/) started as + Digiteo Project #2009-38HD. +- [SAPPORO](https://sapporo.liris.cnrs.fr/) is funded by the French + National Research Agency (ANR) under the reference 2019-CE25-0005 [1] I. Suzuki and M. Yamashita. Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM Journal of Computing, 28(4):1347–1363, 1999. @@ -28,89 +29,46 @@ It was financially supported by the following propject: - *Spaces/*: Spaces in which robots evolve - *Observations/*: Types of robot views of the configuration - *Models/*: Additional properties of some models -- *CasesStudies/* - - *Convergence/*: Convergence of robots in the 2D Euclidean plane - - *Gathering/*: Gathering in R or R² for various models - - *Exploration/*: Exploration of a ring with stop - - *LifeLine/*: Life line connection in the 2D Euclidean plane - -# Compilation - -## configure - -``` -coq_makefile -f _CoqProject -o Makefile -``` - -See below for faster compilation. - -## build (slow) - -``` -make -``` - -Be aware this may take more than 10mn to compile due to some case -studies. You may want to comment them in the _CoqProject file before -the configure step above if you are not interested in these case -studies. Another solution is to follow the fast compilation recipes -below. - -Doing this once a week when developing is good practice. This is the -only way to make a really safe compilation including all -xxx_Assumption.v. You should always do this once in a while to make -sure some universe constraints aren't failing and to check if you did -not miss any remaining axiom. - -But during the development process this makes the compilation when -switching between files too slow. Hence the following less safe -compilation processes: - -## unsafe builds when developing - -During development you can benefit from coq's "vos/vok" generation to -speed up compilation. The only specificity of Pactole concerns -compilation of the files named xxx_Assumptions.v. This files print the -sets of assumptions used in the proofs of final lemmas in Case -studies. Compiling these files for vos/vok target would raise errors. -We provide adapted targets below. - -## build (slow, almost safe, but very parallelisable) - -``` -make [-j] vok -``` -or better when developing -``` -make [-j] vok-nocheck -``` -Doing this once a day when developing is good practice. - -## build (Very fast, unsafe) - - -``` -make [-j] vos -``` -or better when developing -``` -make [-j] vos-nocheck -``` - -This should be your prefered way of compiling when developing. It is -much faster. It is unsafe but in most situations no bad surprise is to -be expected. - -You should do real compilations from time to time as explained above. - -## Proofgeneral - -For easy use of this feature (vos) you can use the auto compilation -feature of proofgeneral. menu: - -menu: Coq / Auto Compilation / Compile Before Require -and then: Coq / Auto Compilation / vos compilation - -Now you can transparently script in any buffer, all needed file will -be compiled quickly. Don't forget to make a big fat "make" from time -to time. +- *CaseStudies/* : Case studies + +# Case Studies + +The directory `CaseStudies` contains the following the following case +studies. Each case study (say `casestudy.v`) has a companion file +called `casestudy_Assuptions.v` whose only purpose is to call `Print +Assumption` on the main theorem of the case study. The reason why this +command is not included in the case study itself is for allowing fast +compilation of the case study. + +Here is a list of the current case studies: + +- Convergence/: Convergence of robots in the 2D Euclidean plane + - [Algorithm_noB.v](CaseStudies/Convergence/Algorithm_noB.v) + - Impossibility_2G_1B.v +- Gathering/: Gathering in R or R² for various models + - Impossibility.v: + - Definitions.v: Common definitions about the gathering problem + - WithMultiplicity.v + - InR/ case studies for the gathering on the enclidean line + - Impossibility.v + - Algorithm.v + - InR2/ case studies for the gathering on the enclidean plane + - Peleg.v + - Viglietta.v + - FSyncFlexNoMultAlgorithm.v + - Algorithm.v + - Algorithm_Assumptions.v +- Exploration/: Exploration of a ring with stop + - ImpossibilityKDividesN.v + - ExplorationDefs.v + - Tower.v +- LifeLine/: Life line connection in the 2D Euclidean plane + - Algorithm.v + +# Other Related Ressources + +A general description of the Pactole library and its use: + + Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Swarms of Mobile Robots: Towards + Versatility with Safety. Leibniz Transactions on Embedded Systems, 8(2):02:1– + 02:36, 2022.