Merge pull request #3620 from FStarLang/_guido_windows

Fixes to make the windows binary build work

Author: mtzguido

examples/dependencies/Makefile

@@ -6,6 +6,11 @@ FSTAR_EXE ?= $(shell which fstar.exe)
 
 V != $(FSTAR_EXE) --version
 
+HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
+# NB: This is overriden (to empty) when testing the binary package
+# so we skip the build test. (Variables given in the command line, not
+# the environment, override those defined in the script.)
+
 ifeq ($(V),)
 $(error "fstar.exe --version failed... place a valid F* in your PATH or set FSTAR_EXE")
 endif
@@ -23,7 +28,7 @@ ENABLE_HINTS ?= --use_hints
 
 FSTAR = $(FSTAR_EXE) $(FSTAR_FLAGS)
 
-.PHONY: all test clean
+.PHONY: all test clean run
 
 all:
 	rm -f .depend && $(MAKE) .depend # Always re-generate dependencies
@@ -55,7 +60,14 @@ $(OUT_DIR)/%.ml:
 $(OUT_DIR)/test.exe: $(subst .ml,.cmx,$(ALL_ML_FILES)) | $(OUT_DIR)
 	$(FSTAR_EXE) --ocamlopt -I $(OUT_DIR) -o $(OUT_DIR)/test.exe $(subst .ml,.cmx,$(ALL_ML_FILES))
 
-test: $(OUT_DIR)/test.exe
+# If we don't have OCaml, just extract the ML files.
+ifneq (,$(HAS_OCAML))
+test: run
+else
+test: $(ALL_ML_FILES)
+endif
+
+run: $(OUT_DIR)/test.exe
 	$(OUT_DIR)/test.exe
 
 clean:

mk/test.mk

@@ -155,6 +155,15 @@ ifeq ($(NOVERIFY),)
 all: __verify
 endif
 
+HAS_OCAML ?= 1
+# We assume we have ocaml, unless HAS_OCAML= was given as an argument
+# to make (this is done by binary package CI). If we don't have ocaml,
+# we don't try to build or run programs.
+ifeq (,$(HAS_OCAML))
+NORUN := 1
+NOBUILD := 1
+endif
+
 # clean
 SUBDIRS_CLEAN += $(SUBDIRS)
 clean: $(addsuffix .__clean, $(SUBDIRS_CLEAN))

ocaml/fstar-lib/FStarC_Compiler_Util.ml

@@ -1172,3 +1172,8 @@ let array_index (l:'a FStar_ImmutableArray_Base.t) (i:Z.t) = FStar_ImmutableArra
 
 let putenv k v = Unix.putenv k v
 let execvp c args = Unix.execvp c (Array.of_list args)
+
+let exn_is_enoent (e:exn) : bool =
+  match e with
+  | Unix.Unix_error (Unix.ENOENT, _, _) -> true
+  | _ -> false

ocaml/fstar-lib/generated/FStarC_OCaml.ml

@@ -400,3 +400,5 @@ val array_index (s:FStar.ImmutableArray.Base.t 'a) (i:FStarC.BigInt.t) : 'a
 
 val putenv : string -> string -> unit
 val execvp : string -> list string -> unit // will return only on error
+
+val exn_is_enoent (e:exn) : bool

ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml

@@ -30,17 +30,16 @@ let shellescape (s:string) : string =
 
 let new_ocamlpath () : string =
   let ocamldir = Find.locate_ocaml () in
+  let sep = match Platform.system with
+    | Platform.Windows -> ";"
+    | Platform.Posix -> ":"
+  in
   let old_ocamlpath = Util.dflt "" (Util.expand_environment_variable "OCAMLPATH") in
-  let new_ocamlpath = ocamldir ^ ":" ^ old_ocamlpath in
+  let new_ocamlpath = ocamldir ^ sep ^ old_ocamlpath in
   new_ocamlpath
 
 let exec_in_ocamlenv #a (cmd : string) (args : list string) : a =
   let new_ocamlpath = new_ocamlpath () in
-  if Platform.system = Platform.Windows then (
-    Errors.raise_error0 Errors.Fatal_OptionsNotCompatible [
-      Errors.text "--ocamlenv is not supported on Windows (yet?)"
-    ]
-  );
   (* Update OCAMLPATH and run (exec) the command *)
   Util.putenv "OCAMLPATH" new_ocamlpath;
   Util.execvp cmd (cmd :: args);

src/basic/FStarC.Compiler.Util.fsti

@@ -70,8 +70,11 @@ let z3_exe : unit -> string =
     find_or (Options.z3_version()) (fun version ->
       let path =
         let z3_v = Platform.exe ("z3-" ^ version) in
+        let local_z3 = Platform.exe (FStarC.Find.fstar_bin_directory ^ "/" ^ "z3-fstar-" ^ version) in
         let smto = Options.smt () in
+
         if Some? smto then Some?.v smto
+        else if BU.file_exists local_z3 then local_z3
         else if inpath z3_v then z3_v
         else Platform.exe "z3"
       in
@@ -187,6 +190,14 @@ let warn_handler (suf:Errors.error_message) (s:string) : unit =
      blank 2 ^^ align (dquotes (arbitrary_string s));
     ] @ suf)
 
+let install_suggestion : Pprint.document =
+  let open FStarC.Errors.Msg in
+  let open FStarC.Pprint in
+  prefix 4 1 (text "Please download the correct version of Z3 from")
+             (url z3url) ^/^
+    group (text "and install it into your $PATH as" ^/^ squotes
+      (doc_of_string (Platform.exe ("z3-" ^ Options.z3_version  ()))) ^^ dot)
+
 (* Talk to the process to see if it's the correct version of Z3
 (i.e. the one in the optionstate). Also check that it indeed is Z3. By
 default, each of these generates an error, but they can be downgraded
@@ -221,10 +232,7 @@ let check_z3version (p:proc) : unit =
     Errors.log_issue0 Errors.Warning_SolverMismatch [
       text (BU.format3 "Unexpected Z3 version for '%s': expected '%s', got '%s'."
                   (proc_prog p) ver_conf ver_found);
-      prefix 4 1 (text "Please download the correct version of Z3 from")
-                 (url z3url) ^/^
-        group (text "and install it into your $PATH as" ^/^ squotes
-          (doc_of_string (Platform.exe ("z3-" ^ Options.z3_version  ()))) ^^ dot);
+      install_suggestion;
     ];
     Errors.stop_if_err(); (* stop now if this was a hard error *)
     _already_warned_version_mismatch := true
@@ -236,6 +244,16 @@ let new_z3proc (id:string) (cmd_and_args : string & list string) : BU.proc =
       try
         BU.start_process id (fst cmd_and_args) (snd cmd_and_args) (fun s -> s = "Done!")
       with
+      | e when BU.exn_is_enoent e ->
+        let open FStarC.Pprint in
+        let open FStarC.Errors.Msg in
+        Errors.raise_error0 Errors.Error_Z3InvocationError [
+          text "Z3 solver not found.";
+          prefix 2 1 (text "Required version:")
+            (text (Options.z3_version ()));
+          install_suggestion;
+        ]
+
       | e ->
         let open FStarC.Pprint in
         let open FStarC.Errors.Msg in