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
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
I can do a short demo of my
ring tactic for
ssralg (implemented in Coq-Elpi) if others are interested in it.
You say “others”, I’m sure it is “everyone”. :-)
@Kazuhiko Sakaguchi I had no clue you were doing this... Are you aware of this: https://hal.inria.fr/hal-01414881/document?
I meant to revive this at some point next year with refinements done in elpi (with a PhD student)
@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).
@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.
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.
In the spirit of what Laurent did some years ago.
I am eager to learn more about this tomorrow then :)
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
you are welcome to join, just add the topics to the wiki
(not sure I'll be there)
I have added the recent issue by Theo to the list of topics. It is the same topic, right?
yes, basically the same, modulo that Théo and I have slightly different views/opinions on the topic
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
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.
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:
In any event, it's unambiguous.
unambiguous, sure, but not until you look it up in a dictionary (as non-native Old English speaker)
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: Jun 01 2023 at 13:01 UTC