Stream: Coq devs & plugin devs

Topic: adding Stalmarck to Coq CI

Karl Palmskog (Oct 30 2021 at 14:18):

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

• a Coq library
• a Coq plugin which uses code extracted code from the Coq library
• a standalone OCaml-based tool which uses extracted code from the Coq library

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.

• Is this possible with only a Dune build?
• Is there any example other project in the CI that resembles this I could use as a template for the CI build scripts?

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

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

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

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: Oct 13 2024 at 01:02 UTC