Reynald Affeldt (Apr 30 2021 at 02:54): 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
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
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.
Reynald Affeldt (May 04 2021 at 08:13):You say “others”, I’m sure it is “everyone”. :-)
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?
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)
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).
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.
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.
Assia Mahboubi (May 04 2021 at 08:48):In the spirit of what Laurent did some years ago.
Cyril Cohen (May 04 2021 at 08:49):I am eager to learn more about this tomorrow then :)
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.
Enrico Tassi (Jan 04 2022 at 16:57):you are welcome to join, just add the topics to the wiki
Enrico Tassi (Jan 04 2022 at 16:57):https://github.com/math-comp/math-comp/wiki/TopicsNextMeeting
Enrico Tassi (Jan 04 2022 at 16:58):(not sure I'll be there)
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?
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
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
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.
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:
Christian Doczkal (Jan 12 2022 at 08:30):In any event, it's unambiguous.
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)
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: Oct 13 2024 at 01:02 UTC
