[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

@@ -30,7 +30,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
@@ -90,9 +90,14 @@ bootstrap:
 
 bootstrap-build: bootstrap
 	$(DUNE_BOOT_PATH)/dune build $(DUNEOPT) @vodeps
-	$(DUNE_BOOT_PATH)/dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d
+	$(DUNE_BOOT_PATH)/dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d
 	$(DUNE_BOOT_PATH)/dune build @install
 
+bootstrap-build-nogtk: bootstrap
+	$(DUNE_BOOT_PATH)/dune build $(DUNEOPT) @vodeps
+	$(DUNE_BOOT_PATH)/dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d
+	$(DUNE_BOOT_PATH)/dune build coq.install coqide-server.install @runtest
+
 # Other common dev targets
 #
 # dune build coq.install

dev/ci/appveyor.sh

@@ -12,4 +12,8 @@ opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $A
 eval "$(opam config env)"
 opam install -y num ocamlfind ounit
 
-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 bootstrap-build-nogtk
+
+# 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

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))

test-suite/misc/universes/dune

@@ -5,4 +5,4 @@
    (source_tree ../../../plugins))
  (action
    (with-outputs-to all_stdlib.v
-    (run ./build_all_stdlib.sh))))
+    (bash "./build_all_stdlib.sh"))))

tools/coq_dune.ml

@@ -136,7 +136,7 @@ type vodep = {
   deps : string list;
 }
 
-type ldep = | VO of vodep | ML4 of string | MLG of string
+type ldep = | VO of vodep | MLG of string
 type ddir = ldep list DirMap.t
 
 (* Filter `.vio` etc... *)
@@ -181,23 +181,17 @@ let pp_vo_dep dir fmt vo =
   let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in
   pp_rule fmt [vo.target] deps action
 
-let pp_ml4_dep _dir fmt ml =
-  let target = Filename.(remove_extension ml) ^ ".ml" in
-  let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in
-  pp_rule fmt [target] [ml] ml4_rule
-
 let pp_mlg_dep _dir fmt ml =
   let target = Filename.(remove_extension ml) ^ ".ml" in
   let ml4_rule = "(run coqpp %{pp-file})" in
   pp_rule fmt [target] [ml] ml4_rule
 
 let pp_dep dir fmt oo = match oo with
   | VO vo -> pp_vo_dep dir fmt vo
-  | ML4 f -> pp_ml4_dep dir fmt f
   | 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"
@@ -220,21 +214,17 @@ let record_dune d ff =
     eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd
 
 (* File Scanning *)
-let choose_ml4g_form f =
-  if Filename.check_suffix f ".ml4" then ML4 f
-  else MLG f
-
-let scan_mlg4 m d =
+let scan_mlg m d =
   let dir = ["plugins"; d] in
   let m = DirMap.add dir [] m in
   let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg"))
                    Array.(to_list @@ readdir (bpath dir))) in
-  List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4
+  List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m ml4
 
 let scan_plugins m =
   let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
   let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
-  List.fold_left scan_mlg4 m dirs
+  List.fold_left scan_mlg m dirs
 
 (* Process .vfiles.d and generate a skeleton for the dune file *)
 let parse_coqdep_line l =
@@ -272,8 +262,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 _ =