From 77bc9bb7c292fbc2ba6459b09e14cbed6b5594e9 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Mon, 25 Dec 2023 18:57:29 -0400
Subject: [PATCH] Update makefile to make extraction cleaner (#41)

* Update makefile to make extraction cleaner

* Update makefile
---
 .github/workflows/ci_build.yml       |  1 +
 .gitignore                           |  6 +--
 driver/main.ml                       |  3 +-
 theories/Frontend/ParserExtraction.v |  3 +-
 theories/Makefile                    | 55 ++++++++++++++++++++++++++++
 theories/makefile                    | 29 ---------------
 6 files changed, 62 insertions(+), 35 deletions(-)
 create mode 100644 theories/Makefile
 delete mode 100644 theories/makefile

diff --git a/.github/workflows/ci_build.yml b/.github/workflows/ci_build.yml
index 6ce979eb..cec17568 100644
--- a/.github/workflows/ci_build.yml
+++ b/.github/workflows/ci_build.yml
@@ -33,6 +33,7 @@ jobs:
         with:
           ocaml-compiler: ${{ env.OCAML_VER }}
           dune-cache: true
+          cache-prefix: "v2"
       - name: install Menhir and Coq
         run: |
           opam update
diff --git a/.gitignore b/.gitignore
index 7073d776..b4845316 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,8 @@
 _build
 
 # Ignore generated parser code
-driver/parser.ml
-driver/parser.mli
+**/parser.ml
+**/parser.mli
 theories/**/Parser.v
 
 # Remove Coq compiled code
@@ -14,5 +14,5 @@ theories/**/Parser.v
 *.vok
 *.vos
 .lia.cache
-makefile.coq*
+CoqMakefile.mk*
 *.~undo-tree~
diff --git a/driver/main.ml b/driver/main.ml
index 20d853fb..be71882e 100644
--- a/driver/main.ml
+++ b/driver/main.ml
@@ -5,7 +5,8 @@ let parse text =
      which we then feed into the parser. *)
   let rec loop lexbuf = lazy (Buf_cons (Lexer.read lexbuf, loop lexbuf)) in
   let token_stream = loop (Lexing.from_string text) in
-  match Parser.prog 50 token_stream with
+  let parse : int -> buffer -> Parser.Cst.obj parse_result = Parser.prog in
+  match parse 50 token_stream with
   | Parsed_pr (e, _) -> Some e
   | Fail_pr_full (_, _) -> None
   | _ -> None
diff --git a/theories/Frontend/ParserExtraction.v b/theories/Frontend/ParserExtraction.v
index 6300aa05..65a33a3b 100644
--- a/theories/Frontend/ParserExtraction.v
+++ b/theories/Frontend/ParserExtraction.v
@@ -8,5 +8,4 @@ Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
 Require Import ExtrOcamlNativeString.
 
-(* Meant to be run in this directory *)
-Extraction "../driver/parser.ml" Parser.prog.
+Extraction "parser.ml" Parser.prog.
diff --git a/theories/Makefile b/theories/Makefile
new file mode 100644
index 00000000..5bf179fe
--- /dev/null
+++ b/theories/Makefile
@@ -0,0 +1,55 @@
+empty :=
+space := $(empty) $(empty)
+
+MENHIR := menhir
+
+COQMAKEFILE := CoqMakefile.mk
+COQPROJECTFILE := _CoqProject
+PARSERBASE := parser.ml
+PARSERFILE := ../driver/$(PARSERBASE)
+PARSEREXTRACTIONDIR := Frontend
+PARSEREXTRACTIONCOQFILE := $(PARSEREXTRACTIONDIR)/ParserExtraction.v
+PARSEREXTRACTIONRESULTFILE := $(PARSEREXTRACTIONDIR)/$(PARSERBASE)
+COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy'))
+COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
+
+.PHONY: all
+all: $(COQMAKEFILE) $(COQPARSERFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" all
+	@+$(MAKE) "$(PARSERFILE)"
+
+.PHONY: clean
+clean: $(COQMAKEFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" cleanall
+	@echo "CLEAN $(COQPARSERFILE) $(PARSERFILE) $(COQMAKEFILE) $(COQMAKEFILE).conf"
+	@rm -f "$(COQPARSERFILE)" "$(PARSERBASE)" "$(PARSERFILE)" "$(COQMAKEFILE)" "$(COQMAKEFILE).conf"
+
+.PHONY: update_CoqProject
+update_CoqProject: clean
+	(echo "-R . Mcltt"; \
+        echo ""; \
+        echo "-arg -w -arg -notation-overridden"; \
+        echo ""; \
+        echo -e "$(subst $(space),\n,$(COQFILES))") > "$(COQPROJECTFILE)"
+
+.PHONY: force
+force: ;
+
+$(COQMAKEFILE): $(COQPROJECTFILE)
+	$(COQBIN)coq_makefile -f "$(COQPROJECTFILE)" -o "$(COQMAKEFILE)"
+
+$(COQPARSERFILE): %.v : %.vy
+	$(MENHIR) --coq "$?"
+
+$(COQPROJECTFILE): ;
+
+$(PARSERBASE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" -B "$(patsubst %.v,%.vo,$?)"
+
+$(PARSERFILE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) "$(PARSERBASE)"
+	@echo "MOVE $(PARSERBASE) => $(PARSERFILE)"
+	@mv "$(PARSERBASE)" "$(PARSERFILE)"
+
+%: $(COQMAKEFILE) force
+	@+$(MAKE) -f "$(COQMAKEFILE)" "$@"
diff --git a/theories/makefile b/theories/makefile
deleted file mode 100644
index 746e4a73..00000000
--- a/theories/makefile
+++ /dev/null
@@ -1,29 +0,0 @@
-empty :=
-space := $(empty) $(empty)
-
-COQMAKEFILE := makefile.coq
-COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy'))
-COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
-
-.PHONY: all
-all: $(COQMAKEFILE)
-
--include $(COQMAKEFILE)
-
-clean::
-	rm -f $(COQMAKEFILE)
-	rm -f $(COQMAKEFILE).conf
-
-$(COQPARSERFILE): %.v : %.vy
-	menhir --coq "$?"
-
-$(COQMAKEFILE): _CoqProject
-	coq_makefile -f _CoqProject -o "$@"
-
-.PHONY: update_CoqProject
-update_CoqProject: cleanall
-	(echo "-R . Mcltt"; \
-        echo ""; \
-        echo "-arg -w -arg -notation-overridden"; \
-        echo ""; \
-        echo -e "$(subst $(space),\n,$(COQFILES))") > _CoqProject