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
It would be nice if bugs come with an issue number
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.
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
Not a problem that I can see
Dune build language is versioned so barrying bugs, it is quite stable
please also consider submitting bonak to the opam archive in some form (e.g.,
@Karl Palmskog Okay, I’ll look into it, although I’m not sure if it’s reusable as a lib.
if it is in opam we can run benchmarks on it, for example
@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.
And since you have a dune setup, you should be able to generate them if you want
Done. See https://github.com/ocaml/opam-repository/pull/21648
@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
if I'm not mistaken, Coq benching is done on git-based opam packages (which are not allowed in the regular OCaml opam repo)
Last updated: Feb 06 2023 at 20:02 UTC