Stream: math-comp users

Topic: Templates for Apery


view this post on Zulip Karl Palmskog (Jan 12 2022 at 11:24):

@Assia Mahboubi please see https://github.com/math-comp/apery/pull/5 for some boilerplate improvements to Apery. (This is an example of the kind of PR I could take care of autonomously, with your permission)

view this post on Zulip Assia Mahboubi (Jan 12 2022 at 12:25):

@Karl Palmskog Many thanks! And thanks as well for this message, which drew my attention to your kind PR.

view this post on Zulip Assia Mahboubi (Jan 12 2022 at 12:26):

Indeed, I should and will release and create the corresponding opam package asap.

view this post on Zulip Assia Mahboubi (Feb 02 2022 at 09:03):

Follow-up: In the end, after the last MC dev meeting, we decided to move this project to coq-community. Apery will in particular serve as a guinea ping for possibly moving the other projects currently under the mathcomp organisation.

view this post on Zulip Karl Palmskog (Feb 02 2022 at 09:09):

@Assia Mahboubi here is the link to begin to move a project to coq-community: https://github.com/coq-community/manifesto/issues/new?assignees=&labels=move-project&template=1-move-a-project.md&title=Proposal+to+move+project+Apery+to+coq-community

Let me know if anything is unclear.

view this post on Zulip Karl Palmskog (Feb 02 2022 at 09:13):

here's an example of a project that was moved: https://github.com/coq-community/manifesto/issues/136

We'd normally like all authors/copyright holders to approve of a move, but they don't have to approve directly on GitHub, e.g., it's fine to just send them an email and write in the GitHub issue when you hear back.

view this post on Zulip Assia Mahboubi (Feb 02 2022 at 09:18):

Thanks @Karl Palmskog ! I will create the issue and continue the discussion there (if needed).

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:07):

@Assia Mahboubi I think things look good in https://github.com/coq-community/apery/pull/8 - so I'll merge in the next hour unless you have concerns. After that, I recommend deleting the old tag and making a new release from scratch on GitHub (which will recreate the tag)

view this post on Zulip Assia Mahboubi (Feb 03 2022 at 12:13):

Please proceed, many thanks!

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:14):

OK, then I do the release as well while I'm at it...

view this post on Zulip Assia Mahboubi (Feb 03 2022 at 12:15):

By "the old tag" are you refering to the one from March 20? This one was for the submission of a companion paper. But it is not of the highest importance I would say.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:15):

ah OK, if you want to keep that tag, we could just do a release called 1.0.1

view this post on Zulip Assia Mahboubi (Feb 03 2022 at 12:15):

Perfect.

view this post on Zulip Assia Mahboubi (Feb 03 2022 at 12:17):

Please proceed with the release if you wish. Or I will do it later on.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:18):

I'll do it quickly once CI finishes. You can edit release text later if you want. My main goal is just to get the opam package into the archive. MathComp tends to be so stable a release can last for 1+ year.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:42):

@Kazuhiko Sakaguchi do you want to join coq-community so you can merge https://github.com/coq-community/apery/pull/4 yourself when it is ready?

view this post on Zulip Kazuhiko Sakaguchi (Feb 03 2022 at 12:56):

@Karl Palmskog Yes, but that PR will not be merged very soon. The story behind the PR is that I use it as a benchmark in a draft paper about Algebra Tactics. So I think it will be merged when the final version of the paper is ready.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:57):

OK, sounds good, but I was indeed thinking about the long, long term here.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:59):

our general philosophy is that our community is small and manpower is scarce, so people interested in a project should be empowered to do basic tasks, and we will assume they synchronize with maintainers at appropriate intervals.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:00):

nevertheless, maintainers can choose to be more strict about repo privileges if they wish

view this post on Zulip Assia Mahboubi (Feb 03 2022 at 13:01):

Regarding this repo at least, I think that the general philosophy you describe is very (wise and) relevant.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:02):

I personally also like to keep PRs as repo branches, rather than in forks, since more in community spirit and sometimes easier to pass PRs between people

view this post on Zulip Assia Mahboubi (Feb 03 2022 at 13:02):

Indeed, fine with me.

view this post on Zulip Théo Zimmermann (Feb 03 2022 at 13:04):

Karl Palmskog said:

I personally also like to keep PRs as repo branches, rather than in forks, since more in community spirit and sometimes easier to pass PRs between people

Yeah, this is a good strategy as long as the number of open PRs is small.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:05):

also quick check @Théo Zimmermann if we could set up up GitLab repo mirroring for Apery

view this post on Zulip Karl Palmskog (Feb 04 2022 at 10:27):

@Assia Mahboubi don't forget Kazuhiko's refactoring PR: https://github.com/coq-community/apery/pull/9

It looks good to me, and also does a nice small fix to CI


Last updated: Feb 08 2023 at 07:02 UTC