Add an Opam file

.gitlab-ci.yml

@@ -2,12 +2,21 @@ stages:
   - build
   - process
 
-.build:
+.build-common:
   stage: build
-  image: mathcomp/mathcomp:${CI_JOB_NAME}
   script:
-    - ./create_makefile.sh --without-classic
-    - make -j ${NJOBS}
+    - opam update -y
+    - opam remove -y coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable  # Check coq-mathcomp-ssreflect is enough
+    - opam pin add -n -y -k path coq-prosa .
+    - opam install -y -v -j ${NJOBS} coq-prosa
+
+.build:
+  image: mathcomp/mathcomp:${CI_JOB_NAME}
+  extends: .build-common
+
+.build-dev:
+  image: mathcomp/mathcomp-dev:${CI_JOB_NAME}
+  extends: .build-common
 
 .build-classic:
   stage: build
@@ -44,11 +53,32 @@ stages:
     - "*/*/*/*/*/*/*/*/*/*.glob"
     expire_in: 1 week
 
+1.9.0-coq-8.9:
+  extends: .build
+
 1.9.0-coq-8.10:
   extends:
     - .build
     - .collect-vo-files
 
+1.9.0-coq-8.11:
+  extends:
+    - .build
+    - .collect-vo-files
+
+1.10.0-coq-8.9:
+  extends: .build
+
+1.10.0-coq-8.10:
+  extends:
+    - .build
+    - .collect-vo-files
+
+1.10.0-coq-8.11:
+  extends:
+    - .build
+    - .collect-vo-files
+
 1.9.0-coq-8.10-classic:
   extends:
     - .build-classic
@@ -66,28 +96,26 @@ spell-check:
   script:
     - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
 
-1.9.0-coq-8.9:
-  extends: .build
-
-1.10.0-coq-dev:
+coq-8.10:
   extends:
-    - .build
-  # it's ok to fail with an unreleased version of Coq
+    - .build-dev
+  # it's ok to fail with an unreleased version of ssreflect
   allow_failure: true
 
-latest-coq-8.10:
+coq-dev:
   extends:
-    - .build
-  # it's ok to fail with an unreleased version of ssreflect
+    - .build-dev
+  # it's ok to fail with an unreleased version of ssreflect and Coq
   allow_failure: true
 
 validate:
   stage: process
   image: mathcomp/mathcomp:1.9.0-coq-8.10
   needs: ["1.9.0-coq-8.10"]
-  dependencies:
-    - 1.9.0-coq-8.10
-  script: make validate
+  script:
+    - ./create_makefile.sh
+    - make -j ${NJOBS}
+    - make validate
 
 validate-classic:
   stage: process
@@ -101,6 +129,7 @@ validate-classic:
   stage: process
   image: mathcomp/mathcomp:1.9.0-coq-8.10
   script:
+    - ./create_makefile.sh
     - make html -j ${NJOBS}
     - mv html with-proofs
     - make gallinahtml -j ${NJOBS}

README.md

@@ -33,13 +33,28 @@ All results published prior to 2020 build on this "classic" version of Prosa.
 - [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
 - [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
 
-## Dependencies 
+## Installation
+
+### With OPAM
+
+Prosa can be installed using the [OPAM package manager](https://opam.ocaml.org/) (>= 2.0)
+
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+# or for the dev version (git master): https://coq.inria.fr/opam/extra-dev
+opam update
+opam install coq-prosa
+```
+
+### From sources
+
+#### Dependencies
 
 Besides Coq itself, Prosa's only external dependency is the ssreflect library of the [Mathematical Components project](https://math-comp.github.io).
 
 Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.
 
-## Compiling Prosa
+#### Compiling Prosa
 
 Assuming ssreflect is available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps.
 

coq-prosa.opam

+opam-version: "2.0"
+version: "dev"
+maintainer: "Pierre Roux <pierre.roux@onera.fr>"
+
+homepage: "https://prosa.mpi-sws.org/"
+dev-repo: "git+https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git"
+bug-reports: "https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/issues"
+license: "BSD"
+
+build: [
+  ["./create_makefile.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+depends: [
+  "coq" {((>= "8.9" & < "8.12~") | = "dev")}
+  "coq-mathcomp-ssreflect" {((>= "1.9" & < "1.11~") | = "dev")}
+]
+
+tags: [
+  "keyword:prosa"
+  "keyword:real-time"
+  "keyword:schedulability analysis"
+  "logpath:prosa"
+]
+authors: [
+  "Felipe Cerqueira"
+  "Björn Brandenburg"
+  "Maxime Lesourd"
+  "Sergey Bozhko"
+  "Xiaojie Guo"
+  "Sophie Quinton"
+  "Marco Perronet"
+]
+synopsis: "A Foundation for Formally Proven Schedulability Analysis"
+description: """Prosa is a repository of definitions and proofs for
+real-time schedulability analysis built with Coq. Prosa’s
+distinguishing characteristic is that Prosa prioritizes readability
+over all other concerns to ensure that specifications remain
+accessible to readers without a background in formal proofs. (A
+background in real-time scheduling is assumed.)"""
+url {
+  src: "git+https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git"
+}