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.
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
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
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
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: Dec 07 2023 at 09:01 UTC