remove hints from Makefiles; use --ext context_pruning instead

book/tutorial/Makefile

@@ -32,8 +32,6 @@ include Makefile.include
 # Definition of F* flags
 # ----------------------
 
-FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
-
 # This flag controls what gets extracted to OCaml. Generally, we don't extract
 # the FStar namespace since it's already extracted and packaged as the ocamlfind
 # package fstar.lib. Here, unlike in -bundle, +Spec matches both Spec and
@@ -51,10 +49,10 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'
 # - --cache_checked_modules to rely on a pre-built ulib and krmllib
 # - --cache_dir, to avoid polluting our generated build artifacts outside o
 
-FSTAR_NO_FLAGS = $(FSTAR_EXE) $(FSTAR_HINTS) \
+FSTAR_NO_FLAGS = $(FSTAR_EXE) --ext context_pruning \
   --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
-  --cache_dir obj --hint_dir hints
+  --cache_dir obj
 
 # Initial dependency analysis
 # ---------------------------
@@ -92,9 +90,6 @@ FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS)
 
 # Creating these directories via a make rule, rather than rely on F* creating
 # them, as two calls to F* might race.
-hints:
-	mkdir $@
-
 obj:
 	mkdir $@
 
@@ -119,7 +114,7 @@ obj:
 # Note: F* will not change the mtime of a checked file if it is
 # up-to-date (checksum matches, file unchanged), but this will confuse
 # make and result in endless rebuilds. So, we touch that file.
-%.checked: | hints obj
+%.checked: | obj
 	$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
 
 # Extraction

krmllib/Makefile

@@ -22,7 +22,7 @@ UINT128_DIR = dist/uint128
 MINI_DIR = dist/minimal
 
 #332 is turning abstract keyword usage into a fatal error
-FSTAR_OPTIONS += --record_hints --use_hints --odir $(EXTRACT_DIR) \
+FSTAR_OPTIONS += --ext context_pruning --odir $(EXTRACT_DIR) \
   --warn_error @332
   # --use_extracted_interfaces
 
@@ -37,7 +37,6 @@ ifneq ($(RESOURCEMONITOR),)
 endif
 
 FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_checked_modules --cache_dir obj \
-  --hint_dir hints \
   $(addprefix --include , $(INCLUDE_PATHS)) --cmi \
   --already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'
 

test/Makefile

@@ -70,7 +70,6 @@ NEGATIVE	= false
 WEB_DIR		?= web
 CACHE_DIR	= .cache
 OUTPUT_DIR	= .output
-HINTS_DIR	= .hints
 
 ifneq ($(CRYPTO),)
   INCLUDE_CRYPTO=--include $(CRYPTO)
@@ -79,7 +78,7 @@ FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
   --cache_dir $(CACHE_DIR) --odir $(OUTPUT_DIR) \
   --include hello-system --include ../krmllib/compat --include ../krmllib/obj \
   --include ../krmllib --include ../runtime \
-  $(INCLUDE_CRYPTO) --include ../book --include ../book/notfslit --use_hints --record_hints \
+  $(INCLUDE_CRYPTO) --include ../book --include ../book/notfslit --ext context_pruning \
   --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
   --trivial_pre_for_unannotated_effectful_fns false \
   --cmi --warn_error -274
@@ -109,11 +108,8 @@ endif
 
 include .depend
 
-$(HINTS_DIR):
-	mkdir -p $@
-
-$(CACHE_DIR)/%.checked: | .depend $(HINTS_DIR)
-	$(FSTAR) $(OTHERFLAGS) --hint_file $(HINTS_DIR)/$*.hints $< && \
+$(CACHE_DIR)/%.checked: | .depend
+	$(FSTAR) $(OTHERFLAGS) $< && \
 	touch $@
 
 $(OUTPUT_DIR)/%.krml: | .depend