Mirror-core doesn't seem to build on Windows

[JasonGross]

make -C theories
make[1]: Entering directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make -f Makefile.coq
make[2]: Entering directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make[2]: Nothing to be done for 'all'.
make[2]: Leaving directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make[1]: Leaving directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make -C src
make[1]: Entering directory '/cygdrive/c/coq-bundle/mirror-core/src'
ocamlbuild mirror-core.otarget
00:00:00 1    (0   ) myocamlbuild.exe                                -------- |←
[KFile "myocamlbuild.ml", line 1, characters 13-14:
Error: Illegal character (\000)
←[KExit code 2 while executing this command:
  ''C:/coq-bundle/bin/ocamlopt.opt -I 'C:/coq-bundle/lib/ocaml\ocamlbuild' unix.
cmxa 'C:/coq-bundle/lib/ocaml\ocamlbuild/ocamlbuildlib.cmxa' myocamlbuild.ml 'C:
/coq-bundle/lib/ocaml\ocamlbuild/ocamlbuild.cmx' -o myocamlbuild.exe
Compilation unsuccessful after building 1 target (0 cached) in 00:00:00.←[K
Makefile:2: recipe for target 'plugin' failed
make[1]: *** [plugin] Error 2
make[1]: Leaving directory '/cygdrive/c/coq-bundle/mirror-core/src'
Makefile:7: recipe for target 'plugin' failed
make: *** [plugin] Error 2

If I run make again, I get

C:\coq-bundle\mirror-core>make
make -C theories
make[1]: Entering directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make -f Makefile.coq
make[2]: Entering directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make[2]: Nothing to be done for 'all'.
make[2]: Leaving directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make[1]: Leaving directory '/cygdrive/c/coq-bundle/mirror-core/theories'
make -C src
make[1]: Entering directory '/cygdrive/c/coq-bundle/mirror-core/src'
ln: failed to create symbolic link `myocamlbuild.ml': File exists
Makefile:9: recipe for target 'myocamlbuild.ml' failed
make[1]: *** [myocamlbuild.ml] Error 1
make[1]: Leaving directory '/cygdrive/c/coq-bundle/mirror-core/src'
Makefile:7: recipe for target 'plugin' failed
make: *** [plugin] Error 2

This is using Pierre Yves-Strub's coq-bundle. I suspect the problem is that cygwin/windows doesn't do symlinks correctly.

[JasonGross]

Also, $(COQLIB)user-contrib/PluginUtils/myocamlbuild.ml doesn't exist for me.

[gmalecha]

coq-plugin-utils (https://github.com/gmalecha/coq-plugin-utils) needs to also be installed in order to build the plugin. Can you install that and then see if it builds? Ultimately, you need either a symlink or a copy of the myocamlbuild.ml file distributed with that that project in order to build the plugin.

I think that that will get pushed into ExtLib.

[JasonGross]

C:\coq-bundle\coq-plugin-utils>make
make -C src
make[1]: Entering directory '/cygdrive/c/coq-bundle/coq-plugin-utils/src'
ocamlbuild coq.otarget
mkdir 'C:\coq-bundle\coq-plugin-utils\src\_build'
00:00:00 1    (0   ) myocamlbuild.exe                                -------- \←
Finished, 1 target (0 cached) in 00:00:01.←[K
00:00:00 1    (0   ) use_ltac.mli.depends                            O------- \←
00:00:00 2    (0   ) use_ltac.cmi                                    O-B---I- |←
00:00:00 4    (0   ) term_match.ml.depends                           O-b---i- |←
00:00:00 6    (0   ) coqstd.cmi                                      O-B---I- /←
00:00:00 8    (0   ) use_ltac.cmo                                    O-B---i- /←
00:00:00 9    (0   ) term_match.cmo                                  O-B---i- /←
00:00:00 11   (0   ) plugin_utils.cmo                                O-B---i- /←
00:00:00 13   (0   ) term_match.cmx                                  ONb---i- -←
00:00:00 14   (0   ) coqstd.cmx                                      ONb---i- -←
00:00:00 15   (0   ) plugin_utils.cmx                                ONb---i- -←
00:00:00 16   (0   ) plugin_utils.cma                                OnB---iL \←
00:00:01 18   (0   ) ...ugin-utils\src\_build/plugin_utils.cma' ..   onb---il |←
Finished, 20 targets (0 cached) in 00:00:01.←[K
make[1]: Leaving directory '/cygdrive/c/coq-bundle/coq-plugin-utils/src'
C:\coq-bundle\coq-plugin-utils>make install COQLIB="C:/coq-bundle/lib/coq/"
make -C src
make[1]: Entering directory '/cygdrive/c/coq-bundle/coq-plugin-utils/src'
ocamlbuild coq.otarget
Finished, 0 targets (0 cached) in 00:00:00.←[K
←[KSANITIZE: a total of 3 files that should probably not be in your source tree
  has been found. A script shell file
  "C:\\coq-bundle\\coq-plugin-utils\\src\\_build/sanitize.sh" is being
  created. Check this script and run it to remove unwanted files or use other
  options (such as defining hygiene exceptions or using the -no-hygiene
  option).
IMPORTANT: I cannot work with leftover compiled files.
ERROR: Leftover OCaml compilation files:
  File plugin_utils.cmx in . has suffix .cmx
  File plugin_utils.cma in . has suffix .cma
  File plugin_utils.cmxa in . has suffix .cmxa
←[KExiting due to hygiene violations.
Compilation unsuccessful after building 0 targets (0 cached) in 00:00:00.←[K
Makefile:4: recipe for target 'all' failed
make[1]: *** [all] Error 1
make[1]: Leaving directory '/cygdrive/c/coq-bundle/coq-plugin-utils/src'
Makefile:5: recipe for target 'plugin' failed
make: *** [plugin] Error 2

[JasonGross]

But if I run sanitize, then it installs

[gmalecha]

That's good. I'll take a look at it tonight and see if there is a tweak to make things work better on Windows.

[JasonGross]

And then mirror-core builds. And I see you've updated the readme.

[gmalecha]

Should I consider this fixed, i.e. if you start with a clean slate and install the dependencies first then does everything work or do you still need to do some hacking?

[JasonGross]

I think there is still an issue with installing ext-lib (that it gives me an error on install and tells me that I need to run sanitize.sh, and if I do that, then it works), but mirror-core itself installs fine assuming the dependencies are installed, so I'll close this issue.