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

@@ -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)

.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~

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,$@)"

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 }} ->

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)" "$@"