Enrico Tassi (Nov 23 2021 at 15:05): Enrico Tassi (Nov 23 2021 at 15:05):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...
Emilio Jesús Gallego Arias (Nov 24 2021 at 15:25):Not sure what do you mean @Enrico Tassi , this file has been there for a long time
Emilio Jesús Gallego Arias (Nov 24 2021 at 15:26):It could be replaced by coq_makefile as I showed in a prototype PR, that's true
Enrico Tassi (Nov 24 2021 at 17:55):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?
Gaëtan Gilbert (Nov 24 2021 at 17:58):native
Enrico Tassi (Nov 24 2021 at 19:29):Is it an haiku?
Enrico Tassi (Nov 24 2021 at 19:30):can you explain a bit better what breaks? also this bunch of makefiles are not just about native, AFAICT
Gaëtan Gilbert (Nov 24 2021 at 19:34):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
Théo Zimmermann (Nov 25 2021 at 09:19):It seems like Gaëtan and Emilio are answering about the legacy / hybrid build system in general, but maybe Enrico was asking specifically about Makefile.build, not Makefile.make / Makefile.vo.
Enrico Tassi (Nov 25 2021 at 10:33):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)
Enrico Tassi (Nov 25 2021 at 13:46):For example the manual seems to be built by that makefile
Théo Zimmermann (Nov 25 2021 at 13:47):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.
Théo Zimmermann (Nov 25 2021 at 13:48):The manual can be built by both build systems but can only be installed by the legacy one.
Gaëtan Gilbert (Nov 25 2021 at 14:05):Another one was the vio / vos / vok stuff.
that's not important for the stdlib build though, just coq_makefile
Théo Zimmermann (Nov 25 2021 at 14:20):I agree it's not important, but it is supported as of today, right?
Gaëtan Gilbert (Nov 25 2021 at 14:28):who knows
the point is that it's not a reason to keep makefile.build
Last updated: Dec 07 2023 at 17:01 UTC