Pierre Roux (Mar 29 2023 at 08:28): Pierre Roux (Mar 29 2023 at 08:28):Dear MathComp developers,
Following the success of the previous MathComp sprint week which
enabled the porting of the library to Hierarchy-Builder, it now just
remains to complete the documentation of the hierarchy of structures before
releasing MathComp 2. We plan to organize an online week-long sprint
to do so. Here is a poll to choose an appropriate period:
https://evento.renater.fr/survey/mathcomp-2-documentation-sprint-ck97yi5r
green/yes: I'm mostly available that week
orange/maybe: I'm only available one or a few days during that week
red/no: I'm mostly unavailable that week
Ideally, we'd like to take a decision on the date by April 6th.
Note that it is not strictly required to be fully available the whole
week, participating one or a few days can already be of great help.
Reynald and Pierre
Pierre Roux (Apr 11 2023 at 07:11):Dear @all , a kind reminder about the poll just above, we'd like to take a decision on the date tomorrow.
Karl Palmskog (Apr 11 2023 at 07:35):is there maybe some support available for MathComp-using project maintainers to port to HB? Or might that be provided only after the release of 2.0?
Reynald Affeldt (Apr 11 2023 at 08:24):You are maybe thinking of projects from coq-community. Do you have a project using MathComp in mind, that is not too big, and that we could maybe use as a tutorial example for porting?
Pierre Roux (Apr 11 2023 at 08:26):(developments already ported/tested in MathCOmp's CI: mathcomp-bigenough, deriving, extructures, coqeal, coquelicot, interval, reglang, fourcolor, gaia, graph-theory, coq-bits, mathcomp-classical, mathcomp-analysis, odd-order, mathcomp-finmap, mathcomp-real-closed, multinomials, mathcomp-zify, mathcomp-abel)
Karl Palmskog (Apr 11 2023 at 08:27):ah OK, I guess Pierre already has Coq-community covered then
Karl Palmskog (Apr 11 2023 at 08:27):https://github.com/coq-community/comp-dec-modal might be interesting?
Karl Palmskog (Apr 11 2023 at 08:29):I have been playing around with https://github.com/coq-community/regexp-Brzozowski/ but it's not in great shape (contains 2010-era MathComp idioms).
Karl Palmskog (Apr 11 2023 at 08:32):also, I have a personal stake in https://github.com/math-comp/tarjan and would like to help with HB there if I can
Reynald Affeldt (Apr 11 2023 at 09:12):Thank you!
Reynald Affeldt (Apr 11 2023 at 09:14):We will maybe try to do a "porting tutorial" using one of those to help porting other projects. comp-dec-modal looks like an appropriate example.
Cyril Cohen (Apr 11 2023 at 09:19):@all this topic is of general interest.
Pierre Roux (Apr 14 2023 at 15:11):Dear MathComp developers,
Considering answers to the poll, the next MathComp sprint will take
place from Wednesday May 3rd to Wednesday May 10th (a week, excluding
Monday 8th which is a french holiday). We will first meet on Wednesday
3rd at 10am UTC+2 (instead of our usual biweekly meeting).
Best regards,
Reynald and Pierre
Cyril Cohen (Apr 16 2023 at 18:32):Pierre Roux said:
Dear MathComp developers,
Considering answers to the poll, the next MathComp sprint will take
place from Wednesday May 3rd to Wednesday May 10th (a week, excluding
Monday 8th which is a french holiday). We will first meet on Wednesday
3rd at 10am UTC+2 (instead of our usual biweekly meeting).Best regards,
Reynald and Pierre
Unfortunately between the time I stated my preferences and now I had to add other appointments. :-/ Hence. I won't be available much on Wednesday 3rd and Thursday 4th... I am willing to spend 1h max on Wednesday for the kick-off meeting and I will be able to work remotely from the train on Thursday afternoon.
Last updated: Nov 29 2023 at 21:01 UTC