Merge pull request #3377 from mtzguido/ci_hints

Tidy up hint usage

Author: mtzguido

Diff for: .docker/build/build_funs.sh

@@ -174,5 +174,4 @@ function build_fstar() {
 # Some environment variables we want
 export V=1 # Make sure to get verbose output from makefiles
 export OCAMLRUNPARAM=b
-export OTHERFLAGS="--use_hints"
 export MAKEFLAGS="$MAKEFLAGS -Otarget" # Group make output by target

Diff for: Makefile

@@ -157,8 +157,8 @@ output-bug-reports:
 # snapshot, nor run the build-standalone script.
 .PHONY: ci
 ci:
-	+$(Q)OTHERFLAGS="${OTHERFLAGS} --use_hints" FSTAR_HOME=$(CURDIR) $(MAKE) ci-pre
-	+$(Q)OTHERFLAGS="${OTHERFLAGS} --use_hints" FSTAR_HOME=$(CURDIR) $(MAKE) ci-post
+	+$(Q)FSTAR_HOME=$(CURDIR) $(MAKE) ci-pre
+	+$(Q)FSTAR_HOME=$(CURDIR) $(MAKE) ci-post
 
 # This rule runs a CI job in a local container, exactly like is done for
 # CI.

Diff for: examples/Makefile.common

@@ -45,6 +45,10 @@ CACHE_DIR ?= _cache
 ADMIT ?=
 MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
 
+# Set HINTS= (empty) to not use hints
+HINTS ?= 1
+MAYBE_HINTS = $(if $(HINTS),--use_hints)
+
 ################################################################################
 # YOU SHOULDN'T NEED TO TOUCH THE REST
 ################################################################################
@@ -54,7 +58,7 @@ VERBOSE_FSTAR=$(BENCHMARK_PRE) $(FSTAR)                     \
 		  --odir $(OUTPUT_DIRECTORY)                \
 		  --cache_dir $(CACHE_DIR)                  \
 		  $(addprefix --include , $(INCLUDE_PATHS)) \
-		  $(OTHERFLAGS) $(MAYBE_ADMIT)
+		  $(OTHERFLAGS) $(MAYBE_ADMIT) $(MAYBE_HINTS)
 
 # As above, but perhaps with --silent, and perhaps with a prefix (usually for monitoring)
 MY_FSTAR=$(RUNLIM) $(VERBOSE_FSTAR) $(SIL)