Submitting the project to Coq's CI

[palmskog]

I would like to try to apply this project in some program verification work. However, since the project has OCaml code, this becomes a risky proposition due to the ever-changing ML API of Coq. Specifically, if I depend on this project, my project could get stuck on an old Coq version.

How about submitting the project to Coq's CI to receive updates as the ML API evolves? The Coq core team encourages this for plugins that are likely to be generally useful, like this one.

Here is a typical PR adding a plugin to Coq's CI that could be used as a template. If given a green light, I could also handle the Coq PR with CI boilerplate.

[damien-pous]

Hi @palmskog, Sure, that's a good idea indeed. I'll have a closer look next week ; the thing is I evolved the library substantially since last version, I should probably first package a new version, and only then put it on Coq's CI? Damien

[palmskog]

@damien-pous do you mean you have changes to the code here outside of GitHub in some private repository, and you plan to push this code to GitHub in the near future?

If not, then it's fine to add the repository to Coq's CI as soon as the master branch is compatible with Coq's master. Integration into Coq's CI is (to me at least) unconnected to any GitHub releases or tags. But there may be work involved in the port to Coq master, which I may be able to help with.

Being in Coq's CI does, however, make it possible to quickly do a release/tag for new stable Coq version, because there is always some commit in the Git history that works with the just-released version of Coq for a CI project.

[damien-pous]

Hi @palmskog, No, everything is on this repo, on the master branch. I'm going to check whether it still compiles with Coq master (i.e., coq.dev in opam ?)

[palmskog]

Right, if it builds with coq.dev (in the Coq opam core-dev repository), then it can be submitted to CI.

Let me know if you run into some hard-to-solve issue with porting to coq.dev, we recently went through the porting exercise to coq.dev with ATBR, so there may be analoguous problems.

[damien-pous]

Ok, so now the master branch compiles with coq.dev (from opam core-dev). If you can handle the Coq PR with CI boilerplate that would be great!

[palmskog]

@damien-pous I submitted the PR as coq/coq#17851, but usually the Coq maintainers would like there to be some basic CI in the repo itself, so they can easily see if a change they submit is backwards-compatible. Do you mind if I do a PR to this repo with some simple CI based on Docker-Coq-Action?

[damien-pous]

Sure, please go ahead!

[palmskog]

Closing this since the Coq CI PR was merged 🎉