From 22c9055920e700085e3921a89b87b19e9cae0a95 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Mon, 3 Jun 2024 02:02:44 -0400
Subject: [PATCH] Add build time check to CI (#96)

* Add build time check to CI

* Increase cache prefix

* Fix CI

* Fix CI, really

* Optimize a tactic
---
 .github/workflows/ci_build.yml      |  4 ++--
 .gitignore                          |  6 ++++++
 theories/CoqMakefile.mk.local-late  | 29 +++++++++++++++++++++++++++++
 theories/Core/Semantic/PER/Lemmas.v |  7 ++++++-
 theories/Makefile                   | 17 ++---------------
 5 files changed, 45 insertions(+), 18 deletions(-)
 create mode 100644 theories/CoqMakefile.mk.local-late

diff --git a/.github/workflows/ci_build.yml b/.github/workflows/ci_build.yml
index e9a34a84..d807375e 100644
--- a/.github/workflows/ci_build.yml
+++ b/.github/workflows/ci_build.yml
@@ -36,7 +36,7 @@ jobs:
         with:
           ocaml-compiler: ${{ env.OCAML_VER }}
           dune-cache: true
-          cache-prefix: "v2"
+          cache-prefix: "v2.1"
       - name: install Menhir and Coq
         run: |
           opam update
@@ -55,7 +55,7 @@ jobs:
         run: |
           eval $(opam env)
           cd theories/
-          make -j ${{ steps.cpu-cores.outputs.count }}
+          make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed
       - name: test parser
         run: |
           eval $(opam env)
diff --git a/.gitignore b/.gitignore
index b4845316..0c348ed6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,4 +15,10 @@ theories/**/Parser.v
 *.vos
 .lia.cache
 CoqMakefile.mk*
+!CoqMakefile.mk.local
+!CoqMakefile.mk.local-late
+*.log
+
+# Editor related
+## Emacs
 *.~undo-tree~
diff --git a/theories/CoqMakefile.mk.local-late b/theories/CoqMakefile.mk.local-late
new file mode 100644
index 00000000..14eb2701
--- /dev/null
+++ b/theories/CoqMakefile.mk.local-late
@@ -0,0 +1,29 @@
+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))
+
+post-all:: $(COQPARSERFILE)
+	@+$(MAKE) "$(PARSERFILE)"
+
+$(COQPARSERFILE): %.v : %.vy
+	$(MENHIR) --coq "$?"
+
+$(PARSERBASE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" -B "$(patsubst %.v,%.vo,$?)"
+
+$(PARSERFILE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) "$(PARSERBASE)"
+	@echo "MOVE $(PARSERBASE) => $@"
+	@mv "$(PARSERBASE)" "$@"
+	@mv "$(patsubst %.ml,%.mli,$(PARSERBASE))" "$(patsubst %.ml,%.mli,$@)"
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 4bdc7736..9f7bbefb 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -272,7 +272,12 @@ Ltac clear_relation_equivalence :=
         (unify R1 R2; clear H) + (is_var R1; clear R1 H) + (is_var R2; clear R2 H)
     end.
 
-Ltac apply_relation_equivalence := rewrite_relation_equivalence_right; clear_relation_equivalence; rewrite_relation_equivalence_left; clear_relation_equivalence.
+Ltac apply_relation_equivalence :=
+  clear_relation_equivalence;
+  rewrite_relation_equivalence_right;
+  clear_relation_equivalence;
+  rewrite_relation_equivalence_left;
+  clear_relation_equivalence.
 
 Lemma per_univ_elem_right_irrel : forall i i' R a b R' b',
     {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
diff --git a/theories/Makefile b/theories/Makefile
index c1b52d89..68c3d572 100644
--- a/theories/Makefile
+++ b/theories/Makefile
@@ -14,9 +14,8 @@ COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy'))
 COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
 
 .PHONY: all
-all: $(COQMAKEFILE) $(COQPARSERFILE)
+all: $(COQMAKEFILE)
 	@+$(MAKE) -f "$(COQMAKEFILE)" all
-	@+$(MAKE) "$(PARSERFILE)"
 
 .PHONY: clean
 clean: $(COQMAKEFILE)
@@ -28,7 +27,7 @@ clean: $(COQMAKEFILE)
 update_CoqProject: clean
 	(echo "-R . Mcltt"; \
         echo ""; \
-        echo "-arg -w -arg -notation-overridden"; \
+        echo "-arg -w -arg -cast-in-pattern,-notation-overridden"; \
         echo ""; \
         echo -e "$(subst $(space),\n,$(COQFILES))") > "$(COQPROJECTFILE)"
 
@@ -38,19 +37,7 @@ force: ;
 $(COQMAKEFILE): $(COQPROJECTFILE)
 	$(COQBIN)coq_makefile -f "$?" -o "$@"
 
-$(COQPARSERFILE): %.v : %.vy
-	$(MENHIR) --coq "$?"
-
 $(COQPROJECTFILE): ;
 
-$(PARSERBASE): $(PARSEREXTRACTIONCOQFILE)
-	@+$(MAKE) -f "$(COQMAKEFILE)" -B "$(patsubst %.v,%.vo,$?)"
-
-$(PARSERFILE): $(PARSEREXTRACTIONCOQFILE)
-	@+$(MAKE) "$(PARSERBASE)"
-	@echo "MOVE $(PARSERBASE) => $@"
-	@mv "$(PARSERBASE)" "$@"
-	@mv "$(patsubst %.ml,%.mli,$(PARSERBASE))" "$(patsubst %.ml,%.mli,$@)"
-
 %: $(COQMAKEFILE) force
 	@+$(MAKE) -f "$(COQMAKEFILE)" "$@"