Stream: Coq devs & plugin devs

Topic: Makefile.build?


view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Nov 24 2021 at 17:58):

native

view this post on Zulip Enrico Tassi (Nov 24 2021 at 19:29):

Is it an haiku?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Nov 25 2021 at 13:46):

For example the manual seems to be built by that makefile

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Nov 25 2021 at 14:20):

I agree it's not important, but it is supported as of today, right?

view this post on Zulip 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: Feb 01 2023 at 16:03 UTC