[dune] [ci] [appveyor] Fix and test Dune for Windows.

Unfortunately our `.vo` building scheme introduces a bit of pitfall as
it needs a POSIX shell and `system` is `cmd.exe` on Windows.
Hopefully, this bit of hack will go away when Dune can understand Coq
libraries.

Another core problem is that shell scripts (`kernel/**.sh`,
`mkcamlp5.opt`) cannot be called with `(run ...)` on Windows, so we
must use `(bash ...)` which is far from ideal.

We also add some minimal testing of a Dune build on Windows, this
should take 3/4 minutes so I believe it is acceptable.

Current problem on windows is that the loadpath is set sometimes to
`_build/install/default/lib/coq/theories/Init`

and others to

`_build/default/theories/Init/`

due to coqroot being a strange thing in Win32 due to lack of symlinks,
which makes it work by miracle on Unix.

Makefile.dune

@@ -24,7 +24,7 @@ help:
 
 voboot:
 	dune build $(DUNEOPT) @vodeps
-	dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d
+	dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d
 
 states: voboot
 	dune build $(DUNEOPT) theories/Init/Prelude.vo

dev/ci/appveyor.sh

@@ -10,6 +10,10 @@ bash opam64/install.sh
 
 opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH
 eval "$(opam config env)"
-opam install -y num ocamlfind camlp5 ounit
+opam install -y num ocamlfind camlp5 ounit dune
 
-cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
+# Basic Dune build
+cd "$APPVEYOR_BUILD_FOLDER" && make -f Makefile.dune release
+
+# Full regular Coq Build
+# cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate

dune

@@ -17,7 +17,7 @@
  (deps
   (source_tree theories)
   (source_tree plugins))
- (action (with-stdout-to .vfiles.d (system "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`"))))
+ (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`"))))
 
 (alias
  (name vodeps)
@@ -33,7 +33,7 @@
 (rule
  (targets revision)
  (deps (:rev-script dev/tools/make_git_revision.sh))
- (action (with-stdout-to revision (run %{rev-script}))))
+ (action (with-stdout-to revision (bash %{rev-script}))))
 
 ; Use summary.log as the target
 (alias

grammar/dune

@@ -8,18 +8,25 @@
 
 ; Custom camlp5! This is a net speedup, and a preparation for using
 ; Dune's preprocessor abilities.
+
+; Note: We could replace this by an executable stanza, current code of
+; mkcamlp5.opt is:
+; $ ocamlopt odyl.cmxa camlp5.cmxa odyl.cmx $OPTS -linkall
 (rule
- (targets coqmlp5)
- (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx -o coqmlp5)))
+ (targets coqmlp5.exe)
+ (action (bash "mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx -o coqmlp5.exe")))
 
 (rule
- (targets coqp5)
- (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5)))
+ (targets coqp5.exe)
+ (action (bash "mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5.exe")))
+
+(rule (copy coqp5.exe coqp5))
+(rule (copy coqmlp5.exe coqmlp5))
 
 (install
  (section bin)
  (package coq)
- (files coqp5 coqmlp5))
+ (files coqp5 coqp5.exe coqmlp5 coqmlp5.exe))
 
 (rule
  (targets q_util.ml)

kernel/byterun/dune

@@ -6,5 +6,5 @@
 
 (rule
  (targets coq_jumptbl.h)
- (deps (:h-file coq_instruct.h))
- (action (run ./make_jumptbl.sh %{h-file} %{targets})))
+ (deps (:h-file coq_instruct.h) make_jumptbl.sh)
+ (action (bash "./make_jumptbl.sh %{h-file} %{targets}")))

kernel/dune

@@ -8,8 +8,8 @@
 
 (rule
  (targets copcodes.ml)
- (deps (:h-file byterun/coq_instruct.h) make-opcodes)
- (action (run ./make_opcodes.sh %{h-file} %{targets})))
+ (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh)
+ (action (bash "./make_opcodes.sh %{h-file} %{targets}")))
 
 (documentation
  (package coq))

lib/envars.ml

@@ -72,7 +72,12 @@ let coqbin =
 (** The following only makes sense when executables are running from
     source tree (e.g. during build or in local mode). *)
 let coqroot =
-  Filename.dirname coqbin
+  (* In Dune, Windows files are not installed with a symbolic link
+     thus we need a different rule *)
+  if Coq_config.arch_is_win32
+  (* this is install/default + /../../default  *)
+  then Filename.(dirname coqbin ^ dir_sep ^ ".." ^ dir_sep ^ ".." ^ dir_sep ^ "default")
+  else Filename.dirname coqbin
 
 (** On win32, we add coqbin to the PATH at launch-time (this used to be
     done in a .bat script). *)

tools/coq_dune.ml

@@ -195,7 +195,7 @@ let pp_dep dir fmt oo = match oo with
   | MLG f -> pp_mlg_dep dir fmt f
 
 let out_install fmt dir ff =
-  let itarget = String.concat "/" dir in
+  let itarget = bpath dir in
   let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in
   let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (bpath [itarget;tg]) in
   fprintf fmt "(install@\n @[(section lib)@\n(package coq)@\n(files @[%a@])@])@\n"
@@ -270,8 +270,13 @@ let exec_ifile f =
   match Array.length Sys.argv with
   | 1 -> f stdin
   | 2 ->
-    let ic = open_in Sys.argv.(1) in
-    (try f ic with _ -> close_in ic)
+    let in_file = Sys.argv.(1) in
+    begin try
+      let ic = open_in in_file in
+      (try f ic
+       with _ -> eprintf "Error: exec_ifile@\n%!"; close_in ic)
+      with _ -> eprintf "Error: cannot open input file %s@\n%!" in_file
+    end
   | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1
 
 let _ =