use cygwin paths for DUNE_SNAPSHOT variable

.common.mk

@@ -1,5 +1,6 @@
 # This makefile is included from several other makefiles in the tree.
-# Its only purpose is to enable configurably 'silent' rules, that do not
+
+# It enables configurably 'silent' rules, that do not
 # print output unless V=1 is set. When writing a rule, you can do as
 # follows (taken from src/Makefile.boot):
 #
@@ -18,6 +19,9 @@
 # Besides that, when not using V=1, F* receives the --silent flag to
 # reduce non-critical output.
 
+# It also defines some other utilities for resource monitoring and
+# paths manipulation for cygwin
+
 Q?=@
 SIL?=--silent
 RUNLIM=
@@ -48,3 +52,8 @@ ifneq ($(RESOURCEMONITOR),)
 	endif
 	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
 endif
+
+# Can be called as $(call maybe_cygwin_path,...)
+#   where ... is the argument
+
+maybe_cygwin_path=$(if ($(ifeq ($(OS),Windows_NT) "y" endif)),$(shell cygpath -m $(1)),$(1))

Makefile

@@ -4,19 +4,15 @@ include .common.mk
 
 all: dune
 
-DUNE_SNAPSHOT ?= $(CURDIR)/ocaml
+DUNE_SNAPSHOT ?= $(call maybe_cygwin_path,$(CURDIR)/ocaml)
 
 # The directory where we install files when doing "make install".
 # Overridden via the command-line by the OPAM invocation.
 PREFIX ?= /usr/local
 
-ifeq ($(OS),Windows_NT)
-  # On Cygwin, the `--prefix` option to dune only
-  # supports Windows paths.
-  FSTAR_CURDIR=$(shell cygpath -m $(CURDIR))
-else
-  FSTAR_CURDIR=$(CURDIR)
-endif
+# On Cygwin, the `--prefix` option to dune only
+# supports Windows paths.
+FSTAR_CURDIR=$(call maybe_cygwin_path,$(CURDIR))
 
 .PHONY: dune dune-fstar verify-ulib
 FSTAR_BUILD_PROFILE ?= release

src/Makefile.boot

@@ -16,7 +16,7 @@ FSTAR_BOOT ?= $(FSTAR)
 # FSTAR_C: This is the way in which we invoke F* for boostrapping
 #   -- we use automatic dependence analysis based on files in ulib, src/{basic, ...} and boot
 #   -- MLish and lax tune type-inference for use with unverified ML programs
-DUNE_SNAPSHOT ?= $(FSTAR_HOME)/ocaml
+DUNE_SNAPSHOT ?= $(call maybe_cygwin_path,$(FSTAR_HOME)/ocaml)
 OUTPUT_DIRECTORY = $(DUNE_SNAPSHOT)/fstar-lib/generated
 FSTAR_C=$(RUNLIM) $(FSTAR_BOOT) $(SIL) $(FSTAR_BOOT_OPTIONS) --cache_checked_modules
 

src/ocaml-output/Makefile

@@ -13,7 +13,7 @@ OCAMLLEX=ocamllex
 FSTAR_OCAMLBUILD_EXTRAS ?= -cflag -g
 
 FSTAR_HOME = ../..
-DUNE_SNAPSHOT ?= $(realpath $(FSTAR_HOME)/ocaml)
+DUNE_SNAPSHOT ?= $(call maybe_cygwin_path,$(realpath $(FSTAR_HOME)/ocaml))
 export DUNE_SNAPSHOT
 
 FStar_Parser_Parse_ml=$(DUNE_SNAPSHOT)/fstar-lib/generated/FStar_Parser_Parse.ml
@@ -119,13 +119,9 @@ install_dir = cd ../../$(1) && find . -type f -exec $(INSTALL_EXEC) -m 644 -D {}
 # Install FStar into $(PREFIX) using the standard Unix directory
 # structure.
 
-ifeq ($(OS),Windows_NT)
-  # On Cygwin, the `--prefix` option to dune only
-  # supports Windows paths.
-  FSTAR_PREFIX=$(shell cygpath -m $(PREFIX))
-else
-  FSTAR_PREFIX=$(PREFIX)
-endif
+# On Cygwin, the `--prefix` option to dune only
+# supports Windows paths.
+FSTAR_PREFIX=$(call maybe_cygwin_path,$(PREFIX))
 
 FSTAR_BUILD_PROFILE ?= release
 
@@ -174,13 +170,9 @@ endif
 # Create a zip / tar.gz package of FStar that contains a Z3 binary and
 # proper license files.
 
-ifeq ($(OS),Windows_NT)
-  # On Cygwin, the `--prefix` option to dune only
-  # supports Windows paths.
-  package_prefix=$(shell cygpath -m $(CURDIR))/fstar
-else
-  package_prefix=$(CURDIR)/fstar
-endif
+# On Cygwin, the `--prefix` option to dune only
+# supports Windows paths.
+package_prefix=$(call maybe_cygwin_path,$(CURDIR)/fstar)
 
 package_dir = cd ../../$(1) && find . -type f -exec $(INSTALL_EXEC) -m 644 -D {} $(package_prefix)/$(2)/{} \;
 

ulib/Makefile.extract-stdlib

@@ -1,19 +1,19 @@
 .PHONY: indent extra
 
 FSTAR_HOME=..
-DUNE_SNAPSHOT ?= $(realpath $(FSTAR_HOME)/ocaml)
-
 include ml/Makefile.realized
+
 NOEXTRACT_MODULES += +FStar.Pervasives -FStar.Pervasives.Native -FStar.Reflection -FStar.Tactics -Steel
 
 #The steel files are included below for native compilation of the framing tactic
 
-OUTPUT_DIRECTORY=$(DUNE_SNAPSHOT)/fstar-lib/generated
-
 include $(FSTAR_HOME)/.common.mk
 include gmake/z3.mk
 include gmake/fstar.mk
 
+DUNE_SNAPSHOT ?= $(call maybe_cygwin_path,$(realpath $(FSTAR_HOME)/ocaml))
+OUTPUT_DIRECTORY=$(DUNE_SNAPSHOT)/fstar-lib/generated
+
 FSTAR_FILES:=$(filter-out $(NOEXTRACT_FILES),$(wildcard *.fst *.fsti))
 
 CODEGEN = OCaml

ulib/Makefile.extract-taclib

@@ -1,21 +1,20 @@
 .PHONY: indent extra
 
 FSTAR_HOME=..
-DUNE_SNAPSHOT ?= $(realpath $(FSTAR_HOME)/ocaml)
-
 include ml/Makefile.realized
 
 #AR: 01/03
 NOEXTRACT_FILES=$(wildcard experimental/Steel.*.fst experimental/Steel.*.fsti)
 
 #The steel files are included below for native compilation of the framing tactic
 
-OUTPUT_DIRECTORY=$(DUNE_SNAPSHOT)/fstar-lib/generated
-
 include $(FSTAR_HOME)/.common.mk
 include gmake/z3.mk
 include gmake/fstar.mk
 
+DUNE_SNAPSHOT ?= $(call maybe_cygwin_path,$(realpath $(FSTAR_HOME)/ocaml))
+OUTPUT_DIRECTORY=$(DUNE_SNAPSHOT)/fstar-lib/generated
+
 FSTAR_FILES:=$(filter-out $(NOEXTRACT_FILES),$(wildcard *.fst *.fsti)) $(wildcard FStar.InteractiveHelpers.*.fst)
 
 ifneq ($(STAGE_EXPERIMENTAL),0)

ulib/ml/Makefile

@@ -12,7 +12,10 @@ INTFILES_RAW=\
 	FStar_UInt64.ml
 
 FSTAR_HOME ?= $(realpath ../..)
-DUNE_SNAPSHOT ?= $(FSTAR_HOME)/ocaml
+
+include $(FSTAR_HOME)/.common.mk
+
+DUNE_SNAPSHOT ?= $(call maybe_cygwin_path,$(FSTAR_HOME)/ocaml)
 
 TARGET_DIR=$(DUNE_SNAPSHOT)/fstar-lib/generated/
 INTFILES=$(addprefix $(TARGET_DIR),$(INTFILES_RAW))