Stream: coq-community devs & users

Topic: Apery PR

Karl Palmskog (Apr 25 2022 at 11:48):

@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

Assia Mahboubi (Apr 25 2022 at 11:58):

Thanks for the ping @Karl Palmskog !

Karl Palmskog (Apr 25 2022 at 12:01):

sidenote to Théo: we might want to design some query to find "stuck" PRs in coq-community and run it now and then

Théo Zimmermann (Apr 25 2022 at 12:29):

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

Kazuhiko Sakaguchi (Apr 25 2022 at 14:47):

Thanks @Karl Palmskog !

Kazuhiko Sakaguchi (Apr 25 2022 at 14:50):

@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

Assia Mahboubi (Apr 25 2022 at 14:52):

Thanks for the heads up @Kazuhiko Sakaguchi , but I need a bit more time to approve that one.

Assia Mahboubi (Apr 25 2022 at 14:53):

In particular I would like to understand better the performance issue (before eventually merging)

Assia Mahboubi (Apr 25 2022 at 14:54):

And I might have time for this only by the end of the week, sorry.

Kazuhiko Sakaguchi (Apr 25 2022 at 15:01):

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.

Karl Palmskog (Apr 26 2022 at 06:57):

@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)

Kazuhiko Sakaguchi (Apr 26 2022 at 07:02):

@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.

Karl Palmskog (Apr 26 2022 at 07:05):

in this case, you could do two tags, one of which becomes a release

Karl Palmskog (Apr 26 2022 at 07:06):

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 (May 03 2022 at 19:50):

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.

Karl Palmskog (May 04 2022 at 06:41):

@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.

Assia Mahboubi (May 05 2022 at 07:32):

Again, I am ok with releasing now. Sure, please proceed as soon as you have time to do so! Thanks a lot!

Karl Palmskog (May 05 2022 at 07:49):

release done, will be installable via opam very soon: https://github.com/coq/opam-coq-archive/pull/2175

Last updated: Jun 03 2023 at 18:01 UTC