Fix karamel tests

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

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.
 

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"

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:

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

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)