From 979772bb723a5c8191ea9056b1e45af78bd8aff1 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 17 Jan 2020 13:10:33 +0100
Subject: [PATCH] Add an Opam file
---
.gitlab-ci.yml | 61 +++++++++++++++++++++++++++++++++++++-------------
README.md | 19 ++++++++++++++--
coq-prosa.opam | 44 ++++++++++++++++++++++++++++++++++++
3 files changed, 106 insertions(+), 18 deletions(-)
create mode 100644 coq-prosa.opam
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4ff3e3be7..2fb9aec45 100644
--- a/.gitlab-ci.yml
+++ b/.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}
diff --git a/README.md b/README.md
index dc7427a9a..13f11fee4 100644
--- a/README.md
+++ b/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.
diff --git a/coq-prosa.opam b/coq-prosa.opam
new file mode 100644
index 000000000..ce6343510
--- /dev/null
+++ b/coq-prosa.opam
@@ -0,0 +1,44 @@
+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"
+}
--
GitLab