Join the meeting

October 16th, 10h-13h (Europe/Paris). visio.inria.fr 304#4680

Agenda

• 10h (15', including connexion issues) : Meetings frequency + next live. (assia)
• 10h15 (20') : Status of finmap (PYS)
  • status of the PR related to inf-semi-lattices
  • needs for sub-lattices / lattice morphisms
• 10h35 (15') : roadmap for multinomials (PYS)
• 10h50 (10') : Merging coq-void (assia)?

Remaining items :

• Summary of PR270 : dispatching order and norm.
  • can we merge by the end of the month?
• News from Portland
• Installation instructions
• Documentation for naming conventions of structures and modules (where to put caps?)
• PR378: Reorder the arguments in compare_nat and ltngtP
  • This is a compatibility breaking change. So we probably should have more discussion before merging.

Notes

• PYS: I have to leave at 11am.
• assia: I have to leave at 11am.

Minutes

Decision: we meet every 2 thursdays from 10 to 11 to stay up to date, next is 31st

PYS declares he will be working on multinomials in November, starting from a release of what we have. Private chat with Cyril to synchronize for the future

PYS asks why PR #388 (non distributive lattice) is not on the math-comp/finmap repository?

• Cyril: this is a PR over a PR, since the old repo of finmap is frozen
• PYS: needs more distributive stuff and would like to have this now

Discussion about about #270 (dispatching order and norm)

• Assia: review is hard, changes large, motivations are unclear
• Kazuhiko: reply on the PR with some motivations and technical issues that should be solved by the PR
• Reynald: says he is using this PR for MC analysis and it works for him
• Assia explains that the lack of doc (e.g. unclear or misleading file headers, no migration instructions, what are the new intended features, HOWTO take advantage of them) and communication with the PR authors made it harder to review, more frequent meetings can surely help
• Maxime gives his perspective: description of the PR is quite low level, hard to distil from it the piece of info Assia is looking for. It makes sense for PR authors and reviewers to meet/skype with the sole purpose of working on the PR (it is a way to allocate a time slot shared among all parties involved)

Coq-void: Enrico thinks we should merge it, it is vacuously OK (and useful). But there is no PR for it, and we should ask Arthur. Enrico does it: https://github.com/arthuraa/coq-void/issues/1

We postpone "news from Portland".

We postpone "Installation instructions", little news is that there are now some instructions for Windows.

PR #361 (fixing the duplicate website), Maxime can merge/fix. Doing it now.

There is duplication between wiki and website about papers using SSR/MC, and they are outdated. Enrico: can't we use google for that? Not clear t works fine. Reynald will elects the official list and keeps it updated until July and advertise it on SSR mailing list.