Why does this exist in the first place? It is not the old build system, but a piece of makefile which calls dune targets with hand written dependencies...
Not sure what do you mean @Enrico Tassi , this file has been there for a long time
It could be replaced by coq_makefile as I showed in a prototype PR, that's true
I don't get why we have it in its current form. It calls dune, so what is its purpose? Can't we just remove it?
Is it an haiku?
can you explain a bit better what breaks? also this bunch of makefiles are not just about native, AFAICT
dune can't build the native compute files IIRC
the bunch of makefiles provide a complete build, but the duplication with dune is only the .vo build and that's kept for native AFAIK
It seems like Gaëtan and Emilio are answering about the legacy / hybrid build system in general, but maybe Enrico was asking specifically about
My problem is that I had to fix dune files, then to discover that I also have to fix this other makefile, which calls "pieces" of dune.
In fact, I thought we had switched to dune, so I did not understand why we still had these makefiles around. I guess native explains why (even if these makefiles seem to have much more than just native stuff)
For example the manual seems to be built by that makefile
There are many reasons why we couldn't fully switch to Dune yet. One of them was indeed the native stuff. Another one was the vio / vos / vok stuff.
The manual can be built by both build systems but can only be installed by the legacy one.
Another one was the vio / vos / vok stuff.
that's not important for the stdlib build though, just coq_makefile
I agree it's not important, but it is supported as of today, right?
the point is that it's not a reason to keep makefile.build
Last updated: Feb 01 2023 at 16:03 UTC