dune support

[Alizter]

We add the files needed to build the library using dune. This is an opt-in feature and does not affect anybody.

Dune is a build system (for OCaml) and can be thought as an alternative to Makefile based build systems. It has various advantages over Makefile based systems. Currently, Coq itself is built using dune, this means that you probably already have it installed. If you want to see how the library builds just go to your HoTT folder and run dune build (after checking out this PR).

Dune has various useful features such as incremental builds and caching. Built files can be found in the (ignored) _build/ directory, not littering the source tree.

In the future we might want to start testing dune in our CI.

Currently due to the way our _CoqProject is generated, using dune together with an IDE is a bit awkward since the Coq arguments will have to be passed manually. Hopefully this will improve in the future.

cc @ejgallego

[artagnon]

Is there some issue with dune 3.0? I see that 3.0.2 was released 11 days ago.

[Alizter]

I don't want to require a newer dune dependency for the project, so I will am content with keeping the base version (used for compiling coq). Dune 3.0 is quite new and still under active development, so it will be some time before Coq moves to that version.

[Alizter]

Something else that should be noted: We currently autogenerate our _CoqProject file from scratch using a script, this allows for editors such as PG and CoqIDE to work with the project. If we compile using dune, _CoqProject can only appear in the _build directory. Even if we modify the _CoqProject that gets generated to work with dune, it won't be present in the source tree without calling make first.

The only way around this is for editors to understand dune files, which there are currently WIP developments to do. But that isn't related to our project.

[artagnon]

There's a (hacky) workaround, at least for VSCoq: if we use -R _build/default/<rest> instead of -R <rest> in the _CoqProject, everything should Just Work. I have _CoqProject generated in-source-tree working on my end: will post a diff soon.

[Alizter]

But _CoqProject only appears in the source-tree because you called make right? It's not possible AFAIK to get dune to do this.

[artagnon]

@Alizter Here's what I have: it shows some spurious errors, and the source tree needs to be cleaned of the _CoqProject before dune can be called again, but I think there's probably a way around it: trawling through the dune docs now.

diff --git a/dune-project b/dune-project
index 94bcf6237e..f25f09e1f0 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,5 @@
-(lang dune 2.9)
+(lang dune 3.0)
+
 (using coq 0.3)
+
 (name HoTT)
diff --git a/etc/generate_coqproject.sh b/etc/generate_coqproject.sh
old mode 100644
new mode 100755
index 417dedb70e..edb79c4265
--- a/etc/generate_coqproject.sh
+++ b/etc/generate_coqproject.sh
@@ -1,5 +1,6 @@
 ## List tracked .v files
-if [ -e .git ]; then
+cd "$(git rev-parse --show-toplevel)"
+if [ $? -eq 0 ]; then
   TRACKED_V_FILES="$(git ls-files "*.v")"
 else
   echo "Warning: Not a git clone, using find instead" >&2
diff --git a/theories/dune b/theories/dune
index c737a62771..53a4e45b96 100644
--- a/theories/dune
+++ b/theories/dune
@@ -1,4 +1,7 @@
-(include_subdirs qualified) ; Tell dune to look through subdirectories
+(include_subdirs qualified)
+
+; Tell dune to look through subdirectories
+
 (dirs :standard theories contrib)

 (coq.theory
@@ -8,16 +11,14 @@
  (flags
   -noinit ; Don't load standard library
   -indices-matter ; Universe levels of index types in inductive types are used to calculate universe level
-    -color on))	     ; Allow color printing (good for errors)
+  -color
+  on))

-; Doesn't really work atm
-(rule (alias _CoqProject)
-  (deps ./etc/generate_coqproject.sh)
-  (action (bash ./etc/generate_coqproject.sh))
-)
+; Allow color printing (good for errors)

-;; Rule for validation -- For dune 3.0
-;;(rule (alias validate)
-;;  (deps (glob_files_rec ./*.vo))
-;;  (action (run coqchk -R . HoTT %{deps} -o))
-;;)
+(rule
+ (alias validate)
+ (deps
+  (glob_files_rec ./*.vo))
+ (action
+  (run coqchk -R . HoTT %{deps} -o)))

[ejgallego]

Folks I have no time this week to help with this, maybe we could do a session on the upcoming Dune hacking day?

[artagnon]

Actually, scratch that. I know the solution, at least for VSCoq: it only needs a _CoqProject with -R _build/default/<dirname>, and nothing else. We don't need to generate the entire _CoqProject.

[artagnon]

The only issue with this is that a _CoqProject will be checked in, and a make-based workflow will overwrite it, resulting in a dirty git index. We have three options:

1. Don't support IDEs with dune-based workflow.
2. Support VSCoq with proposed _CoqProject checked in; live with dirty index for people who want to use make-based build.
3. Drop support for make-based build, and have just the dune build.

[Alizter]

@artagnon HoTT is unlike other coq projects where a simple _CoqProject is given including all the -R _build lines. We generate the entire thing from scratch, this is because our default build system is coq_makefile and that only understands the long elaborate _CoqProject. This PR allows somebody to build the repository using dune.

However if you use dune to build this repo, and then fire up CoqIDE, you will be confused to why nothing it working. The reason is _CoqProject is not present, the only way to do that is to run the script generating it. Make can do this fine, since it doesn't mind polluting the source directory, but AFAIK this is impossible to do from dune since it never pollutes the source directory.

For now if you want to develop using dune, you will need to run the ./etc/generate_coqproject.sh script at least once so that the -R lines (and other options) are at least present. We should probably patch that script to also include the _build directory.

There is also the question of "why not just use dune for everything instead?". Unfortunately, dune doesn't have support for various things that we like to do in our makefile, such as building documentation, timing, etc. This PR was just an attempt at letting people build the library with dune if they so desired. (Support for these various things will come in the future, but are simply not implemented yet).

@ejgallego The core issue here is the lack of editor support for dune rather than anything else, so it needs an independent fix.

[Alizter]

And on a more design note, any IDE claiming to have support for Coq should be able to support both coq_makefile and dune projects without having to choose one or the other. You should think of it as "HoTT uses coq_makefile but there is experimental support with a few bells and whistles to also build using dune".

[Alizter]

Note to self, we can create a dune rule that will produce the makefile no problem. So eventually do this.

[Alizter]

The .opam file is now generated by dune. This also means that the opam jobs in the CI test the dune build. However the docker images don't have dune >= 3.0 so we are stuck for the time being.

[Alizter]

And to be clear, I managed to get _CoqProject to be generated by dune in the source directory so IDEs should work fine.

[jdchristensen]

I tested this and it works for me. The changes don't seem intrusive at all, so I think it would be fine to merge it. But I don't know much about dune.

[Alizter]

@jdchristensen For this to be considered finished, I need to hook up our previous scripts such as timing etc. to also work in the Dune build layout. I also need to update our documentation so that people can easily get their editors to work with this setup. Should be simple enough.

For the record, we have been continuously testing this branch of HoTT in https://github.com/ejgallego/coq-universe, which is a monorepo of various Coq Dune projects that can all be built together.

We also have a restriction on the version of Dune we are using because HoTT will be tested in Coq's CI. So I will have to check there if we feel like merging.

[Alizter]

I'm going to close this PR in favour of #1687.