Merge pull request #5 from coq-community/8.16-ci

compatibility with 8.16, add CI

.github/workflows/docker-action.yml

@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'
           - 'coqorg/coq:8.14'
           - 'coqorg/coq:8.13'

README.md

@@ -44,6 +44,7 @@ verified runtime assertion checker for JML.
 - Additional dependencies: none
 - Coq namespace: `JML`
 - Related publication(s):
+  - [A formal definition of JML in Coq and its application to runtime assertion checking](https://www.research-collection.ethz.ch/handle/20.500.11850/44276) doi:[10.3929/ethz-a-006680049](https://doi.org/10.3929/ethz-a-006680049)
   - [A Formalization of JML in the Coq Proof System](https://www.research-collection.ethz.ch/handle/20.500.11850/68882) doi:[10.3929/ethz-a-006903145](https://doi.org/10.3929/ethz-a-006903145)
 
 ## Building and installation instructions

coq-jmlcoq.opam

@@ -19,7 +19,7 @@ verified runtime assertion checker for JML."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.10" & < "8.16~") | (= "dev")}
+  "coq" {(>= "8.10" & < "8.17~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -6,7 +6,7 @@ community: true
 action: true
 nix: true
 coqdoc: false
-dune: true
+dune: false
 
 synopsis: >-
   Coq definition of the JML specification language
@@ -18,6 +18,9 @@ description: |-
   verified runtime assertion checker for JML.
 
 publications:
+- pub_url: https://www.research-collection.ethz.ch/handle/20.500.11850/44276
+  pub_title: A formal definition of JML in Coq and its application to runtime assertion checking
+  pub_doi: 10.3929/ethz-a-006680049
 - pub_url: https://www.research-collection.ethz.ch/handle/20.500.11850/68882
   pub_title: A Formalization of JML in the Coq Proof System
   pub_doi: 10.3929/ethz-a-006903145
@@ -44,13 +47,14 @@ license:
 
 supported_coq_versions:
   text: 8.10 or later
-  opam: '{(>= "8.10" & < "8.16~") | (= "dev")}'
+  opam: '{(>= "8.10" & < "8.17~") | (= "dev")}'
 
 tested_coq_nix_versions:
 - coq_version: 'master'
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.16'
 - version: '8.15'
 - version: '8.14'
 - version: '8.13'