@Assia Mahboubi any chance of a review+merge for this PR? It looks like a straightforward maintenance PR to me: https://github.com/coq-community/apery/pull/11
Thanks for the ping @Karl Palmskog !
sidenote to Théo: we might want to design some query to find "stuck" PRs in coq-community and run it now and then
Similarly to our list of issues with "help wanted" tag, this should be doable with a GitHub search. Something like: https://github.com/pulls?q=is%3Aopen+is%3Apr+archived%3Afalse+user%3Acoq-community+sort%3Aupdated-asc
Thanks @Karl Palmskog !
@Assia Mahboubi FYI, this PR (the replacement of lia_tactics
and field_tactics
with mczify and Algebra Tactics) is also ready. https://github.com/coq-community/apery/pull/4
Thanks for the heads up @Kazuhiko Sakaguchi , but I need a bit more time to approve that one.
In particular I would like to understand better the performance issue (before eventually merging)
And I might have time for this only by the end of the week, sorry.
Sure. Since I'm preparing an artifact including Algebra Tactics, Apery, and the instruction for benchmarking, this one should not necessarily be merged before the camera-ready deadline. So, no problem.
@Kazuhiko Sakaguchi if possible, please coordinate with Assia to make a tag/release for the artifact (and have it live in the Coq opam archive)
@Karl Palmskog Then, the problem is that the paper contains a performance comparison of two versions of Apery (with and without Algebra Tactics). I'm not sure if making two releases of Apery for this reason is a good practice.
in this case, you could do two tags, one of which becomes a release
it's valuable for the community to have a record in the actual repo of the code used in a paper, but not necessary to put everything on the opam archive. I still think the tactic improvements (without performance stuff) warrant a release (e.g., version 1.0.2 or 1.1.0)
Assia Mahboubi said:
And I might have time for this only by the end of the week, sorry.
Late but done. @Karl Palmskog @Kazuhiko Sakaguchi what is the suggestion in the end? I am fine with releasing the current state of the code. The work by Kazuhiko on algebra-tactics is a quite good occasion for this I would say.
@Assia Mahboubi I'd recommend doing a regular release now, and Kazuhiko can decide later on preserving the scientific artifact with performance measures. If you want, I can do release 1.0.2 on GitHub for current master
branch and submit the opam package to the archive.
Again, I am ok with releasing now. Sure, please proceed as soon as you have time to do so! Thanks a lot!
release done, will be installable via opam very soon: https://github.com/coq/opam-coq-archive/pull/2175
Last updated: Nov 29 2023 at 19:01 UTC