cleanup

Makefile

@@ -10,9 +10,10 @@ all: lib verify
 
 # Find fstar.exe
 ifdef FSTAR_HOME
-FSTAR_EXE := $(FSTAR_HOME)/bin/fstar.exe
+FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 endif
 FSTAR_EXE ?= $(shell which fstar.exe)
+
 ifeq (,$(FSTAR_EXE))
   $(error "Did not find fstar.exe in PATH and FSTAR_EXE/FSTAR_HOME unset, aborting.")
 endif

share/steel/Makefile.include

@@ -1,50 +1,35 @@
 ifeq (,$(STEEL_HOME))
 	$(error STEEL_HOME should be defined in the enclosing Makefile as the prefix directory where Steel was installed, or the root directory of its source repository)
 endif
+include $(STEEL_HOME)/mk/common.mk
+.DEFAULT_GOAL := verify
 
 ifneq (,$(FSTAR_HOME))
-  FSTAR=$(FSTAR_HOME)/bin/fstar.exe
-else
-  FSTAR=fstar.exe
+FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 endif
 
+FSTAR_EXE ?= $(shell which fstar.exe)
+
+$(call need_exe,FSTAR_EXE)
+
 # Add Steel to the OCaml (ocamlfind) search path
 ifeq ($(OS),Windows_NT)
   OCAMLPATH := $(shell cygpath -m $(STEEL_HOME)/lib);$(OCAMLPATH)
 else
   OCAMLPATH := $(STEEL_HOME)/lib:$(OCAMLPATH)
 endif
 
-# Find fstar.exe and the fstar.lib OCaml package
-ifeq (,$(FSTAR_HOME))
-  _check_fstar := $(shell which fstar.exe)
-  ifeq ($(.SHELLSTATUS),0)
-    _fstar_home := $(realpath $(dir $(_check_fstar))/..)
-    ifeq ($(OS),Windows_NT)
-      OCAMLPATH := $(shell cygpath -m $(_fstar_home)/lib);$(OCAMLPATH)
-    else
-      OCAMLPATH := $(_fstar_home)/lib:$(OCAMLPATH)
-    endif
-  endif
-else
-  ifeq ($(OS),Windows_NT)
-    OCAMLPATH := $(shell cygpath -m $(FSTAR_HOME)/lib);$(OCAMLPATH)
-  else
-    OCAMLPATH := $(FSTAR_HOME)/lib:$(OCAMLPATH)
-  endif
-endif
-export OCAMLPATH
-
 FSTAR_FILES += $(filter-out $(EXCLUDE_FILES),$(wildcard *.fst *.fsti))
 ADDITIONAL_INCLUDES ?= 
 FSTAR_OPTIONS += $(OTHERFLAGS) --cmi --cache_checked_modules --warn_error @241 --already_cached 'Prims,FStar,LowStar,Steel,C' --include $(STEEL_HOME)/lib/steel $(ADDITIONAL_INCLUDES) --load_cmxs steel
+FSTAR_OPTIONS += --include $(STEEL_HOME)/build/plugin.checked
 
 COMPAT_INDEXED_EFFECTS?=--compat_pre_typed_indexed_effects
 
 # Used only for OCaml extraction, not krml extraction
 FSTAR_ML_CODEGEN ?= OCaml
 
-MY_FSTAR=$(RUNLIM) $(FSTAR) $(SIL) $(FSTAR_OPTIONS)
+MY_FSTAR=$(RUNLIM) $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 
 %.checked:
 	$(call msg, "CHECK", $(basename $(notdir $@)))

share/steel/examples/steel/OWGCounter/Makefile

@@ -15,7 +15,7 @@ include $(STEEL_HOME)/share/steel/Makefile.include
 OUTPUT_EXE=_build/default/OWGCounterTest.exe
 
 $(OUTPUT_EXE): $(OUTPUT_DIRECTORY)/OWGCounter.ml OWGCounterTest.ml
-	dune build
+	$(FSTAR_EXE) --ocamlenv dune build
 
 counter: $(OUTPUT_EXE)
 	$<