Stream: math-comp devs

Topic: MathComp HB documentation spring sprint


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Apr 11 2023 at 08:27):

ah OK, I guess Pierre already has Coq-community covered then

view this post on Zulip Karl Palmskog (Apr 11 2023 at 08:27):

https://github.com/coq-community/comp-dec-modal might be interesting?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Apr 11 2023 at 09:12):

Thank you!

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Apr 11 2023 at 09:19):

@all this topic is of general interest.

view this post on Zulip 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

view this post on Zulip 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: Jul 23 2024 at 17:01 UTC