wip

Deducteam · Apr 12, 2024 · b70a777 · b70a777
1 parent 22f5d47
commit b70a777
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 5 deletions.
diff --git a/Makefile b/Makefile
@@ -216,13 +216,8 @@ nothing:
 
 .PHONY: vo
 vo: $(LP_FILES:%.lp=%.vo)
-ifeq ($(PROGRESS),1)
-	rm -f .finished
-	$(HOL2DK_DIR)/progress &
-endif
 ifneq ($(INCLUDE_VO_MK),1)
 	$(MAKE) INCLUDE_VO_MK=1 vo
-	touch .finished
 endif
 
 COQC_OPTIONS = -no-glob # -w -coercions

diff --git a/TODO.md b/TODO.md
@@ -1,6 +1,8 @@
 TODO
 ----
 
+- generate spec files in ocaml to optimize dependencies (spec files should not depend on abbreviations)
+
 - use a single term_abbrev file for each theorem, and split it
 
 - pre-compute once and for all the type and term variables of axioms and definitions