Gaëtan Gilbert (Jun 22 2022 at 20:53): 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
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 came with an issue number
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.
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
Emilio Jesús Gallego Arias (Jun 23 2022 at 09:49):Not a problem that I can see
Emilio Jesús Gallego Arias (Jun 23 2022 at 09:49):Dune build language is versioned so barrying bugs, it is quite stable
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)
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.
Enrico Tassi (Jun 23 2022 at 11:07):if it is in opam we can run benchmarks on it, for example
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.
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
Ramkumar Ramachandra (Jun 24 2022 at 18:38):Done. See https://github.com/ocaml/opam-repository/pull/21648
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
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)
Ramkumar Ramachandra (Jun 24 2022 at 18:59):Done. https://github.com/coq/opam-coq-archive/pull/2209
Last updated: Jun 05 2023 at 10:01 UTC