Skip to content
Snippets Groups Projects
Commit f00c59c3 authored by Pierre Courtieu's avatar Pierre Courtieu
Browse files

Merge branch 'master' into public

parents bbf5d22a 5ad4ea70
No related branches found
No related tags found
No related merge requests found
The following people have contrinuted to the Pactole library. See also The following people have contributed to the development of the Pactole library during the indicated periods of time:
the LICENSE file.
Cédric Auger (2013)
Thibaut Balabonski (2016-2017)
Sebastien Bouchard (2021-)
Pierre Courtieu (2013-)
Robin Pelle (2016-2020)
Lionel Rieg (2014-)
Xavier Urbain (2013-)
- Cédric Auger (2013)
- Thibaut Balabonski (2016-2017)
- Sebastien Bouchard (2021- now)
- Pierre Courtieu (2013- now)
- Robin Pelle (2016-2020)
- Lionel Rieg (2014- now)
- Xavier Urbain (2013-now)
# Contributing The fundamental principle is that the MASTER branch must remain compilable at all times and should never contain incomplete developments.
The golden rule is that **MASTER SHOULD COMPILE AT ALL TIME** and does not Development work on the master branch must be avoided. Instead, each feature or topic should have its own dedicated branch. Developers should create new branches as needed, and all work—including collaborative efforts—should occur within these topic-specific branches.
contain in-progress developments.
More precisely, development never happens on master: each topic should have Before merging changes into master, ensure that your code:
its own branch (feel free to create one if needed) and work happens there,
even when several people are involved.
Once a set of changes (e.g. a new case study) is complete and polished enough - Is complete and thoroughly tested
(comments, adequate identation, no use of generated hypothesis names, etc.), - Contains clear and comprehensive comments
you may merge it to master by squashing its commits into meaningful pieces - Features proper indentation
(only a few, usually one may be enough) or submit a pull request. - Uses descriptive hypothesis names rather than auto-generated ones
- Meets all project quality standards
When your changes are ready (such as a completed case study), you have two options:
1. Submit a pull request for review
2. Merge directly into master after squashing your commits into meaningful, well-organized units (typically one or a few commits that clearly represent the changes)
{ {
"@context": "https://doi.org/10.5063/schema/codemeta-2.0", "@context": "https://w3id.org/codemeta/3.0",
"@type": "SoftwareSourceCode", "type": "SoftwareSourceCode",
"name": "Pactole", "applicationCategory": "Coq library dedicated to formal verification of mobile robotic swarm distributed protocols",
"license": "https://spdx.org/licenses/LGPL-3.0",
"codeRepository": "https://gitlab.liris.cnrs.fr/pactole/coq-pactole",
"relatedLink": "TODO? https://???",
"dateCreated": "TODO 2013-??-??",
"datePublished": "TODO 2024-???",
"version": "TODO 2.0???",
"description": "TODO A Coq library formalizing the distributed computing model for robot swarm called Look-Compute-Move (due to Suzuki and Yamashita) and several case studies in this model. ",
"applicationCategory": "FIXME: Formal development",
"releaseNotes": "TODO Second release.",
"runtimePlatform": "Coq-8.20",
"developmentStatus": "active",
"funding": [
{ "@type":"Grant",
"identifier": "Digiteo Project #2009-38HD" } ,
{ "@type":"Grant",
"identifier": "ANR Project 2019-CE25-0005" }
],
"keywords": [
"distributed systems",
"formal proof",
"robot swarm"
],
"programmingLanguage": [
"Coq/Rocq"
],
"runtimePlatform": [
"Coq/Rocq"
],
"author": [ "author": [
{ {
"@type": "Person", "id": "https://orcid.org/0000-0001-8789-9781",
"@id": "https://orcid.org/0000-0001-8789-9781", "type": "Person",
"givenName": "Pierre",
"familyName": "Courtieu",
"email": "Pierre.Courtieu@lecnam.net",
"affiliation": { "affiliation": {
"@type": "Organization", "type": "Organization",
"name": "Conservatoire National des Arts et Métiers" "name": "Conservatoire National des Arts et Métiers"
} },
"email": "Pierre.Courtieu@lecnam.net",
"familyName": "Courtieu",
"givenName": "Pierre"
}, },
{ {
"@type": "Person", "id": "https://orcid.org/0000-0001-7442-2538",
"@id": "https://orcid.org/0000-0001-7442-2538", "type": "Person",
"givenName": "Xavier",
"familyName": "Urbain",
"email": "Xavier.Urbain@univ-lyon1.fr",
"affiliation": { "affiliation": {
"@type": "Organization", "type": "Organization",
"name": "Université Claude Bernard Lyon 1" "name": "Université Claude Bernard Lyon 1"
} },
} "email": "Xavier.Urbain@univ-lyon1.fr",
"familyName": "Urbain",
"givenName": "Xavier"
},
{ {
"@type": "Person", "id": "_:author_3",
"givenName": "Lionel", "type": "Person",
"familyName": "Rieg",
"email": "lionel.rieg@univ-grenoble-alpes.fr",
"affiliation": { "affiliation": {
"@type": "Organization", "type": "Organization",
"name": "Verimag, Grenoble INP -- UGA" "name": "Verimag, Grenoble INP -- UGA"
} },
"email": "lionel.rieg@univ-grenoble-alpes.fr",
"familyName": "Rieg",
"givenName": "Lionel"
} }
], ],
"contributor": "TODO: Les stagiaires comme ci-dessus?", "codeRepository": "https://gitlab.liris.cnrs.fr/pactole/coq-pactole",
"citation": "TODO un papier décrivant Pactole" "description": "A Coq library dedicated to formally verifying distributed protocols for mobile robot swarms. The library implements various extensions of the Look-Compute-Move model, first proposed by Suzuki and Yamashita, providing a robust framework for protocol verification in different theoretical settings. ",
"keywords": [
"distributed systems",
"deductive verification",
"formal proof",
"robotic swarms"
],
"license": "https://spdx.org/licenses/LGPL-3.0",
"name": "Pactole",
"programmingLanguage": "Coq/Rocq",
"relatedLink": "https://pactole.liris.cnrs.fr/",
"runtimePlatform": "Coq-8.20",
"version": "2.1",
"developmentStatus": "active",
"funding": "Digiteo Project #2009-38HD, ANR Project 2019-CE25-0005",
"referencePublication": "https://doi.org/10.4230/LITES.8.2.2"
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment