From 42179633f7b2a4852a8284dd50f0a4ec896e4c97 Mon Sep 17 00:00:00 2001 From: Yishuai Li Date: Tue, 8 Oct 2024 15:13:12 +0800 Subject: [PATCH] Dunify --- .gitignore | 1 + Makefile | 27 ++++++++++----------------- README.md | 5 +++-- _CoqProject | 13 ------------- coq-json.opam | 5 ++--- dune-project | 3 +++ meta.yml | 2 +- test/TestPrint.v | 3 ++- test/_CoqProject | 4 ---- test/dune | 25 +++++++++++++++++++++++++ Decode.v => theories/Decode.v | 0 Encode.v => theories/Encode.v | 0 Instances.v => theories/Instances.v | 0 JSON.v => theories/JSON.v | 0 Jpath.v => theories/Jpath.v | 0 Lexer.v => theories/Lexer.v | 0 Operator.v => theories/Operator.v | 0 Parser.vy => theories/Parser.vy | 0 Printer.v => theories/Printer.v | 0 theories/dune | 11 +++++++++++ 20 files changed, 58 insertions(+), 41 deletions(-) delete mode 100644 _CoqProject create mode 100644 dune-project delete mode 100644 test/_CoqProject create mode 100644 test/dune rename Decode.v => theories/Decode.v (100%) rename Encode.v => theories/Encode.v (100%) rename Instances.v => theories/Instances.v (100%) rename JSON.v => theories/JSON.v (100%) rename Jpath.v => theories/Jpath.v (100%) rename Lexer.v => theories/Lexer.v (100%) rename Operator.v => theories/Operator.v (100%) rename Parser.vy => theories/Parser.vy (100%) rename Printer.v => theories/Printer.v (100%) create mode 100644 theories/dune 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..9455c22 100644 --- 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) 2.5 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 -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..18e1836 100644 --- a/coq-json.opam +++ b/coq-json.opam @@ -14,10 +14,9 @@ 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" 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..82d9e79 100644 --- a/meta.yml +++ b/meta.yml @@ -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/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..093e0f2 --- /dev/null +++ b/test/dune @@ -0,0 +1,25 @@ +(alias + (name runtest) + (deps + (alias_rec all))) + +(rule + (alias runtest) + (deps + (package coq-json)) + (action + (run coqc %{dep:TestDecode.v}))) + +(rule + (alias runtest) + (deps + (package coq-json)) + (action + (run coqc %{dep:TestParse.v}))) + +(rule + (alias runtest) + (deps + (package coq-json)) + (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})))