Dunify

liyishuai · Oct 9, 2024 · cacae07 · cacae07
1 parent b827ba8
commit cacae07
Show file tree

Hide file tree

Showing 22 changed files with 56 additions and 45 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -27,7 +27,7 @@ jobs:
           - 'coqorg/coq:dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-json.opam'

diff --git a/.gitignore b/.gitignore
@@ -34,3 +34,4 @@ nra.cache
 Parser.v
 Makefile.coq*
 *~
+_build/
diff --git a/Makefile b/Makefile
@@ -1,24 +1,17 @@
-COQMAKEFILE ?= Makefile.coq
-MENHIR      ?= menhir
-MENHIRFLAGS ?= --coq
+TEMPLATES ?= ../templates
+TARGETS = .github/workflows/docker-action.yml coq-json.opam dune-project README.md
 
-ifneq ($(MAKECMDGOALS),clean)
-	-include $(COQMAKEFILE)
-endif
+all:
+	dune build
 
-$(COQMAKEFILE): _CoqProject
-	$(COQBIN)coq_makefile -f $^ -o $@
+test: all
+	dune test
 
-.PHONY: clean test
-clean::
-	@ rm -f `cat .gitignore`
-
-Parser.v: Parser.vy
-	$(MENHIR) $(MENHIRFLAGS) $<
-
-test:
-	$(MAKE) -C test
+meta:
+	$(TEMPLATES)/generate.sh $(TARGETS)
 
 publish%:
 	opam publish --packages-directory=released/packages \
 		--repo=coq/opam --tag=v$* -v $* liyishuai/coq-json
+
+.PHONY: all test meta publish
diff --git a/README.md b/README.md
@@ -25,6 +25,7 @@ From JSON to Coq, and vice versa.
   - [ExtLib](https://coq-community.org/coq-ext-lib)
   - [Menhir](http://gallium.inria.fr/~fpottier/menhir/)
   - [MenhirLib](https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib/)
+  - [Dune](https://dune.build) 3.6 or later
 - Coq namespace: `JSON`
 - Related publication(s): none
 
@@ -43,8 +44,8 @@ To instead build and install manually, do:
 ``` shell
 git clone https://github.com/liyishuai/coq-json.git
 cd coq-json
-make   # or make -j <number-of-cores-on-your-machine> 
-make install
+dune build
+dune install
 ```
 
 

diff --git a/_CoqProject b/_CoqProject
diff --git a/coq-json.opam b/coq-json.opam
@@ -14,12 +14,11 @@ synopsis: "JSON in Coq"
 description: """
 From JSON to Coq, and vice versa."""
 
-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-parsec" { >= "0.1.1" }
+  "coq-parsec" { >= "0.2.0" }
   "coq-ext-lib" 
   "menhir" { >= "20220210" }
   "coq-menhirlib" { >= "20220210" }

diff --git a/dune-project b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.6)
+(using coq 0.6)
+(name coq-json)
diff --git a/meta.yml b/meta.yml
@@ -17,7 +17,7 @@ dependencies:
   - description: '[Parsec](https://github.com/liyishuai/coq-parsec)'
     opam:
       name: coq-parsec
-      version: '{ >= "0.1.1" }'
+      version: '{ >= "0.2.0" }'
   - description: '[ExtLib](https://coq-community.org/coq-ext-lib)'
     opam:
       name: coq-ext-lib
@@ -49,7 +49,7 @@ tested_coq_opam_versions:
   - version: '8.19'
   - version: '8.20'
   - version: 'dev'
-test_target: test
+dune: true
 action_appendix: |2-
             export: 'OPAMWITHTEST'
           env:

diff --git a/test/Makefile b/test/Makefile
diff --git a/test/TestPrint.v b/test/TestPrint.v
@@ -11,4 +11,5 @@ Example j1 : json :=
          ("fields", JSON__Object [("ETag", JSON__String "tag-foo"); ("Content-Length", JSON__String "11")]);
          ("body", JSON__String "content-bar")].
 
-Compute to_string j1.
+Goal to_string j1 = "{""version"":{""major"":1,""minor"":1},""code"":200,""reason"":""OK"",""fields"":{""ETag"":""tag-foo"",""Content-Length"":""11""},""body"":""content-bar""}".
+Proof. reflexivity. Qed.
diff --git a/test/_CoqProject b/test/_CoqProject
diff --git a/test/dune b/test/dune
@@ -0,0 +1,20 @@
+(alias
+ (name runtest)
+ (deps
+  (package coq-json)
+  (alias_rec all)))
+
+(rule
+ (alias runtest)
+ (action
+  (run coqc %{dep:TestDecode.v})))
+
+(rule
+ (alias runtest)
+ (action
+  (run coqc %{dep:TestParse.v})))
+
+(rule
+ (alias runtest)
+ (action
+  (run coqc %{dep:TestPrint.v})))
diff --git a/Decode.v → theories/Decode.v b/Decode.v → theories/Decode.v
diff --git a/Encode.v → theories/Encode.v b/Encode.v → theories/Encode.v
diff --git a/Instances.v → theories/Instances.v b/Instances.v → theories/Instances.v
diff --git a/JSON.v → theories/JSON.v b/JSON.v → theories/JSON.v
diff --git a/Jpath.v → theories/Jpath.v b/Jpath.v → theories/Jpath.v
diff --git a/Lexer.v → theories/Lexer.v b/Lexer.v → theories/Lexer.v
diff --git a/Operator.v → theories/Operator.v b/Operator.v → theories/Operator.v
diff --git a/Parser.vy → theories/Parser.vy b/Parser.vy → theories/Parser.vy
diff --git a/Printer.v → theories/Printer.v b/Printer.v → theories/Printer.v
diff --git a/theories/dune b/theories/dune
@@ -0,0 +1,11 @@
+(coq.theory
+ (name JSON)
+ (package coq-json)
+ (synopsis "JSON in Coq")
+ (flags -w -deprecated-syntactic-definition))
+
+(rule
+ (target Parser.v)
+ (deps Parser.vy)
+ (action
+  (run menhir --coq %{deps})))
-Original file line number
+Diff line change
@@ Expand Up / @@ -34,3 +34,4 @@ nra.cache @@
     Parser.v
     Makefile.coq*
     *~
+    _build/