Stream: Coq devs & plugin devs

Topic: add bonak to CI?


view this post on Zulip Gaëtan Gilbert (Jun 22 2022 at 20:53):

https://github.com/artagnon/bonak
AFAIK the devs we have in CI don't use SProp, it would be nice to have something testing it, this seems a nice candidate
cc @Hugo Herbelin @Ramkumar Ramachandra

view this post on Zulip Enrico Tassi (Jun 23 2022 at 05:46):

https://github.com/artagnon/bonak/blob/86655deecfd19e097d33902bc3bd991a0682845a/theories/NType/Yoneda.v#L63
It would be nice if bugs come with an issue number

view this post on Zulip Ramkumar Ramachandra (Jun 23 2022 at 08:39):

Ah yes. Perhaps worth noting that bonak breaks subtly on older versions of Coq; I found an SProp-unrelated bug in dev (which Hugo fixed, thankfully before the release) too. Yes, i think it’s a good testing candidate.

Currently, the dune-project and Actions CI are running on every push to master.

But yes, I agree that we’ve not been keeping track of issues too well.

view this post on Zulip Gaëtan Gilbert (Jun 23 2022 at 09:31):

I didn't notice that it's full dune, not coq_makefile
we don't have other projects like that in CI I think
not sure if it's a problem
cc @Emilio Jesús Gallego Arias

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 09:49):

Not a problem that I can see

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 09:49):

Dune build language is versioned so barrying bugs, it is quite stable

view this post on Zulip Karl Palmskog (Jun 23 2022 at 09:52):

please also consider submitting bonak to the opam archive in some form (e.g., extra-dev as coq-bonak.dev package)

view this post on Zulip Ramkumar Ramachandra (Jun 23 2022 at 10:30):

@Karl Palmskog Okay, I’ll look into it, although I’m not sure if it’s reusable as a lib.

view this post on Zulip Enrico Tassi (Jun 23 2022 at 11:07):

if it is in opam we can run benchmarks on it, for example

view this post on Zulip Karl Palmskog (Jun 23 2022 at 11:15):

@Ramkumar Ramachandra let me know if you need help to create a dev opam package. Most of the time, it suffices to take the in-repo opam package and add a pointer to the GitHub URL.

view this post on Zulip Ali Caglayan (Jun 23 2022 at 11:38):

And since you have a dune setup, you should be able to generate them if you want

view this post on Zulip Ramkumar Ramachandra (Jun 24 2022 at 18:38):

Done. See https://github.com/ocaml/opam-repository/pull/21648

view this post on Zulip Karl Palmskog (Jun 24 2022 at 18:48):

@Ramkumar Ramachandra it's nice that you have done a release, but I would still recommend having the package in the Coq specific opam repository: https://github.com/coq/opam-coq-archive

The difference is that we allow git-based opam packages in the extra-dev part, for example: https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-aac-tactics/coq-aac-tactics.dev/opam

We also test several versions of Coq on each package, and we do continuous testing of already-added packages, see here

view this post on Zulip Karl Palmskog (Jun 24 2022 at 18:50):

if I'm not mistaken, Coq benching is done on git-based opam packages (which are not allowed in the regular OCaml opam repo)

view this post on Zulip Ramkumar Ramachandra (Jun 24 2022 at 18:59):

Done. https://github.com/coq/opam-coq-archive/pull/2209


Last updated: Feb 06 2023 at 20:02 UTC