Merge pull request #3642 from mtzguido/cygwin

Improving Cygwin support

Author: mtzguido

src/basic/FStarC.Platform.fsti

@@ -8,5 +8,5 @@ type sys =
 val system : sys
 val exe : string -> string
 
-(* true if the fstar compiler is compiled from sources extracted to ocaml, false otherwise *)
-val is_fstar_compiler_using_ocaml : bool
+(* true when we are running in Cygwin. Note: system will return 'Windows' in this case *)
+val is_cygwin : bool

src/fstar/FStarC.Main.fst

@@ -166,9 +166,6 @@ let go_normal () =
 
     (* --print: Emit files in canonical source syntax *)
     | Success when Options.print () || Options.print_in_place () ->
-      if not Platform.is_fstar_compiler_using_ocaml then
-        failwith "You seem to be using the F#-generated version of the compiler ; \o
-                   reindenting is not known to work yet with this version";
       let printing_mode =
         if Options.print ()
         then Prettyprint.FromTempToStdout

src/ml/bare/FStarC_Compiler_Util.ml

@@ -188,8 +188,13 @@ let kill_process (p: proc) =
       attempt (fun () -> Unix.close (Unix.descr_of_in_channel p.inc));
       attempt (fun () -> Unix.close (Unix.descr_of_in_channel p.errc));
       attempt (fun () -> Unix.close (Unix.descr_of_out_channel p.outc));
+      (* Try to kill, but the process may already be gone. On Unix we
+         get ESRCH. On Windows, we apparently get EACCES (permission denied). *)
       (try Unix.kill p.pid Sys.sigkill
-       with Unix.Unix_error (Unix.ESRCH, _, _) -> ());
+       with Unix.Unix_error (Unix.ESRCH, _, _) -> ()
+          | Unix.Unix_error (Unix.EACCES, _, _) when FStarC_Platform.system = FStarC_Platform.Windows -> ()
+          ); 
+
       (* Avoid zombie processes (Unix.close_process does the same thing. *)
       waitpid_ignore_signals p.pid;
       (* print_string ("Killed process " ^ p.id ^ "\n" ^ (stack_dump()));       *)
@@ -341,29 +346,39 @@ let ask_process
     kill_process p; raise e
 
 let get_file_extension (fn:string) : string = snd (BatString.rsplit fn ".")
+
+(* NOTE: Working around https://github.com/ocaml-batteries-team/batteries-included/issues/1136 *)
+let is_absolute_windows (path_str : string) : bool =
+  if FStarC_Platform.system = FStarC_Platform.Windows then
+    match BatString.to_list path_str with
+    | '\\' :: _ -> true
+    | letter :: ':' :: '\\' :: _ -> BatChar.is_letter letter
+    | _ -> false
+  else
+    false
+
 let is_path_absolute path_str =
   let open Batteries.Incubator in
   let open BatPathGen.OfString in
-  let path_str' = of_string path_str in
-  is_absolute path_str'
+  let path = of_string path_str in
+  is_absolute path || is_absolute_windows path_str
+
 let join_paths path_str0 path_str1 =
   let open Batteries.Incubator in
   let open BatPathGen.OfString in
   let open BatPathGen.OfString.Operators in
   to_string ((of_string path_str0) //@ (of_string path_str1))
 
 let normalize_file_path (path_str:string) =
-  let open Batteries.Incubator in
-  let open BatPathGen.OfString in
-  let open BatPathGen.OfString.Operators in
-  to_string
-    (normalize_in_tree
-       (let path = of_string path_str in
-         if is_absolute path then
-           path
-         else
-           let pwd = of_string (BatSys.getcwd ()) in
-           pwd //@ path))
+  if is_path_absolute path_str then
+    path_str
+  else
+    let open Batteries.Incubator in
+    let open BatPathGen.OfString in
+    let open BatPathGen.OfString.Operators in
+    let path = of_string path_str in
+    let cwd = of_string (BatSys.getcwd ()) in
+    to_string (normalize_in_tree (cwd //@ path))
 
 type stream_reader = BatIO.input
 let open_stdin () = BatIO.stdin

src/ml/bare/FStarC_Platform.ml

@@ -14,4 +14,4 @@ let exe name =
   else
     name^".exe"
 
-let is_fstar_compiler_using_ocaml = true
+let is_cygwin = Sys.cygwin

tests/dune_hello/Makefile

@@ -4,6 +4,9 @@ FSTAR_EXE ?= fstar.exe
 
 .PHONY: all
 all: run
+ifneq ($(OS),Windows_NT) # See comment in ../simple_hello/Makefile
+all: run.bc
+endif
 
 Hello.ml: Hello.fst
 	$(FSTAR_EXE) --codegen OCaml Hello.fst --extract Hello --z3version 4.13.3
@@ -15,6 +18,8 @@ bin/hello.exe: Hello.ml
 .PHONY: run
 run: bin/hello.exe
 	./bin/hello.exe | grep "Hi!"
+
+run.bc: bin/hello.exe
 	# Find a way to install this? dune install skips the bytecode
 	$(FSTAR_EXE) --ocamlenv dune exec ./hello.bc | grep "Hi!"
 

tests/simple_hello/Makefile

@@ -6,11 +6,19 @@
 # just take fstar.exe from the PATH.
 FSTAR_EXE ?= fstar.exe
 
-all: Hello.test
+all: Hello.exe.test
 
-Hello.test: Hello.exe Hello.byte
-	./Hello.exe  | grep "Hello F\*!"
-	./Hello.byte | grep "Hello F\*!"
+# In a Cygwin build, somehow this dll is not the search path (copying it
+# to this directory does make the test work). Just skip it for now.
+# $ ./Hello.byte
+# Fatal error: cannot load shared library dllzarith
+# Reason: No such file or directory
+ifneq ($(OS),Windows_NT)
+all: Hello.byte.test
+endif
+
+Hello.%.test: Hello.%
+	./$< | grep "Hello F\*!"
 
 %.ml: %.fst
 	$(FSTAR_EXE) --codegen OCaml $< --extract $* --z3version 4.13.3