From 18640c782f216e6e62e25ce24b6061ad93703cf6 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 24 Mar 2022 11:03:10 +0000
Subject: Update makefile and remove _CoqProject

---
 Makefile    | 19 +++++++++++--------
 _CoqProject | 15 ---------------
 2 files changed, 11 insertions(+), 23 deletions(-)
 delete mode 100644 _CoqProject

diff --git a/Makefile b/Makefile
index 3b51d00..978a109 100644
--- a/Makefile
+++ b/Makefile
@@ -22,11 +22,11 @@ COQMAKE := $(COQBIN)coq_makefile
 COQDOCFLAGS := --no-lib-name -l
 
 VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, $(wildcard src/$(d)/*.v))
-LIT := $(wildcard lit/*.org)
+LIT := docs/basic-block-generation.org docs/scheduler.org docs/scheduler-languages.org
 
 PREFIX ?= .
 
-.PHONY: all install proof clean extraction test
+.PHONY: all install proof clean extraction test force
 
 all: lib/COMPCERTSTAMP
 	$(MAKE) proof
@@ -74,24 +74,27 @@ src/extraction/STAMP:
 	@$(COQEXEC) ./src/extraction/Extraction.v
 	@touch $@
 
-Makefile.coq:
+Makefile.coq: force
 	@echo "COQMAKE Makefile.coq"
 	$(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq
+	echo "$(COQINCLUDES)" >_CoqProject
+
+force:
 
 docs/vericert.1:
 	$(MAKE) -C docs vericert.1
 
-clean:: Makefile.coq
-	$(MAKE) -f Makefile.coq clean
-	$(MAKE) -C test clean
-	rm -f Makefile.coq
-
 detangle-all:
 	emacs --batch --eval "(progn(require 'org)(require 'ob-tangle)\
         (setq org-src-preserve-indentation t)\
         $(foreach vs,$(VS),(org-babel-detangle \"$(vs)\"))\
         (org-save-all-org-buffers))"
 
+clean:: Makefile.coq
+	$(MAKE) -f Makefile.coq clean
+	$(MAKE) -C test clean
+	rm -f Makefile.coq
+
 clean::
 	rm -f */*.v.d */*.glob */*.vo */*~ *~
 	rm -f src/extraction/*.ml src/extraction/*.mli
diff --git a/_CoqProject b/_CoqProject
deleted file mode 100644
index 69d12c1..0000000
--- a/_CoqProject
+++ /dev/null
@@ -1,15 +0,0 @@
--R src/common vericert.common
--R src/extraction vericert.extraction
--R src/hls vericert.hls
--R src vericert
-
--R lib/CompCert/backend compcert.backend
--R lib/CompCert/cfrontend compcert.cfrontend
--R lib/CompCert/common compcert.common
--R lib/CompCert/cparser compcert.cparser
--R lib/CompCert/driver compcert.driver
--R lib/CompCert/exportclight compcert.exportclight
--R lib/CompCert/lib compcert.lib
--R lib/CompCert/verilog compcert.verilog
--R lib/CompCert/flocq Flocq
--R lib/CompCert/MenhirLib MenhirLib
-- 
cgit