Stream: Coq devs & plugin devs

Topic: adding Stalmarck to Coq CI


view this post on Zulip Karl Palmskog (Oct 30 2021 at 14:18):

I maintain the Stalmarck project in Coq community, which consists of:

The only way I could have this be maintainable was to use Dune to build everything. The regular make build still works but builds only the Coq library.

The plugin uses only a very small part of the ML API that seems to quite stable, but I'd still like to include the project into the Coq CI to ensure compatibility for the long term.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 01 2021 at 22:30):

I don't see a problem at all @Karl Palmskog , in fact it is much better when plugins include a dune file as we can create overlays and use incremental compilation

view this post on Zulip Emilio Jesús Gallego Arias (Nov 01 2021 at 22:30):

I don't think anything special is needed for the template, just replace make with the right build instructions for your plugin; I guess if something extra is needed we will learn on the way

view this post on Zulip Emilio Jesús Gallego Arias (Nov 01 2021 at 22:31):

I think we usually require that the CI targets do produce installable stuff so other parts on the CI can depend on that, but we will likely modify this once we can setup an incremental CI fully

view this post on Zulip Théo Zimmermann (Nov 02 2021 at 08:58):

I think we usually require that the CI targets do produce installable stuff so other parts on the CI can depend on that

And that's not even a strict requirement if the project has no reverse dependencies...


Last updated: Feb 02 2023 at 13:03 UTC