Stream: math-comp devs

Topic: Fortnightly meetings


view this post on Zulip Reynald Affeldt (Apr 30 2021 at 02:54):

Dear math-comp devs subscribers, you can fuel next week's meeting with topics using the wiki: https://github.com/math-comp/math-comp/wiki/TopicsNextMeeting

view this post on Zulip Reynald Affeldt (May 04 2021 at 08:08):

As of now, the agenda for tomorrow’s meeting could be (1) quickly going through last time’s TODOs to check progress and (2) trying to make progress on a few selected PRs

view this post on Zulip Kazuhiko Sakaguchi (May 04 2021 at 08:11):

I can do a short demo of my ring tactic for ssralg (implemented in Coq-Elpi) if others are interested in it.

view this post on Zulip Reynald Affeldt (May 04 2021 at 08:13):

You say “others”, I’m sure it is “everyone”. :-)

view this post on Zulip Cyril Cohen (May 04 2021 at 08:18):

@Kazuhiko Sakaguchi I had no clue you were doing this... Are you aware of this: https://hal.inria.fr/hal-01414881/document?

view this post on Zulip Cyril Cohen (May 04 2021 at 08:19):

I meant to revive this at some point next year with refinements done in elpi (with a PhD student)

view this post on Zulip Kazuhiko Sakaguchi (May 04 2021 at 08:24):

@Cyril Cohen I didn't know that. In short, my work currently reuses internals of the ring tactic of Coq, but its reification uses keyed matching rather than syntactic matching, and it is quite efficient to reify a large goal (approx. 1000 lines in the goal buffer).

view this post on Zulip Assia Mahboubi (May 04 2021 at 08:46):

@Cyril Cohen I am aware of both your previous work with Damien and of @Kazuhiko Sakaguchi experiments. Our recent discussions with Kazuhiko were mostly about 1) bringing (at least a core) ring to mathcomp 2) making reification more efficient. Although there is a much larger agenda, which is that of our PhD project for Chris.

view this post on Zulip Assia Mahboubi (May 04 2021 at 08:48):

The example Kazuhiko is talking about is a simplified instance of polynomials Sander Dahmen sent me a wile ago, in the context of a computational proof of the properties of group law for elliptic curves.

view this post on Zulip Assia Mahboubi (May 04 2021 at 08:48):

In the spirit of what Laurent did some years ago.

view this post on Zulip Cyril Cohen (May 04 2021 at 08:49):

I am eager to learn more about this tomorrow then :)

view this post on Zulip Karl Palmskog (Jan 04 2022 at 16:14):

Christian suggested I should join the next MathComp meeting to discuss coordination for release processes and the like for MC-related projects (and how they tie in to the opam repo, the Coq Platform, Docker images, etc.).

If MC people don't mind, we could also discuss briefly further synergies between MC and coq-community, such as our plans for next-generation templates that should support the math-comp repo.

view this post on Zulip Enrico Tassi (Jan 04 2022 at 16:57):

you are welcome to join, just add the topics to the wiki

view this post on Zulip Enrico Tassi (Jan 04 2022 at 16:57):

https://github.com/math-comp/math-comp/wiki/TopicsNextMeeting

view this post on Zulip Enrico Tassi (Jan 04 2022 at 16:58):

(not sure I'll be there)

view this post on Zulip Reynald Affeldt (Jan 05 2022 at 02:54):

I have added the recent issue by Theo to the list of topics. It is the same topic, right?

view this post on Zulip Karl Palmskog (Jan 05 2022 at 07:50):

yes, basically the same, modulo that Théo and I have slightly different views/opinions on the topic

view this post on Zulip Karl Palmskog (Jan 05 2022 at 11:19):

if anyone is into that kind of stuff, I did a tentative ER diagram of a Coq project, possibly useful as a basis for new templates: https://raw.githubusercontent.com/coq-community/templates/v2/Coqtemplate.svg

view this post on Zulip Karl Palmskog (Jan 12 2022 at 08:19):

I'm surprised that "fortnightly" is used for a project primarily based in France (as opposed to "bi-weekly"). "Fortnightly" is as American as it gets.

view this post on Zulip Christian Doczkal (Jan 12 2022 at 08:29):

I discussed this with @Cyril Cohen - who made this decision - and the point was that bi-weekly is ambiguous: it can mean either twice per week or every two weeks. Wikipedia says that fortnight derives from Old English and is rarely used in North America. :shrug:

view this post on Zulip Christian Doczkal (Jan 12 2022 at 08:30):

In any event, it's unambiguous.

view this post on Zulip Karl Palmskog (Jan 12 2022 at 08:35):

unambiguous, sure, but not until you look it up in a dictionary (as non-native Old English speaker)

view this post on Zulip Enrico Tassi (Jan 12 2022 at 08:47):

eh eh, I did not know the meaning either... It must the be the ssr-inspired love for conciseness, since "it takes place once every two weeks" also works ;-)


Last updated: Aug 11 2022 at 03:02 UTC