remove hints from makefiles and project files

FStarLang · Jan 15, 2025 · d35a5e4 · d35a5e4
1 parent be9d298
commit d35a5e4
Show file tree

Hide file tree

Showing 13 changed files with 20 additions and 32 deletions.
diff --git a/examples/algorithms/BinarySearch/BinarySearch.fsproj b/examples/algorithms/BinarySearch/BinarySearch.fsproj
@@ -5,7 +5,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project . -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>

diff --git a/examples/algorithms/Huffman/Huffman.fsproj b/examples/algorithms/Huffman/Huffman.fsproj
@@ -5,7 +5,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project . -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>

diff --git a/examples/data_structures/Lens/Lens.fsproj b/examples/data_structures/Lens/Lens.fsproj
@@ -5,7 +5,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project . -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>

diff --git a/examples/dependencies/Makefile b/examples/dependencies/Makefile
@@ -18,13 +18,10 @@ endif
 OUT_DIR   = out
 CACHE_DIR = cache
 ROOTS     = Test.fst
-HINT_DIR  = hints
 
 FSTAR_FLAGS = $(OTHERFLAGS) --cmi --odir $(OUT_DIR) --cache_dir $(CACHE_DIR) \
-  --cache_checked_modules --already_cached 'Prims FStar' --z3version 4.13.3
-
-# Run with ENABLE_HINTS= to disable
-ENABLE_HINTS ?= --use_hints
+  --cache_checked_modules --already_cached 'Prims FStar' --z3version 4.13.3 \
+  --ext context_pruning
 
 FSTAR = $(FSTAR_EXE) $(FSTAR_FLAGS)
 
@@ -44,7 +41,7 @@ all:
 include .depend
 
 $(CACHE_DIR)/%.checked:
-	$(FSTAR) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $<).hints && \
+	$(FSTAR) $< && \
 	touch $@
 
 # 2. Compile all .ml files to .cmx and link them to get an executable

diff --git a/examples/hello/Hello/Hello.fsproj b/examples/hello/Hello/Hello.fsproj
@@ -8,7 +8,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>

diff --git a/examples/hello/TestFSharp/TestFSharp.fsproj b/examples/hello/TestFSharp/TestFSharp.fsproj
@@ -6,7 +6,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>

diff --git a/examples/old/tls-record-layer/Makefile b/examples/old/tls-record-layer/Makefile
@@ -177,13 +177,13 @@ chacha-aead-test: chacha-aead-compile
 	./test_chacha_aead.exe
 
 bignum-ver:
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part4.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
-	$(FSTAR) --use_hints --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part4.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
+	$(FSTAR) --ext context_pruning --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
 
 KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KRML_HOME)/krmllib $(KRML_HOME)/test)
 ifeq ($(OS),Windows_NT)

diff --git a/examples/old/tls-record-layer/crypto/Makefile b/examples/old/tls-record-layer/crypto/Makefile
@@ -2,9 +2,7 @@ FSTAR_HOME=../../..
 
 FSTAR?=$(FSTAR_HOME)/bin/fstar.exe
 
-HINTS_ENABLED?=--use_hints
-
-OPTIONS=--fstar_home $(FSTAR_HOME) --max_fuel 4 --initial_fuel 0 --max_ifuel 2 --initial_ifuel 0 --z3rlimit 20  $(HINTS_ENABLED) $(OTHERFLAGS)
+OPTIONS=--fstar_home $(FSTAR_HOME) --max_fuel 4 --initial_fuel 0 --max_ifuel 2 --initial_ifuel 0 --z3rlimit 20 --ext context_pruning $(OTHERFLAGS)
 
 FSTAR_INCLUDE_PATHS=--include $(FSTAR_HOME)/ulib/hyperstack --include hacl
 

diff --git a/examples/sample_project/Makefile b/examples/sample_project/Makefile
@@ -14,7 +14,7 @@ TOP_LEVEL_FILE=ml/main.ml
 OUTPUT_DIRECTORY=_output
 
 ################################################################################
-FSTAR=fstar.exe --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --use_hints $(OTHERFLAGS)
+FSTAR=fstar.exe --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --ext context_pruning $(OTHERFLAGS)
 ML_FILES=$(addprefix $(OUTPUT_DIRECTORY)/,$(addsuffix .ml,$(subst .,_, $(subst .fst,,$(FSTAR_FILES)))))
 OCAML_EXE=$(PROGRAM).ocaml.exe
 KRML_EXE=$(PROGRAM).exe

diff --git a/mk/lib.mk b/mk/lib.mk
@@ -1,6 +1,3 @@
-FSTAR_OPTIONS += --use_hints
-FSTAR_OPTIONS += --hint_dir $(SRC)/.hints
-FSTAR_OPTIONS += --warn_error -333 # Do not warn about missing hints
 FSTAR_OPTIONS += --ext context_pruning
 FSTAR_OPTIONS += --z3version 4.13.3
 

diff --git a/mk/test.mk b/mk/test.mk
@@ -27,8 +27,6 @@ FSTAR_EXE ?= $(FSTAR_ROOT)/out/bin/fstar.exe
 FSTAR_EXE := $(abspath $(FSTAR_EXE))
 export FSTAR_EXE
 
-HINTS_ENABLED?=--use_hints
-
 # This warning is really useless.
 OTHERFLAGS += --warn_error -321
 OTHERFLAGS += --ext context_pruning
@@ -50,7 +48,7 @@ FSTAR = $(FSTAR_EXE) $(SIL) 				\
 	--odir $(OUTPUT_DIR)				\
 	--cache_dir $(CACHE_DIR)			\
 	--already_cached Prims,FStar,LowStar		\
-	 $(OTHERFLAGS) $(MAYBE_ADMIT) $(HINTS_ENABLED)
+	 $(OTHERFLAGS) $(MAYBE_ADMIT)
 
 ifneq ($(MAKECMDGOALS),clean)
 ifeq ($(NODEPEND),) # Set NODEPEND=1 to not dependency analysis

diff --git a/stage0/ulib/Makefile.verify b/stage0/ulib/Makefile.verify
diff --git a/stage0/ulib/gmake/fstar.mk b/stage0/ulib/gmake/fstar.mk