Minutes 2024 09 18 - math-comp/math-comp GitHub Wiki

  • Chair: Cyril (leading the meeting, to be decided at each meeting for the next one, should send the reminder / cancel if no topics)
  • Secretary: Quentin (taking notes, can be decided at the beginning of the meeting)
  • Participants: Reynald Affeldt, Cyril Cohen, Thomas Lamiaux, Pierre Roux, Kazuhiko Sakaguchi, Quentin Vermande

Practical documentation for Coq (i.e. tutorials)

  • On the Coq platform (easy to find (centralized), updates (easy to make a PR)), accessible interactively online with JsCoq. A few tutorials exist, doc on Equations in progress. They would start developping the doc for every feature/project: make a reviewer team of people in charge of writing and maintaining documentation, respecting some standard (e.g. pedagogy). Maintaining is not expected to be too much work, as ssreflect does not evolve much.
  • There exists MC and ssreflect tutorials, easy to port. Not exactly light, a lot of work.
  • 2 things to do: writing and organizing. Organizing is for the reviewer team to do, should be discussed with the users, e.g. via issues. With respect to writing, it is more about reviewing than anything.
  • A project could be created with the people interested, to gather interested people and issues.
  • The book should be mostly up to date.
  • Writing takes a lot of time, but deciding what you want to do and reviewing does not.
  • Kazuhiko worried about tutorials getting outdated, e.g. the header documentation of ssralg.
  • That means the tutorial should be in the CI.
  • This is not the case yet because it is a new project, should be done in the near future. It was not an issue for Equations since the plugins basically does not change.
  • Kazuhiko's point is that the explanations should be updated and those can not be checked with the CI. We should add commands that would draw our attention to things we should change in the explanation. It should be built so that things that are prone to evolving have Coq code corresponding to the explanation and should be in the CI (sufficiently high, maybe even in Nix packages so that it is a reverse dependency of MC).
  • It could be added in the documentation that some explanations are specific to some version and might break in the future.
  • Cyril worries that JsCoq has no maintainer, what is its future?
  • There will be a JsCoq2 soon to be released. No good solution yet, but the community needs something like that. There will be a fork of the ocaml website for coq.
  • Cyril, Kazuhiko, Pierre and Quentin agree to be volunteer to the team.
  • Thomas proposes two projects, one for ssreflect and one for MC.
  • They are intimately tied. It is fine to have one project, we can make two later if needed.

Release

  • This is about finding a volunteer, ideally Laurent with someone else. Only about MC2. ~2 to 3 hours of work.
  • Cyril volunteers (it does not look too bad).
  • 8.20.0 is out, we can drop 8.18 after this release.

PR#1125 looking for reviewers

  • Kazuhiko wants to remove the new parameters of SemiLinear ((S : semiRingType) (f : {rmorphism R -> S}))? If $f$ is not idfun, you can just use the composition of $f$ and $s$ as the scaling morphism.
  • Cyril thinks it is ok.
  • It can still be reverted if needed.
  • Kazuhiko generalized some more results

Performance issue of PR#1125

  • Kazuhiko replaced isLinear by isSemiLinear. The unification trace shows nmodType in front of zmodType triggering CS instanciation, triggering a recursive CS instanciation. The zmodType comes from the isLinear factory, using the mixin solves the issue.
  • Cyril asks for a branch without this workaround.
  • Still 4% slowdown, rewrite linearB and linearN sometimes are very slow. This is acceptable. Kazuhiko will investigate potential failing unifications with linearB and linearN.
  • Users are supposed to use them as much as possible. The issue should be fixed before merging. Probably combination of how HB is packaging things and how unification works.
  • We are you purposefully avoiding linearB and linearN?
  • We should not teach users to workaround this kind of problem. Documentation is not enough.
  • Reynald asks whether there is a way to have no semi-structure for people who do not need them and have them for people who need them.
  • Cyril sees only two options: factories that hide them (what Kazuhiko does) and forking MC. The performance issue is not accidental and will come up as we extend the hierarchy.
  • This issue already came up when doing matrices in CoqRobot. The reason may not be HB.
  • Kazuhiko found two issues: failing selection of subterms and unification super slow. If this hypothesis is right, that would be the same perf issue on linearD, fixed by avoiding the use of factories for linear functions.
  • Maybe we should make sure HB does not introduce too many intermediate definitions when producing instances.
  • The factory uses a sub-structure as one of the parameter w.r.t. the corresponding parameter of the mixin.
  • Laurent reported a similar kind of issue where instance building could simplify.
  • Maybe worth a specific meeting to investigate. Maybe the next MC sharing days

Morphism joins in MC#1256

Postponed.