diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index b0ef8b1..4e7a670 100644
--- 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
index d934ecd..568ef69 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,3 +34,4 @@ nra.cache
 Parser.v
 Makefile.coq*
 *~
+_build/
diff --git a/Makefile b/Makefile
index d39ba4b..396a1cb 100644
--- 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
index 2ad46ac..4c565f0 100644
--- a/README.md
+++ b/README.md
@@ -22,9 +22,9 @@ From JSON to Coq, and vice versa.
 - Compatible Coq versions: 8.14 or later
 - Additional dependencies:
   - [Parsec](https://github.com/liyishuai/coq-parsec)
-  - [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 +43,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
deleted file mode 100644
index 362dabf..0000000
--- a/_CoqProject
+++ /dev/null
@@ -1,13 +0,0 @@
--Q . JSON
--arg -w -arg -notation-overridden
--arg -w -arg -deprecated-syntactic-definition
--native-compiler no
-JSON.v
-Parser.v
-Lexer.v
-Printer.v
-Instances.v
-Operator.v
-Jpath.v
-Decode.v
-Encode.v
diff --git a/coq-json.opam b/coq-json.opam
index b6e9175..d14f30f 100644
--- a/coq-json.opam
+++ b/coq-json.opam
@@ -14,13 +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-ext-lib" 
+  "coq-parsec" { >= "0.2.0" }
   "menhir" { >= "20220210" }
   "coq-menhirlib" { >= "20220210" }
 ]
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..5c5c356
--- /dev/null
+++ 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
index c36bd53..0cc33f0 100644
--- a/meta.yml
+++ b/meta.yml
@@ -17,10 +17,7 @@ dependencies:
   - description: '[Parsec](https://github.com/liyishuai/coq-parsec)'
     opam:
       name: coq-parsec
-      version: '{ >= "0.1.1" }'
-  - description: '[ExtLib](https://coq-community.org/coq-ext-lib)'
-    opam:
-      name: coq-ext-lib
+      version: '{ >= "0.2.0" }'
   - description: '[Menhir](http://gallium.inria.fr/~fpottier/menhir/)'
     opam:
       name: menhir
@@ -49,7 +46,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
deleted file mode 100644
index bb69e69..0000000
--- a/test/Makefile
+++ /dev/null
@@ -1 +0,0 @@
-include ../Makefile
diff --git a/test/TestPrint.v b/test/TestPrint.v
index 79bba15..5f39340 100644
--- 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
deleted file mode 100644
index 19800ec..0000000
--- a/test/_CoqProject
+++ /dev/null
@@ -1,4 +0,0 @@
--Q .. JSON
-TestDecode.v
-TestPrint.v
-TestParse.v
\ No newline at end of file
diff --git a/test/dune b/test/dune
new file mode 100644
index 0000000..529ae8a
--- /dev/null
+++ 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 b/theories/Decode.v
similarity index 100%
rename from Decode.v
rename to theories/Decode.v
diff --git a/Encode.v b/theories/Encode.v
similarity index 100%
rename from Encode.v
rename to theories/Encode.v
diff --git a/Instances.v b/theories/Instances.v
similarity index 100%
rename from Instances.v
rename to theories/Instances.v
diff --git a/JSON.v b/theories/JSON.v
similarity index 100%
rename from JSON.v
rename to theories/JSON.v
diff --git a/Jpath.v b/theories/Jpath.v
similarity index 100%
rename from Jpath.v
rename to theories/Jpath.v
diff --git a/Lexer.v b/theories/Lexer.v
similarity index 100%
rename from Lexer.v
rename to theories/Lexer.v
diff --git a/Operator.v b/theories/Operator.v
similarity index 100%
rename from Operator.v
rename to theories/Operator.v
diff --git a/Parser.vy b/theories/Parser.vy
similarity index 100%
rename from Parser.vy
rename to theories/Parser.vy
diff --git a/Printer.v b/theories/Printer.v
similarity index 100%
rename from Printer.v
rename to theories/Printer.v
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..09afadd
--- /dev/null
+++ 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})))