tests: rework makefiles

Makefile

@@ -190,8 +190,7 @@ ci-post:						\
 	ci-ulib-in-fsharp				\
 	ci-ocaml-test					\
 	ci-uregressions					\
-	$(if $(FSTAR_CI_TEST_KARAMEL),ci-karamel-test,)	\
-	ci-ulib-extra
+	$(if $(FSTAR_CI_TEST_KARAMEL),ci-karamel-test,)
 
 .PHONY: ci-uregressions
 ci-uregressions:

mk/common.mk

@@ -0,0 +1,92 @@
+# This makefile is included from several other makefiles in the tree.
+
+MAKEFLAGS += --no-builtin-rules
+Q?=@
+SIL?=--silent
+RUNLIM=
+ifneq ($(V),)
+	Q=
+	SIL=
+else
+	MAKEFLAGS += -s
+endif
+
+define NO_RUNLIM_ERR
+runlim not found:
+  To use RESOURCEMONITOR=1, the `runlim` tool must be installed and in your $$PATH.
+  It must also be a recent version supporting the `-p` option.
+  You can get it from: [https://github.com/arminbiere/runlim]
+endef
+
+define msg =
+@printf "   %-14s  %s\n" $(1) $(2)
+endef
+define bold_msg =
+@#-tput bold 2>/dev/null
+@printf -- "  %-15s" $(1)
+@#-tput sgr0 2>/dev/null
+@printf "  %s\n" $(2)
+endef
+
+# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
+# information about the time and space taken by each F* invocation.
+ifneq ($(RESOURCEMONITOR),)
+	ifeq ($(shell which runlim),)
+		_ := $(error $(NO_RUNLIM_ERR)))
+	endif
+	ifneq ($(MONID),)
+		MONPREFIX=$(MONID).
+	endif
+	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
+endif
+
+# Ensure that any failing rule will not create its target file.
+# In other words, make `make` less insane.
+.DELETE_ON_ERROR:
+
+.DEFAULT_GOAL:=__undef
+.PHONY: __undef
+__undef:
+	$(error "This makefile does not have a default goal")
+
+# Check that a variable is defined. If not, abort with an (optional) error message.
+need =												\
+  $(if $(value $(strip $1)),,									\
+    $(error Need a value for $(strip $1)$(if $2, ("$(strip $2)"))))
+
+# Check that a variable is defined and pointing to an executable.
+# Is there no negation in make...?
+# Wew! this was interesting to write. Especially the override part.
+need_exe =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -x $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+    $(error Need an executable for $(strip $1)$(if $2, ("$(strip $2)"))))			\
+
+need_file =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -f $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+    $(error Need a file path for $(strip $1)$(if $2, ("$(strip $2)"))))				\
+
+need_dir =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -d $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") is not a directory (cwd = $(CURDIR)))),	\
+    $(error Need an *existing* directory path for $(strip $1)$(if $2, ("$(strip $2)"))))	\
+
+need_dir_mk =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(shell mkdir -p $(value $(strip $1)) && echo 1),					\
+      $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+      $(error $(strip $1) ("$(value $(strip $1))") is not a directory (mkdir failed, cwd = $(CURDIR)))),	\
+    $(error Need a directory path for $(strip $1)$(if $2, ("$(strip $2)"))))			\

mk/test.mk

@@ -0,0 +1,79 @@
+# Include this makefile for unit tests. It mostly has all you need.
+# This is NOT meant for external consumption. Do not point to this.
+
+ifeq ($(FSTAR_ROOT),)
+  $(error FSTAR_ROOT is not set. Please set it to the root of your F* repository)
+endif
+include $(FSTAR_ROOT)/mk/common.mk
+.DEFAULT_GOAL := all
+
+# Set a default FSTAR_EXE for most clients.
+FSTAR_EXE ?= $(FSTAR_ROOT)/bin/fstar.exe
+
+OCAMLOPT := $(FSTAR_EXE) --ocamlenv ocamlfind opt
+
+HINTS_ENABLED?=--use_hints
+
+# This warning is really useless.
+OTHERFLAGS += --warn_error -321
+OTHERFLAGS += --ext context_pruning
+
+# Set ADMIT=1 to admit queries
+ADMIT ?=
+MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
+
+OUTPUT_DIR ?= _output
+CACHE_DIR ?= _cache
+
+FSTAR = $(FSTAR_EXE) $(SIL) 				\
+	--cache_checked_modules				\
+	--odir $(OUTPUT_DIR)				\
+	--cache_dir $(CACHE_DIR)			\
+	--already_cached Prims,FStar			\
+	 $(OTHERFLAGS) $(MAYBE_ADMIT) $(HINTS_ENABLED)
+
+ifeq ($(NODEPEND),)
+FSTAR_FILES ?= $(wildcard *.fst) $(wildcard *.fsti)
+$(call need, FSTAR_FILES, "List of F* files to verify. It defaults to all fst/fsti in the directory (none were found)")
+
+.depend: $(FSTAR_FILES)
+	$(call msg, "DEPEND", $(CURDIR))
+	$(FSTAR) --dep full $(FSTAR_FILES) --output_deps_to $@
+depend: .depend
+include .depend
+endif
+
+%.fst.checked:
+	$(call msg, "CHECK", $(basename $(notdir $@)))
+	$(FSTAR) $<
+	touch -c $@
+
+%.fsti.checked:
+	$(call msg, "CHECK", $(basename $(notdir $@)))
+	$(FSTAR) $<
+	touch -c $@
+
+%.fst.output: %.fst
+	$(call msg, "OUTPUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format human -f --print_expected_failures $< >$@ 2>&1
+
+%.fsti.output: %.fsti
+	$(call msg, "OUTPUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format human -f --print_expected_failures $< >$@ 2>&1
+
+%.fst.json_output: %.fst
+	$(call msg, "JSONOUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1
+
+%.fsti.json_output: %.fsti
+	$(call msg, "JSONOUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1
+
+$(OUTPUT_DIR)/%.ml:
+	$(call msg, "EXTRACT", $(basename $(notdir $@)))
+	$(FSTAR) $(subst .checked,,$(notdir $<)) --codegen OCaml --extract_module $(subst .fst.checked,,$(notdir $<))
+
+verify-all: $(ALL_CHECKED_FILES)
+
+clean:
+	rm -rf $(OUTPUT_DIR) $(CACHE_DIR) .depend

tests/.gitignore

@@ -0,0 +1,2 @@
+_cache
+_output

tests/Cfg.fst.config.json

@@ -0,0 +1,8 @@
+{
+  "fstar_exe": "../bin/fstar.exe",
+  "options": [
+    "--ext", "context_pruning"
+  ],
+  "include_dirs": [
+  ]
+}

tests/Makefile

@@ -1,31 +1,30 @@
-FSTAR_HOME=..
-export OTHERFLAGS += --ext context_pruning
-include ../examples/Makefile.include
+FSTAR_ROOT ?= ..
+# include $(FSTAR_ROOT)/mk/test.mk
+# ^ No need to include this here, we are just descending to other directories
 
 ALL_TEST_DIRS += bug-reports
+ALL_TEST_DIRS += simple_hello
+ALL_TEST_DIRS += dune_hello
+ALL_TEST_DIRS += semiring
 ALL_TEST_DIRS += coercions
 ALL_TEST_DIRS += error-messages
+ALL_TEST_DIRS += tactics
 ALL_TEST_DIRS += friends
 ALL_TEST_DIRS += ide
 ALL_TEST_DIRS += incl
 ALL_TEST_DIRS += machine_integers
 ALL_TEST_DIRS += micro-benchmarks
 ALL_TEST_DIRS += prettyprinting
 ALL_TEST_DIRS += projectors
+ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += restricted_includes
-ALL_TEST_DIRS += semiring
 ALL_TEST_DIRS += struct
-ALL_TEST_DIRS += tactics
-ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
-ALL_TEST_DIRS += simple_hello
-ALL_TEST_DIRS += dune_hello
-HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
+ALL_TEST_DIRS += calc
 
-ifneq (,$(HAS_OCAML))
+# GM: I am unconditionally enabling this.
 ALL_TEST_DIRS += extraction
-endif
 
 all: $(addsuffix .all, $(ALL_TEST_DIRS))
 clean: $(addsuffix .clean, $(ALL_TEST_DIRS))

tests/bug-reports/Makefile

@@ -1,10 +1,11 @@
-FSTAR_HOME=../..
-include $(FSTAR_HOME)/examples/Makefile.include
-include $(FSTAR_HOME)/ulib/ml/Makefile.include
+include Makefile.include
+# ^ stopgap so I don't have to rewrite this entire makefile (yet)
+# but the right thing to do is include /mk/test.mk and rewrite this.
 
 OTHERFLAGS+=--warn_error +240
 
-all: verify iverify not-verify extract
+all: verify iverify not-verify # extract
+.DEFAULT_GOAL := all
 
 ##################
 # Positive tests #
@@ -177,6 +178,9 @@ Bug1383.verify: OTHERFLAGS += --warn_error @275 #Z3 warnings are fatal
 Bug1694.verify: OTHERFLAGS += --codegen OCaml
 Bug2210.verify: OTHERFLAGS += --codegen OCaml
 
+# Disable hints, see #3572
+Bug1614a.verify: HINTS_ENABLED =
+
 Bug2684a.verify: OTHERFLAGS += --cache_checked_modules
 Bug2684b.verify: OTHERFLAGS += --cache_checked_modules
 Bug2684c.verify: OTHERFLAGS += --cache_checked_modules