removing uses of --verify_module in our makefiles ***NO_CI***

.completion/fish/fstar.exe.fish

@@ -13,8 +13,6 @@ complete -c fstar.exe -l detail_hint_replay --description "Emit a detailed repor
 complete -c fstar.exe -l doc --description "Extract Markdown documentation files for the input modules, as well as an index. Output is written to --odir directory."
 complete -c fstar.exe -l dump_module --description "[module name]"
 complete -c fstar.exe -l eager_inference --description "Solve all type-inference constraints eagerly; more efficient but at the cost of generality"
-complete -c fstar.exe -l explicit_deps --description "Do not find dependencies automatically, the user provides them on the command-line"
-complete -c fstar.exe -l extract_all --description "Discover the complete dependency graph and do not stop at interface boundaries"
 complete -c fstar.exe -l extract_module -r --description "Only extract the specified modules (instead of the possibly-partial dependency graph)"
 complete -c fstar.exe -l extract_namespace -r --description "Only extract modules in the specified namespace"
 complete -c fstar.exe -l fstar_home -r --description "Set the FSTAR_HOME variable to [dir]"
@@ -68,8 +66,6 @@ complete -c fstar.exe -l use_eq_at_higher_order --description "Use equality cons
 complete -c fstar.exe -l use_hints --description "Use a previously recorded hints database for proof replay"
 complete -c fstar.exe -l no_tactics --description "Do not run the tactic engine before discharging a VC"
 complete -c fstar.exe -l using_facts_from -r --description "Implies --z3refresh; prunes the context to include facts from the given namespace of fact id (multiple uses of this option will prune the context to include those facts that match any of the provided namespaces / fact ids"
-complete -c fstar.exe -l verify_all --description "With automatic dependencies, verify all the dependencies, not just the files passed on the command-line."
-complete -c fstar.exe -l verify_module -r --description "Name of the module to verify"
 complete -c fstar.exe -l __temp_no_proj -r --description "Don't generate projectors for this module"
 complete -c fstar.exe -l version --description "Display version number"
 complete -c fstar.exe -l warn_default_effects --description "Warn when (a -> b) is desugared to (a -> Tot b)"

doc/tutorial/code/exercises/Makefile

@@ -63,4 +63,3 @@ Ex01a-ocaml: out Ex01a.fst
 # %.fst-in: 
 # 	@echo $(OPTIONS) \
 # 	--include $(FSTAR_HOME)/ulib/hyperstack \
-# 	--verify_module $(basename $(notdir $@))

doc/tutorial/code/solutions/Makefile

@@ -70,4 +70,3 @@ Ex01a-ocaml: out Ex01a.fst
 # %.fst-in:
 # 	@echo $(OPTIONS) \
 #  	--include $(FSTAR_HOME)/ulib/hyperstack \
-#  	--verify_module $(basename $(notdir $@))

examples/Makefile.include

@@ -13,7 +13,7 @@ MSBUILD = xbuild
 endif
 
 %.uver: %.fst
-	$(FSTAR) --verify_module $* $^
+	$(FSTAR) $^
 
 %.fail-uver: %.fst
-	(! $(FSTAR) --verify_module $* $^ >/dev/null 2>&1) || (echo "NEGATIVE TEST FAILED ($@)!" ; false)
+	(! $(FSTAR) $^ >/dev/null 2>&1) || (echo "NEGATIVE TEST FAILED ($@)!" ; false)

examples/algorithms/Makefile

@@ -7,7 +7,7 @@ all: uall
 uall: BinarySearch.uver IntSort.uver InsertionSort.uver MergeSort.uver QuickSort.List.uver QuickSort.Seq.uver GC.uver Unification.uver Huffman.uver #downgrade QuickSort.Array.uver //TODO
 
 downgrade: QuickSort.Array.fst downgrade.fst
-	$(FSTAR) --include $(FSTAR_HOME)/ulib/reclaimable downgrade.fst --verify_module Downgrade
+	$(FSTAR) --include $(FSTAR_HOME)/ulib/reclaimable downgrade.fst
 
 include $(FSTAR_HOME)/ulib/ml/Makefile.include
 

examples/low-level/crypto/Makefile

@@ -89,22 +89,19 @@ all-lax: $(addsuffix .fst-lax, $(LAX)) $(addsuffix .fst-lax, $(VERIFY))
 %.fst-in: 
 	@echo $(OPTIONS) \
 	$(FSTAR_INCLUDE_PATHS) \
-	--__temp_no_proj Crypto.Symmetric.MAC \
-	--verify_module $(basename $(notdir $@))
+	--__temp_no_proj Crypto.Symmetric.MAC
 
 # Verifying one file at a time
 %.fst-ver:
 	$(FSTAR) $(OPTIONS) \
 	$(FSTAR_INCLUDE_PATHS) \
 	--__temp_no_proj Crypto.Symmetric.MAC \
-	--verify_module $(basename $(notdir $@)) \
 	$(basename $@).fst
 
 # Lax verifying one file at a time
 %.fst-lax:
 	$(FSTAR) $(OPTIONS) \
 	$(FSTAR_INCLUDE_PATHS) --lax \
-	--verify_module $(basename $(notdir $@)) \
 	$(basename $@).fst
 
 AEAD_FILES=$(addsuffix .fst, $(VERIFY))
@@ -115,4 +112,3 @@ aead-wc:
 
 all-assumes: $(addsuffix .fst, $(VERIFY) $(LAX))
 	grep "\(assume\)\|\(admit\)\|\(lax\)" $^
-

examples/paradoxes/Makefile

@@ -13,5 +13,4 @@ propImpredicative:
 
 %.fst-in:
 	@echo $(OPTIONS) \
-	--__temp_no_proj InjectiveTypeFormers \
-	--verify_module $(basename $(notdir $@))
+	--__temp_no_proj InjectiveTypeFormers

examples/preorders/Makefile

@@ -8,7 +8,7 @@ uall: $(patsubst %.fst,%.uver,$(wildcard *.fst))
 # special casing this file since there is a weird interaction
 # between --verify_module and --use_hints
 MRefHeap.uver : MRefHeap.fst
-	$(FSTAR) --record_hints --verify_module MRefHeap $^
+	$(FSTAR) --record_hints $^
 
 
 # Targets to get F* arguments in interactive mode

examples/tactics/Makefile

@@ -44,7 +44,7 @@ all:	Apply.uver		\
 	# launch			\
 
 launch: Launch.fst
-	$(FSTAR) --unsafe_tactic_exec --verify_module Launch $^
+	$(FSTAR) --unsafe_tactic_exec $^
 
 neg:
 	$(MAKE) -C neg

src/syntax/FStar.Syntax.Util.fs

@@ -618,7 +618,7 @@ let field_projector_prefix = Ident.reserved_prefix ^ "proj__"
    examples/preorders/MRefHeap.fst (even after regenerating hints), it
    will produce the following error:
 
-   fstar.exe  --use_hints --verify_module MRefHeap MRefHeap.fst
+   fstar.exe  --use_hints MRefHeap.fst
    ./MRefHeap.fst(55,51-58,27): (Error) Unknown assertion failed
    Verified module: MRefHeap (2150 milliseconds)
    1 error was reported (see above)