Dunify

.github/workflows/docker-action.yml

@@ -23,6 +23,8 @@ jobs:
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.18'
+          - 'coqorg/coq:8.19'
+          - 'coqorg/coq:8.20'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

.gitignore

@@ -34,3 +34,4 @@ nra.cache
 Makefile.coq*
 *~
 *.conf
+_build/

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/liyishuai/coq-parsec/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/liyishuai/coq-parsec/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/liyishuai/coq-parsec/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/liyishuai/coq-parsec/actions/workflows/docker-action.yml
 
 
 
@@ -17,16 +17,17 @@ Inspired by Haskell Parsec library.
 ## Meta
 
 - Author(s):
-  - Yishuai Li [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0002-5728-5903)
+  - Yishuai Li [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0002-5728-5903)
   - Azzam Althagafi
-  - Yao Li [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-8720-883X)
-  - Li-yao Xia [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0003-2673-4400)
-  - Benjamin C. Pierce [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-7839-1636)
+  - Yao Li [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-8720-883X)
+  - Li-yao Xia [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0003-2673-4400)
+  - Benjamin C. Pierce [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-7839-1636)
 - License: [BSD 3-Clause "New" or "Revised" License](LICENSE)
 - Compatible Coq versions: 8.14 or later
 - Additional dependencies:
   - [Cérès](https://github.com/Lysxia/coq-ceres)
   - [ExtLib](https://coq-community.org/coq-ext-lib/)
+  - [Dune](https://dune.build) 2.5 or later
 - Coq namespace: `Parsec`
 - Related publication(s): none
 
@@ -45,8 +46,8 @@ To instead build and install manually, do:
 ``` shell
 git clone https://github.com/liyishuai/coq-parsec.git
 cd coq-parsec
-make   # or make -j <number-of-cores-on-your-machine> 
-make install
+dune build
+dune install
 ```
 
 

coq-parsec.opam

@@ -14,10 +14,9 @@ synopsis: "Monadic parser combinator library in Coq"
 description: """
 Inspired by Haskell Parsec library."""
 
-build: [make "-j%{jobs}%"]
-run-test: [make "-j%{jobs}%" "test"]
-install: [make "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
+  "dune" {>= "3.6"}
   "coq" { >= "8.14~" }
   "coq-ceres" { >= "0.4.0" }
   "coq-ext-lib" { >= "0.11.3" }

dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.6)
+(using coq 0.6)
+(name coq-parsec)

meta.yml

@@ -34,7 +34,7 @@ dependencies:
     opam:
       name: coq-ext-lib
       version: '{ >= "0.11.3" }'
-test_target: test
+dune: true
 categories:
   - name: Computer Science/Data Types and Data Structures
 keywords:
@@ -51,3 +51,5 @@ tested_coq_opam_versions:
   - version: '8.16'
   - version: '8.17'
   - version: '8.18'
+  - version: '8.19'
+  - version: '8.20'