From 34f36186485449570de2cc75fd1ba7a695e41fb6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 16 Oct 2024 15:57:05 -0700
Subject: [PATCH] tests: rework makefiles

This is part of the new build, but self-contained enough to be merged
before that. It unifies most makefiles in tests/ into a single
mk/test.mk (mk is a new top-level directory for make infra).

It also disconnects examples/ and tests/. The mutually recursive
inclusions are hard to work with.
---
 examples/calc/Makefile                        |  11 --
 mk/common.mk                                  |  92 +++++++++++++++
 mk/test.mk                                    |  79 +++++++++++++
 tests/.gitignore                              |   2 +
 tests/Cfg.fst.config.json                     |   8 ++
 tests/Makefile                                |  21 ++--
 tests/bug-reports/Makefile                    |  12 +-
 tests/bug-reports/Makefile.include            |  12 ++
 {examples => tests}/calc/BasicTests.fst       |   0
 {examples => tests}/calc/BasicTests.fst.hints |   0
 {examples => tests}/calc/CalcImpl.fst         |   0
 {examples => tests}/calc/CalcImpl.fst.hints   |   0
 {examples => tests}/calc/CalcInference.fst    |   0
 .../calc/CalcInference.fst.hints              |   0
 {examples => tests}/calc/CalcTest.fst         |   0
 {examples => tests}/calc/CalcTest.fst.hints   |   0
 {examples => tests}/calc/Long.fst             |   0
 {examples => tests}/calc/Long.fst.hints       |   0
 tests/calc/Makefile                           |   3 +
 {examples => tests}/calc/SeqCalc.fst          |   0
 {examples => tests}/calc/SeqCalc.fst.hints    |   0
 tests/coercions/Makefile                      |  15 +--
 tests/error-messages/Bug                      |   0
 tests/error-messages/Makefile                 |  13 +--
 tests/extraction/Makefile                     |  18 ++-
 tests/extraction/Makefile.common              | 109 ------------------
 tests/extraction/cmi/0/Makefile               |  17 ++-
 tests/extraction/cmi/1/Makefile               |  17 ++-
 tests/extraction/cmi/2/Makefile               |  15 +--
 tests/extraction/cmi/Makefile                 |   6 +-
 tests/extraction/cmi/Makefile.common          |  29 -----
 tests/friends/1/Makefile                      |  23 +---
 tests/friends/2/Makefile                      |  23 +---
 tests/friends/3/Makefile                      |  23 +---
 tests/friends/Makefile                        |   6 +-
 tests/hacl/Makefile                           |  16 +--
 tests/ide/Makefile                            |  21 ++--
 tests/ide/Makefile.common                     |  17 ++-
 tests/ide/emacs/FStarMode_GH73.out.expected   |   2 +-
 tests/ide/emacs/Makefile                      |  17 +--
 tests/ide/emacs/Search.cons-snoc.out.expected |   3 +-
 tests/ide/emacs/Tutorial.push.out.expected    |   2 +-
 tests/ide/lsp/Makefile                        |   6 +-
 tests/incl/Makefile                           |   4 -
 tests/incl/Makefile.sub                       |   6 +-
 tests/machine_integers/.gitignore             |   1 +
 tests/machine_integers/Makefile               |  34 ++----
 tests/micro-benchmarks/Makefile               |  29 ++---
 tests/micro-benchmarks/ns_resolution/Makefile |  15 +--
 tests/prettyprinting/Makefile                 |  33 +++---
 tests/projectors/Makefile                     |  16 +--
 tests/restricted_includes/Makefile            |  16 +--
 tests/semiring/Makefile                       |  29 +++--
 tests/simple_hello/Makefile                   |   5 +-
 tests/struct/Makefile                         |   6 +-
 tests/struct/Makefile.sub                     |  10 +-
 tests/tactics/Makefile                        |  22 ++--
 tests/typeclasses/Makefile                    |  16 +--
 tests/vale/Makefile                           |  23 +---
 59 files changed, 381 insertions(+), 522 deletions(-)
 delete mode 100644 examples/calc/Makefile
 create mode 100644 mk/common.mk
 create mode 100644 mk/test.mk
 create mode 100644 tests/.gitignore
 create mode 100644 tests/Cfg.fst.config.json
 create mode 100644 tests/bug-reports/Makefile.include
 rename {examples => tests}/calc/BasicTests.fst (100%)
 rename {examples => tests}/calc/BasicTests.fst.hints (100%)
 rename {examples => tests}/calc/CalcImpl.fst (100%)
 rename {examples => tests}/calc/CalcImpl.fst.hints (100%)
 rename {examples => tests}/calc/CalcInference.fst (100%)
 rename {examples => tests}/calc/CalcInference.fst.hints (100%)
 rename {examples => tests}/calc/CalcTest.fst (100%)
 rename {examples => tests}/calc/CalcTest.fst.hints (100%)
 rename {examples => tests}/calc/Long.fst (100%)
 rename {examples => tests}/calc/Long.fst.hints (100%)
 create mode 100644 tests/calc/Makefile
 rename {examples => tests}/calc/SeqCalc.fst (100%)
 rename {examples => tests}/calc/SeqCalc.fst.hints (100%)
 delete mode 100644 tests/error-messages/Bug
 delete mode 100644 tests/extraction/Makefile.common
 delete mode 100644 tests/extraction/cmi/Makefile.common

diff --git a/examples/calc/Makefile b/examples/calc/Makefile
deleted file mode 100644
index fe0e5f6e667..00000000000
--- a/examples/calc/Makefile
+++ /dev/null
@@ -1,11 +0,0 @@
-EXCLUDED_FSTAR_FILES=Launch.fst Test.Math.Lemmas.fst CanonDeep.fst Poly1.fst Poly2.fst
-FSTAR_FILES = $(filter-out $(EXCLUDED_FSTAR_FILES), $(wildcard *.fst))
-
-all: verify-all
-
-$(CACHE_DIR):
-	mkdir -p $@
-
-include ../Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
diff --git a/mk/common.mk b/mk/common.mk
new file mode 100644
index 00000000000..49e16828c89
--- /dev/null
+++ b/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)"))))			\
diff --git a/mk/test.mk b/mk/test.mk
new file mode 100644
index 00000000000..7419f175f94
--- /dev/null
+++ b/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
diff --git a/tests/.gitignore b/tests/.gitignore
new file mode 100644
index 00000000000..d6ce352b348
--- /dev/null
+++ b/tests/.gitignore
@@ -0,0 +1,2 @@
+_cache
+_output
diff --git a/tests/Cfg.fst.config.json b/tests/Cfg.fst.config.json
new file mode 100644
index 00000000000..33824b76ec5
--- /dev/null
+++ b/tests/Cfg.fst.config.json
@@ -0,0 +1,8 @@
+{
+  "fstar_exe": "../bin/fstar.exe",
+  "options": [
+    "--ext", "context_pruning"
+  ],
+  "include_dirs": [
+  ]
+}
diff --git a/tests/Makefile b/tests/Makefile
index e864166662f..264abb62407 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,10 +1,14 @@
-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
@@ -12,20 +16,15 @@ 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))
diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
index fc290c24d62..07ea22963c5 100644
--- a/tests/bug-reports/Makefile
+++ b/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
diff --git a/tests/bug-reports/Makefile.include b/tests/bug-reports/Makefile.include
new file mode 100644
index 00000000000..7836f1999fe
--- /dev/null
+++ b/tests/bug-reports/Makefile.include
@@ -0,0 +1,12 @@
+FSTAR_EXE ?= ../../bin/fstar.exe
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/common.mk
+include $(FSTAR_ROOT)/ulib/gmake/fstar.mk
+
+# we ignore the return result in benchmark runs because we can have micro-benchmarks which
+# produce error asserts when executed with '--admit_smt_queries true'
+%.uver: %.fst
+	$(Q)$(BENCHMARK_PRE) $(FSTAR)  $^
+
+%.fail-uver: %.fst
+	(! $(FSTAR) $^ >/dev/null 2>&1) || (echo "NEGATIVE TEST FAILED ($@)!" ; false)
diff --git a/examples/calc/BasicTests.fst b/tests/calc/BasicTests.fst
similarity index 100%
rename from examples/calc/BasicTests.fst
rename to tests/calc/BasicTests.fst
diff --git a/examples/calc/BasicTests.fst.hints b/tests/calc/BasicTests.fst.hints
similarity index 100%
rename from examples/calc/BasicTests.fst.hints
rename to tests/calc/BasicTests.fst.hints
diff --git a/examples/calc/CalcImpl.fst b/tests/calc/CalcImpl.fst
similarity index 100%
rename from examples/calc/CalcImpl.fst
rename to tests/calc/CalcImpl.fst
diff --git a/examples/calc/CalcImpl.fst.hints b/tests/calc/CalcImpl.fst.hints
similarity index 100%
rename from examples/calc/CalcImpl.fst.hints
rename to tests/calc/CalcImpl.fst.hints
diff --git a/examples/calc/CalcInference.fst b/tests/calc/CalcInference.fst
similarity index 100%
rename from examples/calc/CalcInference.fst
rename to tests/calc/CalcInference.fst
diff --git a/examples/calc/CalcInference.fst.hints b/tests/calc/CalcInference.fst.hints
similarity index 100%
rename from examples/calc/CalcInference.fst.hints
rename to tests/calc/CalcInference.fst.hints
diff --git a/examples/calc/CalcTest.fst b/tests/calc/CalcTest.fst
similarity index 100%
rename from examples/calc/CalcTest.fst
rename to tests/calc/CalcTest.fst
diff --git a/examples/calc/CalcTest.fst.hints b/tests/calc/CalcTest.fst.hints
similarity index 100%
rename from examples/calc/CalcTest.fst.hints
rename to tests/calc/CalcTest.fst.hints
diff --git a/examples/calc/Long.fst b/tests/calc/Long.fst
similarity index 100%
rename from examples/calc/Long.fst
rename to tests/calc/Long.fst
diff --git a/examples/calc/Long.fst.hints b/tests/calc/Long.fst.hints
similarity index 100%
rename from examples/calc/Long.fst.hints
rename to tests/calc/Long.fst.hints
diff --git a/tests/calc/Makefile b/tests/calc/Makefile
new file mode 100644
index 00000000000..e1e94ee097f
--- /dev/null
+++ b/tests/calc/Makefile
@@ -0,0 +1,3 @@
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
+all: verify-all
diff --git a/examples/calc/SeqCalc.fst b/tests/calc/SeqCalc.fst
similarity index 100%
rename from examples/calc/SeqCalc.fst
rename to tests/calc/SeqCalc.fst
diff --git a/examples/calc/SeqCalc.fst.hints b/tests/calc/SeqCalc.fst.hints
similarity index 100%
rename from examples/calc/SeqCalc.fst.hints
rename to tests/calc/SeqCalc.fst.hints
diff --git a/tests/coercions/Makefile b/tests/coercions/Makefile
index bb98c2bec1c..e1e94ee097f 100644
--- a/tests/coercions/Makefile
+++ b/tests/coercions/Makefile
@@ -1,14 +1,3 @@
-FSTAR_HOME=../..
-
-FSTAR_FILES = $(wildcard *.fst)
-
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	rm -f .depend
-	rm -rf _cache
-	rm -rf _output
diff --git a/tests/error-messages/Bug b/tests/error-messages/Bug
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/tests/error-messages/Makefile b/tests/error-messages/Makefile
index 291cf343595..3210f2d64cf 100644
--- a/tests/error-messages/Makefile
+++ b/tests/error-messages/Makefile
@@ -1,7 +1,6 @@
-FSTAR_HOME=../..
-all: check-all
-
-FSTAR_FILES=$(wildcard *.fst)
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
+all: $(if $(ACCEPT),accept,check-all)
 
 # This so that we don't get warnings about:
 # 241: "unable to load checked file"
@@ -9,11 +8,6 @@ FSTAR_FILES=$(wildcard *.fst)
 # 333: "unable to read hints"
 OTHERFLAGS+=--warn_error -241-247-333-274+240
 
-# Sorry, without this we can get noise in error locations.
-# See issue #1993. Also, warnings from dependencies would
-# pollute the output.
-OTHERFLAGS+=--already_cached 'Prims FStar'
-
 # Remove --query_stats and --hint_info from this subdir, since
 # they output timing info.
 OTHERFLAGS := $(filter-out --query_stats, $(OTHERFLAGS))
@@ -53,7 +47,6 @@ TuplePat.fst.output      : OTHERFLAGS+=--dump_module TuplePat
 Monoid.fst.json_output   : OTHERFLAGS+=--dump_module Monoid
 Monoid.fst.output        : OTHERFLAGS+=--dump_module Monoid
 
-include $(FSTAR_HOME)/examples/Makefile.common
 
 .PHONY: %.human_check
 %.human_check: %.expected %.output
diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile
index 9d601ca8897..9ef4e2fb56b 100644
--- a/tests/extraction/Makefile
+++ b/tests/extraction/Makefile
@@ -1,12 +1,12 @@
-FSTAR_EXAMPLES=$(realpath ../../examples)
-include $(FSTAR_EXAMPLES)/Makefile.include
-include $(FSTAR_ULIB)/ml/Makefile.include
+FSTAR_ROOT ?= ../..
+NODEPEND=1
+include $(FSTAR_ROOT)/mk/test.mk
 
 all: inline_let all_cmi Eta_expand.test Div.test ExtractAs.test
 
-%.exe: %.fst | out
-	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml $<
-	$(OCAMLOPT) out/$(patsubst %.fst,%.ml,$<) -o $@
+%.exe: %.fst
+	$(FSTAR) --codegen OCaml $<
+	$(OCAMLOPT) -package fstar.lib -linkpkg $(OUTPUT_DIR)/$(patsubst %.fst,%.ml,$<) -o $@
 
 %.test: %.exe
 	$(call msg,RUN,$<)
@@ -22,19 +22,15 @@ Div.test: Div.exe
 
 inline_let: InlineLet.fst
 	$(FSTAR) --codegen OCaml InlineLet.fst
-	egrep -A 10 test InlineLet.ml | grep -qs "17"
+	egrep -A 10 test $(OUTPUT_DIR)/InlineLet.ml | grep -qs "17"
 	@touch $@
 
 all_cmi:
 	+$(MAKE) -C cmi all
 
-out:
-	mkdir -p out
-
 clean:
 	rm -rf out
 	rm -f *.exe
 	rm -f *~
 	rm -f *.exe *.test
 	rm -f inline_let
-
diff --git a/tests/extraction/Makefile.common b/tests/extraction/Makefile.common
deleted file mode 100644
index ad642c601a6..00000000000
--- a/tests/extraction/Makefile.common
+++ /dev/null
@@ -1,109 +0,0 @@
-ifdef FSTAR_HOME
-  FSTAR_ULIB=$(shell if test -d $(FSTAR_HOME)/ulib ; then echo $(FSTAR_HOME)/ulib ; else echo $(FSTAR_HOME)/lib/fstar ; fi)
-else
-  # FSTAR_HOME not defined, assume fstar.exe installed through opam
-  # or binary package, and reachable from PATH
-  FSTAR_ULIB=$(dir $(shell which fstar.exe))/../lib/fstar
-endif
-include $(FSTAR_ULIB)/gmake/z3.mk
-include $(FSTAR_ULIB)/gmake/fstar.mk
-
-#for getting macros for OCaml commands to compile extracted code
-include $(FSTAR_ULIB)/ml/Makefile.include
-
-ifdef FSTAR_HOME
-  -include $(FSTAR_HOME)/.common.mk
-  FSTAR=$(FSTAR_HOME)/bin/fstar.exe
-else
-  FSTAR=fstar.exe
-endif
-
-#################################################################################
-# Customize these variables for your project
-#################################################################################
-
-# The root files of your project, from which to begin scanning dependences
-FSTAR_FILES ?=
-
-# The paths to related files which to include for scanning
-#   -- No need to add FSTAR_HOME/ulib; it is included by default
-INCLUDE_PATHS ?=
-
-# The executable file you want to produce
-PROGRAM ?=
-
-# A driver in ML to call into your program
-TOP_LEVEL_FILE ?=
-
-# A place to put all the emitted .ml files
-OUTPUT_DIRECTORY ?= _output
-
-# A place to put all the .checked files
-CACHE_DIR ?= _cache
-
-# Set ADMIT=1 to admit queries
-ADMIT ?=
-MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
-
-################################################################################
-# YOU SHOULDN'T NEED TO TOUCH THE REST
-################################################################################
-
-VERBOSE_FSTAR=$(BENCHMARK_PRE) $(FSTAR)                     \
-		  --cache_checked_modules                   \
-		  --odir $(OUTPUT_DIRECTORY)                \
-		  --cache_dir $(CACHE_DIR)                  \
-		  $(addprefix --include , $(INCLUDE_PATHS)) \
-		  $(OTHERFLAGS) $(MAYBE_ADMIT)
-
-# As above, but perhaps with --silent, and perhaps with a prefix (usually for monitoring)
-MY_FSTAR=$(RUNLIM) $(VERBOSE_FSTAR) $(SIL)
-
-#--------------------------------------------------------------------------------
-# Default target: verify all FSTAR_FILES
-#--------------------------------------------------------------------------------
-
-#--------------------------------------------------------------------------------
-# Include the .depend before any other target
-# since we rely on the dependences it computes in other rules
-# #
-# We do an indirection via ._depend so we don't write an empty file if
-# the dependency analysis failed.
-#--------------------------------------------------------------------------------
-.depend: $(FSTAR_FILES)
-	$(Q)$(MY_FSTAR) --dep full $(FSTAR_FILES) --output_deps_to $@
-
-depend: .depend
-
-include .depend
-#--------------------------------------------------------------------------------
-
-# a.fst.checked is the binary, checked version of a.fst
-%.fst.checked:
-	$(call msg, "CHECK", $(basename $(notdir $@)))
-	$(Q)$(MY_FSTAR) $<
-	@touch -c $@
-
-# a.fsti.checked is the binary, checked version of a.fsti
-%.fsti.checked:
-	$(call msg, "CHECK", $(basename $(notdir $@)))
-	$(Q)$(MY_FSTAR) $<
-	@touch -c $@
-
-%.fst.output: %.fst
-	$(call msg, "OUTPUT", $(basename $(notdir $@)))
-	$(Q)$(VERBOSE_FSTAR) -f --print_expected_failures $< >$@ 2>&1
-
-%.fsti.output: %.fsti
-	$(call msg, "OUTPUT", $(basename $(notdir $@)))
-	$(Q)$(VERBOSE_FSTAR) -f --print_expected_failures $< >$@ 2>&1
-
-clean:
-	rm -rf $(CACHE_DIR)
-
-#----------------------------------------------------------------------------------
-
-#extract F* files to OCaml
-$(OUTPUT_DIRECTORY)/%.ml:
-	$(call msg, "EXTRACT", $(basename $(notdir $@)))
-	$(Q)$(MY_FSTAR) $(subst .checked,,$(notdir $<)) --codegen OCaml --extract_module $(subst .fst.checked,,$(notdir $<))
diff --git a/tests/extraction/cmi/0/Makefile b/tests/extraction/cmi/0/Makefile
index c6b5fdd088f..068dafb4d4d 100644
--- a/tests/extraction/cmi/0/Makefile
+++ b/tests/extraction/cmi/0/Makefile
@@ -4,17 +4,14 @@
 ### A.id remains, since it should have been inlined
 ################################################################################
 
-# This is needed because ../Makefile.common includes
-# ../../../Makefile.common, but GNU Make does not support chained
-# includes with relative paths
-FSTAR_EXAMPLES = $(realpath ../../../../examples)
-
-ROOTS=B.fst
-EXTRACT=A B
+FSTAR_ROOT ?= ../../../..
+OTHERFLAGS += --cmi
+include $(FSTAR_ROOT)/mk/test.mk
 
 all: test
 
-include ../Makefile.common
+$(OUTPUT_DIR)/%.ml: %.fst.checked
+	$(FSTAR) --codegen OCaml --extract $* $*.fst
 
-test: B.ml
-	egrep test_function B.ml | egrep -q -v A.id #test that A.id is inlined
+test: $(OUTPUT_DIR)/B.ml
+	egrep test_function $< | egrep -q -v A.id #test that A.id is inlined
diff --git a/tests/extraction/cmi/1/Makefile b/tests/extraction/cmi/1/Makefile
index 29af8d6cf22..437abea837e 100644
--- a/tests/extraction/cmi/1/Makefile
+++ b/tests/extraction/cmi/1/Makefile
@@ -7,17 +7,14 @@
 ### lack implementations
 ################################################################################
 
-# This is needed because ../Makefile.common includes
-# ../../../Makefile.common, but GNU Make does not support chained
-# includes with relative paths
-FSTAR_EXAMPLES = $(realpath ../../../../examples)
-
-ROOTS=B.fst
-EXTRACT=A B
+FSTAR_ROOT ?= ../../../..
+OTHERFLAGS += --cmi
+include $(FSTAR_ROOT)/mk/test.mk
 
 all: test
 
-include ../Makefile.common
+$(OUTPUT_DIR)/%.ml: %.fst.checked
+	$(FSTAR) --codegen OCaml --extract $* $*.fst
 
-test: B.ml
-	egrep test_function B.ml | egrep -q -v A.id #test that A.id is inlined
+test: $(OUTPUT_DIR)/B.ml
+	egrep test_function $< | egrep -q -v A.id #test that A.id is inlined
diff --git a/tests/extraction/cmi/2/Makefile b/tests/extraction/cmi/2/Makefile
index 0a82d5be09a..3f11732a1ea 100644
--- a/tests/extraction/cmi/2/Makefile
+++ b/tests/extraction/cmi/2/Makefile
@@ -7,17 +7,14 @@
 ### lack implementations
 ################################################################################
 
-# This is needed because ../Makefile.common includes
-# ../../../Makefile.common, but GNU Make does not support chained
-# includes with relative paths
-FSTAR_EXAMPLES = $(realpath ../../../../examples)
-
-ROOTS=Test.fst
-EXTRACT=Test
+FSTAR_ROOT ?= ../../../..
+OTHERFLAGS += --cmi
+include $(FSTAR_ROOT)/mk/test.mk
 
 all: test
 
-include ../Makefile.common
+$(OUTPUT_DIR)/%.ml: %.fst.checked
+	$(FSTAR) --codegen OCaml --extract $* $*.fst
 
-test: Test.ml
+test: $(OUTPUT_DIR)/Test.ml
 	egrep M.f $^ | egrep -q -v magic  #test that there is no magic in the call to M.f; fragile
diff --git a/tests/extraction/cmi/Makefile b/tests/extraction/cmi/Makefile
index 3d20fbcc01a..bf645a16f8d 100644
--- a/tests/extraction/cmi/Makefile
+++ b/tests/extraction/cmi/Makefile
@@ -1,7 +1,7 @@
 all:
-	+$(MAKE) -C 0
-	+$(MAKE) -C 1
-	+$(MAKE) -C 2
+	+$(MAKE) -C 0 all
+	+$(MAKE) -C 1 all
+	+$(MAKE) -C 2 all
 
 clean:
 	+$(MAKE) -C 0 clean
diff --git a/tests/extraction/cmi/Makefile.common b/tests/extraction/cmi/Makefile.common
deleted file mode 100644
index 719c8514927..00000000000
--- a/tests/extraction/cmi/Makefile.common
+++ /dev/null
@@ -1,29 +0,0 @@
-ifndef FSTAR_EXAMPLES
-  $(error FSTAR_EXAMPLES must be defined)
-endif
-
-ROOTS?=
-EXTRACT?=
-
-include $(FSTAR_EXAMPLES)/Makefile.include
-include .depend
-
-OTHERFLAGS+=--cache_dir .cache
-
-%.fst.checked:
-	$(FSTAR) $< --cache_checked_modules
-
-%.fsti.checked:
-	$(FSTAR) $< --cache_checked_modules
-
-%.ml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml --extract_module $(basename $(notdir $(subst .checked,,$<))) --cmi
-
-.depend:
-	mkdir -p .cache
-	$(FSTAR) --dep full $(ROOTS) $(addprefix --extract ,$(ROOTS)) --cmi > .depend
-
-depend: .depend
-
-clean:
-	rm -rf .depend *.ml *.checked *~ .cache
diff --git a/tests/friends/1/Makefile b/tests/friends/1/Makefile
index 002dfbd744f..0f60780cf89 100644
--- a/tests/friends/1/Makefile
+++ b/tests/friends/1/Makefile
@@ -1,22 +1,3 @@
-FSTAR_HOME=../../..
-
+FSTAR_ROOT ?= ../../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include .depend
-include $(FSTAR_HOME)/examples/Makefile.include
-
-verify-all: $(ALL_CHECKED_FILES)
-
-.depend:
-	$(call msg, "DEPEND", $(patsubst $(shell realpath $(FSTAR_HOME))/%,%/,$(shell pwd)))
-	$(Q)$(FSTAR) --dep full $(wildcard *.fst *.fsti) --output_deps_to .depend
-
-%.checked:
-	$(call msg, "CHECK", $<)
-	$(Q)$(FSTAR) $(SIL) --cache_checked_modules $<
-	$(Q)touch -c $@
-
-clean:
-	rm -f .depend *.checked
-
-depend: .depend
diff --git a/tests/friends/2/Makefile b/tests/friends/2/Makefile
index 002dfbd744f..0f60780cf89 100644
--- a/tests/friends/2/Makefile
+++ b/tests/friends/2/Makefile
@@ -1,22 +1,3 @@
-FSTAR_HOME=../../..
-
+FSTAR_ROOT ?= ../../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include .depend
-include $(FSTAR_HOME)/examples/Makefile.include
-
-verify-all: $(ALL_CHECKED_FILES)
-
-.depend:
-	$(call msg, "DEPEND", $(patsubst $(shell realpath $(FSTAR_HOME))/%,%/,$(shell pwd)))
-	$(Q)$(FSTAR) --dep full $(wildcard *.fst *.fsti) --output_deps_to .depend
-
-%.checked:
-	$(call msg, "CHECK", $<)
-	$(Q)$(FSTAR) $(SIL) --cache_checked_modules $<
-	$(Q)touch -c $@
-
-clean:
-	rm -f .depend *.checked
-
-depend: .depend
diff --git a/tests/friends/3/Makefile b/tests/friends/3/Makefile
index 002dfbd744f..0f60780cf89 100644
--- a/tests/friends/3/Makefile
+++ b/tests/friends/3/Makefile
@@ -1,22 +1,3 @@
-FSTAR_HOME=../../..
-
+FSTAR_ROOT ?= ../../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include .depend
-include $(FSTAR_HOME)/examples/Makefile.include
-
-verify-all: $(ALL_CHECKED_FILES)
-
-.depend:
-	$(call msg, "DEPEND", $(patsubst $(shell realpath $(FSTAR_HOME))/%,%/,$(shell pwd)))
-	$(Q)$(FSTAR) --dep full $(wildcard *.fst *.fsti) --output_deps_to .depend
-
-%.checked:
-	$(call msg, "CHECK", $<)
-	$(Q)$(FSTAR) $(SIL) --cache_checked_modules $<
-	$(Q)touch -c $@
-
-clean:
-	rm -f .depend *.checked
-
-depend: .depend
diff --git a/tests/friends/Makefile b/tests/friends/Makefile
index 1178d1724e3..c7ab8ff3561 100644
--- a/tests/friends/Makefile
+++ b/tests/friends/Makefile
@@ -1,11 +1,11 @@
+# FSTAR_ROOT ?= ../..
+# include $(FSTAR_ROOT)/mk/test.mk
+
 DIRS=1 2 3
 
 all: $(addsuffix .all, $(DIRS))
 clean: $(addsuffix .clean, $(DIRS))
 
-FSTAR_HOME=../..
-include $(FSTAR_HOME)/examples/Makefile.include
-
 %.all: %
 	+$(MAKE) -C $* all
 
diff --git a/tests/hacl/Makefile b/tests/hacl/Makefile
index ccee95fd891..6de34439627 100644
--- a/tests/hacl/Makefile
+++ b/tests/hacl/Makefile
@@ -1,14 +1,4 @@
-FSTAR_HOME=../..
-
-FSTAR_FILES = $(wildcard *.fst *.fsti)
-OTHERFLAGS += --ext context_pruning --z3rlimit_factor 2
+FSTAR_ROOT?=../..
+include $(FSTAR_ROOT)/mk/test.mk
+OTHERFLAGS += --z3rlimit_factor 2
 all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	rm -f .depend
-	rm -rf _cache
-	rm -rf _output
diff --git a/tests/ide/Makefile b/tests/ide/Makefile
index 19f1d50bcc5..a544ba0d063 100644
--- a/tests/ide/Makefile
+++ b/tests/ide/Makefile
@@ -1,24 +1,23 @@
-FSTAR_HOME=../..
-include ../../examples/Makefile.include
+FSTAR_ROOT ?= ../..
+NODEPEND=1
+include $(FSTAR_ROOT)/mk/test.mk
 
-ALL_TEST_DIRS=\
-lsp \
-emacs
+ALL_TEST_DIRS += lsp
+ALL_TEST_DIRS += emacs
 
 all: $(addsuffix .all, $(ALL_TEST_DIRS)) test_incremental
+clean: $(addsuffix .clean, $(ALL_TEST_DIRS))
 
-INCR_TEST_FILES := $(wildcard $(FSTAR_HOME)/ulib/*.fst  $(FSTAR_HOME)/ulib/*.fsti)
+INCR_TEST_FILES := $(wildcard $(FSTAR_ROOT)/ulib/*.fst  $(FSTAR_ROOT)/ulib/*.fsti)
 
 .PHONY: test_incremental
-test_incremental: $(patsubst $(FSTAR_HOME)/ulib/%, %.test-incr, $(INCR_TEST_FILES))
+test_incremental: $(patsubst $(FSTAR_ROOT)/ulib/%, %.test-incr, $(INCR_TEST_FILES))
 
-%.test-incr: $(FSTAR_HOME)/ulib/%
+%.test-incr: $(FSTAR_ROOT)/ulib/%
 	$(call msg, "IDE_INCR", $<)
-	$(Q)python3 test-incremental.py $(FSTAR_HOME)/bin/fstar.exe $< $(if $(V),,>/dev/null)
+	$(Q)python3 test-incremental.py $(FSTAR_EXE) $< $(if $(V),,>/dev/null)
 	@touch $@
 
-clean: $(addsuffix .clean, $(ALL_TEST_DIRS))
-
 %.all: %
 	+$(MAKE) -C $^ all
 
diff --git a/tests/ide/Makefile.common b/tests/ide/Makefile.common
index cf0e1e46e12..394aed34d82 100644
--- a/tests/ide/Makefile.common
+++ b/tests/ide/Makefile.common
@@ -1,13 +1,16 @@
-.PHONY: .FORCE rebuild-all check-all accept-all
+.PHONY: .FORCE rebuild-all check-all
 .SUFFIXES:
 
 ALL := $(wildcard *.in)
 
 DISABLED=FailRange.in
 
+# Disable hints, or we get warnings
+HINTS_ENABLED := 
+
 IN=$(filter-out $(DISABLED), $(ALL))
 
-all: check
+all: $(if $(ACCEPT),accept,check)
 
 # Rebuild all .out files
 BUILD_TARGETS := $(IN:.in=.out)
@@ -38,13 +41,9 @@ touch:
 
 %.in: .FORCE
 
-FSTAR_HOME = ../../..
-include $(FSTAR_HOME)/ulib/gmake/z3.mk
-include $(FSTAR_HOME)/.common.mk
-
-ifdef Z3
-SMT=--smt $(Z3)
-endif
+FSTAR_ROOT ?= ../../..
+include $(FSTAR_ROOT)/mk/test.mk
+.DEFAULT_GOAL := all
 
 JSON_CLEANUP:=python ../cleanup.py
 
diff --git a/tests/ide/emacs/FStarMode_GH73.out.expected b/tests/ide/emacs/FStarMode_GH73.out.expected
index 870e96a0347..ee934ccefff 100644
--- a/tests/ide/emacs/FStarMode_GH73.out.expected
+++ b/tests/ide/emacs/FStarMode_GH73.out.expected
@@ -1,5 +1,5 @@
 {"kind": "protocol-info", "rest": "[...]"}
-{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "- Pattern uses these theory symbols or terms that should not be in an SMT\n  pattern:\n    Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [435, 8], "end": [435, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
+{"kind": "response", "query-id": "1", "response": [], "status": "success"}
 {"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": [], "status": "success"}
diff --git a/tests/ide/emacs/Makefile b/tests/ide/emacs/Makefile
index 1c65d9d29bc..0b66e0ac367 100644
--- a/tests/ide/emacs/Makefile
+++ b/tests/ide/emacs/Makefile
@@ -1,26 +1,27 @@
 include ../Makefile.common
 
-FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --ide --warn_error -282 --ext fstar:no_absolute_paths
+.DELETE_ON_ERROR:
+
+OTHERFLAGS += --warn_error -282 --ext fstar:no_absolute_paths
 
 # Feed .in to F* and record output as .out.  Output is passed through cleanup.py
 # to ensure that the output is deterministic by pretty-printing JSON messages
 # (otherwise the order of fields in JSON dictionaries might vary across runs)
-# We turn off the .checked file cache so we don't get any races in CI
-# because we don't track dependency information.
-%.out: %.in $(FSTAR_HOME)/bin/fstar.exe
+%.out: %.in
 	$(call msg, "OUT_IDE", $<)
 	$(Q)$(eval FST := $(firstword $(subst ., ,$<)))
-	$(Q)$(FSTAR) --cache_off "$(realpath ${FST}.fst)" < "$<" | $(JSON_CLEANUP) "$@"
+	$(Q)$(FSTAR) --ide --silent "$(realpath ${FST}.fst)" < "$<" | $(JSON_CLEANUP) "$@"
 
 # The Harness.* tests for the push-partial-checked-file request require Harness.fst.checked
-Harness.%.out: Harness.%.in $(FSTAR_HOME)/bin/fstar.exe Harness.fst.checked
+Harness.%.out: Harness.%.in $(CACHE_DIR)/Harness.fst.checked
 	$(call msg, "OUT_IDE", $<)
 	$(Q)$(eval FST := $(firstword $(subst ., ,$<)))
-	$(Q)$(FSTAR) "$(realpath ${FST}.fst)" < "$<" | $(JSON_CLEANUP) "$@"
+	$(Q)$(FSTAR) --ide "$(realpath ${FST}.fst)" < "$<" | $(JSON_CLEANUP) "$@"
 
+# Only here for Harness.fst.checked
 %.checked: %
 	$(call msg, "CHECK", $<)
-	$(Q)$(FSTAR_HOME)/bin/fstar.exe $(SMT) --cache_checked_modules --silent $<
+	$(Q)$(FSTAR) --cache_checked_modules --silent $<
 
 .depend:
 	$(call msg, "DEPEND")
diff --git a/tests/ide/emacs/Search.cons-snoc.out.expected b/tests/ide/emacs/Search.cons-snoc.out.expected
index e8b32e0bb84..553227ca0b5 100644
--- a/tests/ide/emacs/Search.cons-snoc.out.expected
+++ b/tests/ide/emacs/Search.cons-snoc.out.expected
@@ -1,4 +1,3 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": [], "status": "success"}
-{"contents": "* Error 147 at FStar.Seq.Properties.fsti(760,0-762,62):\n  - Effect template FStar.Pervasives.STATE_h should be applied to arguments for its binders ((heap: Type)) before it can be used at an effect position\n  - See also <input>(1,0-1,0)\n\n", "kind": "message", "level": "error", "query-id": "2"}
-{"contents": "1 error was reported (see above)\n", "kind": "message", "level": "error", "query-id": "2"}
+{"contents": "* Error 147 at <input>(1,0-1,0):\n  - Effect template FStar.Pervasives.STATE_h should be applied to arguments for its binders ((heap: Type)) before it can be used at an effect position\n\n", "kind": "message", "level": "error", "query-id": "2"}
diff --git a/tests/ide/emacs/Tutorial.push.out.expected b/tests/ide/emacs/Tutorial.push.out.expected
index 91c41cd2478..ea080bf09d2 100644
--- a/tests/ide/emacs/Tutorial.push.out.expected
+++ b/tests/ide/emacs/Tutorial.push.out.expected
@@ -1,5 +1,5 @@
 {"kind": "protocol-info", "rest": "[...]"}
-{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "- Pattern uses these theory symbols or terms that should not be in an SMT\n  pattern:\n    Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [435, 8], "end": [435, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
+{"kind": "response", "query-id": "1", "response": [], "status": "success"}
 {"kind": "response", "query-id": "2", "response": [], "status": "success"}
 {"kind": "response", "query-id": "3", "response": [], "status": "success"}
 {"kind": "response", "query-id": "4", "response": [], "status": "success"}
diff --git a/tests/ide/lsp/Makefile b/tests/ide/lsp/Makefile
index 019b4c53a50..79626a37e24 100644
--- a/tests/ide/lsp/Makefile
+++ b/tests/ide/lsp/Makefile
@@ -1,12 +1,10 @@
 include ../Makefile.common
 
-FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --lsp --warn_error -282
+OTHERFLAGS += --lsp --warn_error -282
 
 # Feed .in to F* and record output as .out.  Output is passed through cleanup.py
 # to ensure that the output is deterministic by pretty-printing JSON messages
 # (otherwise the order of fields in JSON dictionaries might vary across runs)
-# We turn off the .checked file cache so we don't get any races in CI
-%.out: %.in $(FSTAR_HOME)/bin/fstar.exe
+%.out: %.in
 	$(call msg, "OUT_LSP", $<)
 	$(Q)$(FSTAR) < "$<" 2>&1 | $(JSON_CLEANUP) "$@"
-
diff --git a/tests/incl/Makefile b/tests/incl/Makefile
index 9b5000f305a..64650b053ec 100644
--- a/tests/incl/Makefile
+++ b/tests/incl/Makefile
@@ -1,9 +1,5 @@
 # Test the 'include' functionality
 
-FSTAR_HOME=../..
-include $(FSTAR_HOME)/ulib/gmake/fstar.mk
-include $(FSTAR_HOME)/.common.mk
-
 # Do not warn about missing checked files in these tests.
 OTHERFLAGS += --warn_error -241
 
diff --git a/tests/incl/Makefile.sub b/tests/incl/Makefile.sub
index 91e5ba62ad0..f46e0682ace 100644
--- a/tests/incl/Makefile.sub
+++ b/tests/incl/Makefile.sub
@@ -2,9 +2,9 @@
 # or 'neg' rule is called depends on the parent Makefile, which decides
 # from the name of the subdirectory.
 
-FSTAR_HOME=../../..
-include $(FSTAR_HOME)/ulib/gmake/fstar.mk
-include $(FSTAR_HOME)/.common.mk
+FSTAR_ROOT?=../../..
+NODEPEND=1
+include $(FSTAR_ROOT)/mk/test.mk
 
 # Do not warn about missing checked files in these tests.
 OTHERFLAGS += --warn_error -241
diff --git a/tests/machine_integers/.gitignore b/tests/machine_integers/.gitignore
index 1a8f3a84fdd..eed7623f257 100644
--- a/tests/machine_integers/.gitignore
+++ b/tests/machine_integers/.gitignore
@@ -1,2 +1,3 @@
 out/
 *.out
+BigList.memcheck
diff --git a/tests/machine_integers/Makefile b/tests/machine_integers/Makefile
index e408ed4ba87..cee737e8800 100644
--- a/tests/machine_integers/Makefile
+++ b/tests/machine_integers/Makefile
@@ -1,23 +1,20 @@
+FSTAR_ROOT ?= ../..
+FSTAR_FILES = $(wildcard Test*.fst)
+include $(FSTAR_ROOT)/mk/test.mk
+
 .PHONY: %.run clean
 .PRECIOUS: %.exe %.out
 
-FSTAR_HOME=../..
-
-include $(FSTAR_HOME)/examples/Makefile.include
-include $(FSTAR_HOME)/ulib/ml/Makefile.include
-
-MODULES=$(wildcard Test*.fst)
+all: $(patsubst %.fst,%.run,$(FSTAR_FILES)) BigList.memcheck
 
-all: $(patsubst %.fst,%.run,$(MODULES)) out/BigList.memcheck
+accept: $(patsubst %.fst,%.run-accept,$(FSTAR_FILES))
 
-accept: $(patsubst %.fst,%.run-accept,$(MODULES))
-
-%.exe: %.fst | out
+%.exe: %.fst
 	$(call msg, "BUILD", $(notdir $@))
 	$(eval B := $(patsubst %.exe,%,$@))
-	$(Q)$(FSTAR) $(SIL) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml --extract '${B}' '${B}.fst'
+	$(Q)$(FSTAR) --odir out --codegen OCaml --extract '${B}' '${B}.fst'
 	$(Q)/bin/echo -e '\n\nlet _ = main ()\n' >> out/${B}.ml
-	$(Q)$(OCAMLOPT) out/${B}.ml -o $@
+	$(Q)$(OCAMLOPT) -package fstar.lib -linkpkg out/${B}.ml -o $@
 
 %.out: %.exe
 	$(call msg, "OUTPUT", $(notdir $@))
@@ -29,16 +26,9 @@ accept: $(patsubst %.fst,%.run-accept,$(MODULES))
 %.run-accept: %.out
 	cp $< $<.expected
 
-out:
-	mkdir -p out
-
 # Test that this file does not use much memory (currently 580MB),
 # we give it 1.5GB
-out/BigList.memcheck: BigList.fst
+BigList.memcheck: BigList.fst
 	$(call msg, "MEMCHECK", $<)
-	$(Q)( ulimit -v 1500000 && $(FSTAR) $(SIL) BigList.fst )
-	$(Q)touch $@
-
-clean:
-	rm -rf out
-	rm -f *.exe
+	( ulimit -v 1500000 && $(FSTAR) BigList.fst )
+	touch $@
diff --git a/tests/micro-benchmarks/Makefile b/tests/micro-benchmarks/Makefile
index df5f4c4a765..dca3a971036 100644
--- a/tests/micro-benchmarks/Makefile
+++ b/tests/micro-benchmarks/Makefile
@@ -1,32 +1,25 @@
-FSTAR_HOME=../..
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
+
 OTHERFLAGS+=--warn_error +240
-FSTAR_FILES = $(wildcard *.fst)
 
-all: verify-all ns-resolution
+all: verify-all \
+	ns-resolution \
+	Erasable.ml-cmp \
+	InlineForExtractionNormRequest.ml-cmp \
+	MachineIntegerConstants.ml-cmp \
+	ExtractMutRecTypesAndTerms.ml-cmp
 
 ns-resolution:
-	+$(MAKE) -C ns_resolution
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES))) \
-            Erasable.ml-cmp \
-	    InlineForExtractionNormRequest.ml-cmp \
-	    MachineIntegerConstants.ml-cmp \
-	    ExtractMutRecTypesAndTerms.ml-cmp
+	+$(MAKE) -C ns_resolution all
 
 $(CACHE_DIR)/MustEraseForExtraction.fst.checked: OTHERFLAGS += --warn_error @318
 
 %.ml: %.fst
-	$(FSTAR) $(OTHERFLAGS) --codegen OCaml --extract $(subst .ml,, $@) $^
+	$(FSTAR) $(OTHERFLAGS) --codegen OCaml --odir . --extract $(subst .ml,, $@) $^
 
 %.ml-cmp: %.ml %.ml.expected
 	diff -u --strip-trailing-cr $<.expected $<
 	touch $@
 
-clean:
-	rm -f .depend
-	rm -rf _cache
-	rm -rf _output
-
 .PRECIOUS: %.ml
diff --git a/tests/micro-benchmarks/ns_resolution/Makefile b/tests/micro-benchmarks/ns_resolution/Makefile
index e768c871b5b..0f60780cf89 100644
--- a/tests/micro-benchmarks/ns_resolution/Makefile
+++ b/tests/micro-benchmarks/ns_resolution/Makefile
@@ -1,14 +1,3 @@
-FSTAR_HOME=../../..
-
-FSTAR_FILES=$(wildcard *.fst)
-
+FSTAR_ROOT ?= ../../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	rm -f .depend
-	rm -rf _cache
-	rm -rf _output
diff --git a/tests/prettyprinting/Makefile b/tests/prettyprinting/Makefile
index beddbae8d28..b3bb87dd426 100644
--- a/tests/prettyprinting/Makefile
+++ b/tests/prettyprinting/Makefile
@@ -1,12 +1,12 @@
-FSTAR_HOME = ../..
-FSTAR=$(FSTAR_HOME)/bin/fstar.exe
-EXCLUDED_FILES=
-include $(FSTAR_HOME)/.common.mk
+FSTAR_ROOT ?= ../..
+NODEPEND=1
+include $(FSTAR_ROOT)/mk/test.mk
 
-BASES=$(filter-out $(EXCLUDED_FILES), $(wildcard *.fst))
+EXCLUDED_FILES=
+FSTAR_FILES=$(filter-out $(EXCLUDED_FILES), $(wildcard *.fst))
 
-TESTS=$(patsubst %.fst, .%.test.print, $(BASES))
-TESTS_IN_PLACE=$(patsubst %.fst, .%.test.inplace, $(BASES))
+TESTS=$(patsubst %.fst, .%.test.print, $(FSTAR_FILES))
+TESTS_IN_PLACE=$(patsubst %.fst, .%.test.inplace, $(FSTAR_FILES))
 
 # GM: Do we really want to test the --print_in_place feature for every
 # base file? It seems unlikely this will ever regress. But it doesn't
@@ -21,13 +21,12 @@ printed:
 
 printed/%.fst: %.fst | printed
 	$(call msg, "PPRINT", $(basename $(notdir $@)))
-	$(Q)$(FSTAR) $(SIL) --print $< > $@
+	$(Q)$(FSTAR) --print $< > $@
 
 inplace/%.fst: %.fst | inplace
-	$(call msg, "PPRINT", $(basename $(notdir $@)))
+	$(call msg, "PPRINT INPLACE", $(basename $(notdir $@)))
 	$(Q)cp $< $@
-	$(Q)$(FSTAR) $(SIL) --print_in_place $@
-
+	$(Q)$(FSTAR) --print_in_place $@
 
 # Note how these two rules make an empty touch file for 
 # the target so we don't keep running diff uselessly.
@@ -42,20 +41,14 @@ inplace/%.fst: %.fst | inplace
 %.fst.accept: printed/%.fst
 	cp $< $(patsubst printed/%.fst,%.fst.expected, $<)
 
-accept: $(patsubst %, %.accept, $(BASES))
-
-clean:
-	$(call msg, "CLEAN")
-	$(Q)rm -rf printed inplace
-	$(Q)rm -f .*.test.print
-	$(Q)rm -f .*.test.inplace
+accept: $(patsubst %, %.accept, $(FSTAR_FILES))
 
 .PHONY: accept clean
 
 # Keep the printed fst files so we can look at them easily
 # Sigh, .SECONDARY does not take patterns
-.SECONDARY: $(patsubst %,printed/%,$(BASES))
-.SECONDARY: $(patsubst %,inplace/%,$(BASES))
+.SECONDARY: $(patsubst %,printed/%,$(FSTAR_FILES))
+.SECONDARY: $(patsubst %,inplace/%,$(FSTAR_FILES))
 
 # This is so that, e.g., if the --print call fails then make will delete
 # the printed file, which is anyway created by bash (and will likely
diff --git a/tests/projectors/Makefile b/tests/projectors/Makefile
index b0d903477bd..e1e94ee097f 100644
--- a/tests/projectors/Makefile
+++ b/tests/projectors/Makefile
@@ -1,15 +1,3 @@
-FSTAR_HOME=../..
-
-FSTAR_FILES=$(wildcard *.fst)
-
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	$(call msg, "CLEAN")
-	$(Q)rm -f .depend
-	$(Q)rm -rf _cache
-	$(Q)rm -rf _output
diff --git a/tests/restricted_includes/Makefile b/tests/restricted_includes/Makefile
index 763b3fc7adb..e1e94ee097f 100644
--- a/tests/restricted_includes/Makefile
+++ b/tests/restricted_includes/Makefile
@@ -1,15 +1,3 @@
-FSTAR_HOME=../..
-
-FSTAR_FILES=$(wildcard *.fst *.fsti)
-
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	$(call msg, "CLEAN")
-	$(Q)rm -f .depend
-	$(Q)rm -rf _cache
-	$(Q)rm -rf _output
diff --git a/tests/semiring/Makefile b/tests/semiring/Makefile
index de9c30fd675..7e6b0f392fb 100644
--- a/tests/semiring/Makefile
+++ b/tests/semiring/Makefile
@@ -1,35 +1,42 @@
-FSTAR_HOME?=../..
-FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 
 # This tests that the semiring tactic can be made into a plugin.
 # We should make it so in the library and just remove this, along
 # with its hacks.
 
-OCAMLOPT=OCAMLPATH="$(FSTAR_HOME)/lib" ocamlfind opt
-
 .PHONY: %.native %.interpreted
 .PRECIOUS: %.fst.checked %.ml %.cmxs
 
 all: CanonCommSemiring.interpreted CanonCommSemiring.native
 
 %.fst.checked: %.fst
+	$(call msg, "CHECK", $<)
 	$(FSTAR) --cache_checked_modules $*.fst
 
-%.ml: %.fst.checked
+# NOTE: This is overriding the default rule in test.mk.
+# If you add explicit dependencies here, it will fall back to the default rule.
+$(OUTPUT_DIR)/%.ml:
+	$(call msg, "EXTRACT", $<)
 	$(FSTAR) --codegen Plugin --extract $* $*.fst
-	cat $*.ml.fixup >> $*.ml
+	cat $*.ml.fixup >> $@
 
-%.cmxs: %.ml $(FSTAR_HOME)/bin/fstar.exe
-	$(OCAMLOPT) -shared -package fstar.lib -o $@ $*.ml
+%.cmxs: %.ml
+	$(call msg, "OCAMLOPT", $<)
+	$(OCAMLOPT) -w -8 -shared -package fstar.lib -o $@ $*.ml
 
-# REMARK: --load will compile $*.ml if $*.cmxs does not exist, but we compile it before
-%.native: %.cmxs %.fst %.Test.fst
-	$(FSTAR) --load $* $*.Test.fst
+# REMARK: --load will compile $*.ml if $*.cmxs does not exist, but we
+# compile it before and use --load_cmxs
+%.native: $(OUTPUT_DIR)/%.cmxs %.fst %.Test.fst
+	$(call msg, "CHECK NATIVE", $<)
+	$(FSTAR) --load_cmxs $* $*.Test.fst
 	@touch $@
 
 %.interpreted: %.fst.checked %.Test.fst
+	$(call msg, "CHECK INTERP", $<)
 	$(FSTAR) $*.Test.fst
 	@touch $@
 
 clean:
 	rm -f *.checked *.ml *.o *.cm[ix] *.cmxs *~
+	rm -rf $(CACHE_DIR) $(OUTPUT_DIR)
diff --git a/tests/simple_hello/Makefile b/tests/simple_hello/Makefile
index 0fae4812b8e..d4cbb66c1b3 100644
--- a/tests/simple_hello/Makefile
+++ b/tests/simple_hello/Makefile
@@ -4,7 +4,10 @@
 
 FSTAR ?= ../../bin/fstar.exe
 
-all: Hello.exe
+all: Hello.test
+
+Hello.test: Hello.exe
+	./Hello.exe | grep "Hello F\*!"
 
 %.ml: %.fst
 	$(FSTAR) --codegen OCaml $< --extract $*
diff --git a/tests/struct/Makefile b/tests/struct/Makefile
index 8891901a71d..eec602c6ffd 100644
--- a/tests/struct/Makefile
+++ b/tests/struct/Makefile
@@ -1,8 +1,8 @@
 # Test the 'struct' functionality
 
-FSTAR_HOME=../..
-include $(FSTAR_HOME)/ulib/gmake/fstar.mk
-include $(FSTAR_HOME)/.common.mk
+FSTAR_ROOT ?= ../..
+NODEPEND=1
+include $(FSTAR_ROOT)/mk/test.mk
 
 POSTESTS=$(wildcard *.pos)
 POSTESTS:=$(filter-out jsonparser.pos, $(POSTESTS))
diff --git a/tests/struct/Makefile.sub b/tests/struct/Makefile.sub
index 91e5ba62ad0..69f42b72b8a 100644
--- a/tests/struct/Makefile.sub
+++ b/tests/struct/Makefile.sub
@@ -2,17 +2,13 @@
 # or 'neg' rule is called depends on the parent Makefile, which decides
 # from the name of the subdirectory.
 
-FSTAR_HOME=../../..
-include $(FSTAR_HOME)/ulib/gmake/fstar.mk
-include $(FSTAR_HOME)/.common.mk
+FSTAR_ROOT?=../../..
+NODEPEND=1
+include $(FSTAR_ROOT)/mk/test.mk
 
 # Do not warn about missing checked files in these tests.
 OTHERFLAGS += --warn_error -241
 
-all: uall
-
-uall: $(POSTARGETS) $(NEGTARGETS)
-
 check-pos: $(wildcard *.fst)
 	$(call msg, "CHECK", $(basename $(notdir $(shell pwd))))
 	$(Q)$(FSTAR) $(SIL) Test.fst
diff --git a/tests/tactics/Makefile b/tests/tactics/Makefile
index bede3521728..e054c1b7ec2 100644
--- a/tests/tactics/Makefile
+++ b/tests/tactics/Makefile
@@ -1,22 +1,14 @@
-FSTAR_HOME=../..
-
-FSTAR_FILES=$(wildcard *.fst)
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 
 all: verify-all Hacl.Meta.Use.fst.test
 
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	$(call msg, "CLEAN")
-	$(Q)rm -f .depend
-	$(Q)rm -rf _cache
-	$(Q)rm -rf _output
+# The negative tests in this file may succeed with hints, force them off.
+$(CACHE_DIR)/Pruning.fst.checked: HINTS_ENABLED=
 
 Hacl_Meta.ml:
-	$(Q)$(FSTAR) Hacl.Meta.fst --codegen Plugin
+	$(FSTAR) Hacl.Meta.fst --codegen Plugin
 
 Hacl.Meta.Use.fst.test: Hacl.Meta.Use.fst Hacl_Meta.ml
-	$(Q)$(FSTAR) $< --load Hacl.Meta
-	@touch $@
+	$(FSTAR) $< --load Hacl.Meta
+	touch $@
diff --git a/tests/typeclasses/Makefile b/tests/typeclasses/Makefile
index b0d903477bd..e1e94ee097f 100644
--- a/tests/typeclasses/Makefile
+++ b/tests/typeclasses/Makefile
@@ -1,15 +1,3 @@
-FSTAR_HOME=../..
-
-FSTAR_FILES=$(wildcard *.fst)
-
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	$(call msg, "CLEAN")
-	$(Q)rm -f .depend
-	$(Q)rm -rf _cache
-	$(Q)rm -rf _output
diff --git a/tests/vale/Makefile b/tests/vale/Makefile
index cedc760939e..158fbc67e21 100644
--- a/tests/vale/Makefile
+++ b/tests/vale/Makefile
@@ -1,4 +1,8 @@
-FSTAR_HOME=../..
+FSTAR_ROOT ?= ../..
+FSTAR_FILES=$(wildcard *.fst)
+FSTAR_FILES:=$(filter-out X64.Poly1305.fst,$(FSTAR_FILES))
+include $(FSTAR_ROOT)/mk/test.mk
+all: verify-all
 
 OTHERFLAGS += \
 --z3cliopt smt.QI.EAGER_THRESHOLD=100 \
@@ -11,21 +15,4 @@ OTHERFLAGS += \
 --max_ifuel 1 \
 --initial_ifuel 0 \
 --warn_error -350
-
 # ^ 350: deprecated lightweight do notation
-
-FSTAR_FILES=$(wildcard *.fst)
-
-FSTAR_FILES:=$(filter-out X64.Poly1305.fst,$(FSTAR_FILES))
-
-all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	$(call msg, "CLEAN")
-	$(Q)rm -f .depend
-	$(Q)rm -rf _cache
-	$(Q)rm -rf _output