Generate .opam and CI from coq-community/templates

.github/workflows/docker-action.yml

@@ -0,0 +1,31 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-ssprove.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

CI.md

@@ -0,0 +1,18 @@
+In this project, continuous integration is based on Github Actions.
+For now we rely on https://github.com/coq-community/templates to generate
+the action from the `meta.yml` file. Actually the `coq-ssprove.opam` file is
+also generated from it.
+
+## With bash
+
+```bash
+TMP=$(mktemp -d); git clone https://github.com/coq-community/templates.git $TMP
+$TMP/generate.sh .github/workflows/docker-action.yml coq-ssprove.opam
+```
+
+## With fish
+
+```fish
+set TMP (mktemp -d) ; git clone https://github.com/coq-community/templates.git $TMP
+$TMP/generate.sh .github/workflows/docker-action.yml coq-ssprove.opam
+```

coq-ssprove.opam

@@ -0,0 +1,42 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "[email protected]"
+version: "dev"
+
+homepage: "https://github.com/ssprove/ssprove"
+dev-repo: "git+https://github.com/ssprove/ssprove.git"
+bug-reports: "https://github.com/ssprove/ssprove/issues"
+license: "MIT"
+
+synopsis: "A framework for modular crypto proofs"
+description: """
+This repository contains a library for doing both state separating proofs
+(SSP) and for showing low-level equivalences of probabilistic stateful
+programs."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.14"}
+  "coq-mathcomp-ssreflect" {(>= "1.13.0" & < "1.14~")}
+  "coq-mathcomp-analysis" {= "0.3.13"}
+  "coq-equations" {>= "1.3"}
+  "coq-extructures" {(>= "0.3.1" & < "dev")}
+]
+
+tags: [
+  "logpath:"
+]
+authors: [
+  "Carmine Abate"
+  "Philipp G. Haselwarter"
+  "Exequiel Rivas"
+  "Antoine Van Muylder"
+  "Théo Winterhalter"
+  "Nikolaj Sidorenco"
+  "Cătălin Hrițcu"
+  "Kenji Maillard"
+  "Bas Spitters"
+]

meta.yml

@@ -0,0 +1,65 @@
+fullname: SSProve framework
+shortname: ssprove
+organization: ssprove
+opam_name: coq-ssprove
+community: false
+action: true
+coqdoc: false
+branch: main
+
+synopsis: >-
+  A framework for modular crypto proofs
+description: |-
+  This repository contains a library for doing both state separating proofs
+  (SSP) and for showing low-level equivalences of probabilistic stateful
+  programs.
+authors:
+- name: Carmine Abate
+  initial: true
+- name: Philipp G. Haselwarter
+  initial: true
+- name: Exequiel Rivas
+  initial: true
+- name: Antoine Van Muylder
+  initial: true
+- name: Théo Winterhalter
+  initial: true
+- name: Nikolaj Sidorenco
+  initial: false
+- name: Cătălin Hrițcu
+  initial: true
+- name: Kenji Maillard
+  initial: true
+- name: Bas Spitters
+  initial: true
+
+opam-file-maintainer: [email protected]
+
+opam-file-version: dev
+
+license:
+  fullname: MIT
+  identifier: MIT
+  file: LICENSE
+
+supported_coq_versions:
+  text: Coq 8.14
+  opam: '{>= "8.14"}'
+
+tested_coq_opam_versions:
+- version: '1.13.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+
+dependencies:
+- opam:
+    name: coq-mathcomp-ssreflect
+    version: '{(>= "1.13.0" & < "1.14~")}'
+- opam:
+    name: coq-mathcomp-analysis
+    version: '{= "0.3.13"}'
+- opam:
+    name: coq-equations
+    version: '{>= "1.3"}'
+- opam:
+    name: coq-extructures
+    version: '{(>= "0.3.1" & < "dev")}'