From cf2c89f9345dbb9f86798cda11f33daaa45046cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 23 Oct 2024 18:15:28 -0700
Subject: [PATCH] Fix karamel tests

---
 examples/Makefile                |  3 +-
 examples/demos/Makefile          |  3 +-
 examples/demos/low-star/Makefile | 10 ++++--
 examples/kv_parsing/Makefile     | 53 +++++++++++++-------------------
 examples/miniparse/Makefile      |  3 +-
 mk/test.mk                       |  7 +++--
 6 files changed, 39 insertions(+), 40 deletions(-)

diff --git a/examples/Makefile b/examples/Makefile
index f5dc86c1822..3c8d801afe9 100644
--- a/examples/Makefile
+++ b/examples/Makefile
@@ -33,8 +33,9 @@ SUBDIRS += verifythis
 
 ifdef KRML_HOME
 SUBDIRS += demos
-SUBDIRS += kv_parsing
 SUBDIRS += miniparse
+SUBDIRS_ALL += kv_parsing
+SUBDIRS_CLEAN += kv_parsing
 endif
 
 # These have custom makefiles
diff --git a/examples/demos/Makefile b/examples/demos/Makefile
index e0142ba454c..1fed695880c 100644
--- a/examples/demos/Makefile
+++ b/examples/demos/Makefile
@@ -1,4 +1,5 @@
-SUBDIRS += low-star
+SUBDIRS_ALL += low-star
+SUBDIRS_CLEAN += low-star
 # SUBDIRS += fstar_and_lowstar
 # ^ This has never been enabled, add it? It does need karamel and krmllib.
 
diff --git a/examples/demos/low-star/Makefile b/examples/demos/low-star/Makefile
index 0f589365824..59d7fd85db9 100644
--- a/examples/demos/low-star/Makefile
+++ b/examples/demos/low-star/Makefile
@@ -1,8 +1,14 @@
 FSTAR_ROOT ?= ../../..
 include $(FSTAR_ROOT)/mk/test.mk
 
+ifneq ($(KRML_HOME),)
+KRML = $(KRML_HOME)/krml
+else
+KRML = krml
+endif
+
 extract:
-	krml -skip-compilation Demo.fst -tmpdir out | grep "wrote out"
+	$(KRML) -skip-compilation Demo.fst -tmpdir $(OUTPUT_DIR) | grep "wrote out"
 
 extract-tailcalls:
-	krml -skip-compilation -ftail-calls Demo.fst -tmpdir out | grep "wrote out"
+	$(KRML) -skip-compilation -ftail-calls Demo.fst -tmpdir $(OUTPUT_DIR) | grep "wrote out"
diff --git a/examples/kv_parsing/Makefile b/examples/kv_parsing/Makefile
index da1b79f5b23..7e62e68c2e6 100644
--- a/examples/kv_parsing/Makefile
+++ b/examples/kv_parsing/Makefile
@@ -1,43 +1,32 @@
-include ../Makefile.include
-
 ifndef KRML_HOME
      $(error "Please define the `KRML_HOME` variable.")
 endif
 
-FST_FILES :=	Slice.fst \
-		Parsing.fst \
-		Serializing.fst \
-		IntegerParsing.fst \
-		KeyValue.fst \
-		PureParser.fst \
-		PureValidator.fst \
-		Validator.fst \
-		ValidatedParser.fst \
-		ValidatedAccess.fst \
-		PureEncoder.fst \
-		Serializer.fst \
-		EnumParsing.fst \
-		VectorParsing.fst
-
-EXTRACT_FILES := IntegerParsing.fst \
-		 Validator.fst \
-		 ValidatedParser.fst \
-		 ValidatedAccess.fst \
-		 Serializer.fst \
-		 EnumParsing.fst \
-		 VectorParsing.fst
+OTHERFLAGS += --include $(KRML_HOME)/krmllib
+OTHERFLAGS += --include $(KRML_HOME)/krmllib/obj # cache dir for krmllib
+OTHERFLAGS += --include $(KRML_HOME)/krmllib/compat
+OTHERFLAGS += --z3rlimit_factor 4
 
-FSTAR_INCLUDE_PATHS:=--include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/compat
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 
-OTHERFLAGS+=$(FSTAR_INCLUDE_PATHS) --z3rlimit_factor 4
+# None of this was exercised.
+#
+# EXTRACT_FILES := IntegerParsing.fst \
+#                  Validator.fst \
+#                  ValidatedParser.fst \
+#                  ValidatedAccess.fst \
+#                  Serializer.fst \
+#                  EnumParsing.fst \
+#                  VectorParsing.fst
 
-all: $(FST_FILES:.fst=.uver)
 
-%.fst-in:
-	@echo $(OTHERFLAGS)
+# # all: $(FST_FILES:.fst=.uver)
 
+# # %.fst-in:
+# #         @echo $(OTHERFLAGS)
 
-extract-c: $(EXTRACT_FILES)
-	krml -skip-compilation -warn-error +11 $(EXTRACT_FILES)
+# # extract-c: $(EXTRACT_FILES)
+# #         krml -skip-compilation -warn-error +11 $(EXTRACT_FILES)
 
-clean:
+# # clean:
diff --git a/examples/miniparse/Makefile b/examples/miniparse/Makefile
index c8c194def39..a4ec15bfaeb 100644
--- a/examples/miniparse/Makefile
+++ b/examples/miniparse/Makefile
@@ -2,7 +2,6 @@
 # # Inspired from: ../tactics/Makefile
 
 # ifdef KRML_HOME
-# INCLUDE_PATHS+=$(KRML_HOME)/krmllib
 # endif
 # FSTAR_FILES=$(wildcard *.fst) $(wildcard *.fsti)
 
@@ -29,6 +28,8 @@
 # %.fst-in:
 #         @echo $(OTHERFLAGS) $(addprefix --include , $(INCLUDE_PATHS))
 
+OTHERFLAGS += --include $(KRML_HOME)/krmllib
+OTHERFLAGS += --include $(KRML_HOME)/krmllib/obj # cache dir for krmllib
 
 FSTAR_ROOT ?= ../..
 include $(FSTAR_ROOT)/mk/test.mk
diff --git a/mk/test.mk b/mk/test.mk
index 8ede2644e5c..a3ceaab9dee 100644
--- a/mk/test.mk
+++ b/mk/test.mk
@@ -144,11 +144,12 @@ all: $(addsuffix .__all, $(SUBDIRS_ALL))
 # Implied by 'all' for each directory, but we cannot write 'all: verify' or we
 # will get duplicate invocations for all/verify on a same subdir, and they overlap.
 SUBDIRS_VERIFY += $(SUBDIRS)
-ifeq ($(NOVERIFY),)
 __verify: $(ALL_CHECKED_FILES)
-endif
-__verify: $(addsuffix .__verify, $(SUBDIRS_VERIFY))
+verify: $(addsuffix .__verify, $(SUBDIRS_VERIFY))
 verify: __verify
+ifeq ($(NOVERIFY),)
+all: __verify
+endif
 
 # clean
 SUBDIRS_CLEAN += $(SUBDIRS)