Dune build: don't require a bash for building

[MSoegtropIMC]

On Windows having a Posix compliant shell is difficult. @ejgallego pointed out that it wouldn't be difficult to have a Dune based build system for Coq projects which would not require aPosix shell. This would greatly simplify building Coq projects on Windows.

I Labeled this as feature because on Windows it would indeed be a valuable user facing feature to have a reliable build system, which does not require a bash.

[SkySkimmer]

Posix shell and bash are not the same thing, which do you mean?

[ejgallego]

Places to modify come from #8421 :

(action (bash "./make_jumptbl.sh %{h-file} %{targets}")))
(action (bash "./make_opcodes.sh %{h-file} %{targets}")))

all that we need is to write an OCaml program doing the same; this should be easy [and even better than the sh solution]

The test suite is another story, the Windows build of Dune works quite well as of today, however the test-suite is having some path problems I need to solve.

[MSoegtropIMC]

@SkySkimmer : of cause one should restrict one self to Posix and not using and bash specific stuff. But even having a reasonably small Posix subset on Windows is hard. I actually started to write a Posix sibset shell for system functions in programming languages cause it is such a pain.

@ejgallego : as I said I already started to write a shell replacement intended to replace the OCaml system function.

[ejgallego]

I am not rewriting this couple of scripts for now; however that should be pretty easy for anyone willing to have the shell-free build on Win, but indeed that's better by a windows user.

By the way @MSoegtropIMC you may be interested on https://discuss.ocaml.org/t/preferred-ocaml-windows-environments-mainly-for-continuous-integration/3299/3

[ejgallego]

@MSoegtropIMC so this was basically solved by #9624 , even if we have a couple of minor places that still use bash, these should be very easy to fix. In fact we won't depend on bash neither on a shell.

So the big question is, how do we actually test the bash-less build?

[MSoegtropIMC]

So the big question is, how do we actually test the bash-less build?

Well on Windows this is easy. My build scripts create a MinGW Coq in an folder outside of Cygwin so that it can be started without having a cygwin in the path. This folder than servers as a template for creating the installer. If Coq is started from this folder there there is no bash or other shell (besides CMD).

[ejgallego]

Will ocaml even work in that case?

Anyways, you can try when you feel like it, another minor patch is necessary for coq but that's all to be done with the coq part of this bug.

[MSoegtropIMC]

Will ocaml even work in that case?

Well no - this is the reason I started this mini posix shell project. I did an analysis back then and concluded that by replacing the OCaml library system command with this mini shell, OCaml and its support tools should work on Windows and furthermore that I could remove a lot of Windows hacks all over the place. If dune will fix this in the same way I can't tell.

[ejgallego]

Dune doesn't call bash [unless (bash ...) is used], however it does call OCaml, YMMV :)

[MSoegtropIMC]

It has been a while since I looked into it. Afair OCaml at some point calls gcc as a wrapper for gnu binutil tools and this was also slightly problematic e.g. in terms of command line length and quoting. This means it should work in not too exotic cases, but it likely won't work with very long command lines or file names requiring more subtle quoting.

I guess it is best if I again do some deeper analysis of the situation and write a short report on the topic, so that we can make proper decisions. I still think that it is a good idea to have a system independent abstraction of "command line tool process creation" in OCaml, though.

[ejgallego]

@MSoegtropIMC this is so far solved, so I will close this issue soon as I remove the last call to bash due to handling to .v files.

[MSoegtropIMC]

@ejgallego : great to hear - I will look into providing a dune executable in the Windows build then.

One question: would you expect that OCaml and Coq native build also work then? If not, what would be missing? As far as I remember (it is >2 years back) the main issue with native compute on Windows was ocamlbuild and its use of a shell. The ocaml compiler itself was fine afair.

[ejgallego]

One question: would you expect that OCaml and Coq native build also work then?

If that was the main issue I think we will definitively see an improvement as Dune has its own implementation of META file parsing and doesn't ever call a shell.

It is early to tell tho as I haven't completed support for native compute in Dune yet.

[ejgallego]

Dune has its own implementation of META file parsing and doesn't ever call a shell.

This is in fact done so Dune can be a true root of the dependency chain. As it stands today, Dune has zero runtime dependencies [not even the OCaml compiler]

[MSoegtropIMC]

It is early to tell tho as I haven't completed support for native compute in Dune yet.

it sounds like a plan for native compute for the future. Please let me know as soon as you think it is time to give it a try on windows. Everything else I have (MinGW ocaml, gcc, binutils, ...), it is just disabled currently.

[ejgallego]

native compute support in Dune is ready barring a technical problem with Coq outputting outside it's own directory which interferes with some target dir sandboxing Dune has; this problem has the potential to delay support by a while unfortunately.

[Zimmi48]

This issue should be closed (if it is solved in 8.10) or postponed to 8.11 (if there are still bits to do).

[ejgallego]

There is one use of bash still, which can be removed by using Dune master; however if you are curious I am waiting to remove the bootstrap hack as to provide composition capabilities in Dune.

The reason is as follows: the stdlib can be compiled with Dune, however there is a special directory Init that requires a special flag. We could always add some hack to Dune, however it seems to me that I'd be more natural to declare two libs Coq.Init and Coq and have them compose.

What do you think?

I'll open an issue to talk about that as soon as I have the Dune PR ready, the current namespacing is a bit delicate so it is not clear how to do right; maybe in the end we want to treat the stdlib as an atomic entity [for now] and just have a field to provide per-module flags.

[Zimmi48]

I think I wouldn't mind the split in two libs if that helps, but I am not sure I can actually see the issue.

[ejgallego]

I am not sure I can actually see the issue.

• Coq.Init.* has to be compiled with -noinit
• The rest of Coq shouldn't use that flag, and has an implicit dependency on Prelude.vo which coqdep doesn't output [this is also a problem :S]

[ejgallego]

Bash is still used in:

• building the documentation
• running the test-suite
• shim developers target

So we are on the edge of being able to close this, one could argue that for test-suite / shim targets we can require bash. However, for documentation that's a different story.

[ejgallego]

Incredible work by @Alizter and @rlepigre means that the test suite will soon work on dune, and a few of the shims may go away!

[ejgallego]

(Likely final) report on this: I can now build Coq on Windows native with Opam 2.2 without too much trouble. Current problems are:

• ocamlfind is buggy, but a patch exists (c.f. https://github.com/ocaml/opam/issues/6129)
• Coq's configure does not properly detect the arch, as it assumes uname exists, this can be workarounded by hand.
• the revision file is still generated by bash

Other than that, Coq is functional from a regular PowerShell + dune build setup.