Skip to content

Minutes 2024 11 27

Jump to bottom Edit New page
Kazuhiko Sakaguchi edited this page Nov 27, 2024 · 2 revisions

2024-11-27 meeting:

  • Chair: Cyril (leading the meeting, to be decided at each meeting for the next one, should send the reminder / cancel if no topics)
  • Secretary: Cyril (taking notes, can be decided at the beginning of the meeting)

Topics queue:

  • News from the next release.
    • Pierre merged a few PRS, and Cyril and Laurent planned to release tomorrow.
  • github rights / teams ( https://github.com/orgs/math-comp/teams )
    • Read minutes and take action
  • Future of #1125, #1169 and #1256
    • these 3 PRs had heavy performance issues: semi-module +100%, algebra +20%, preorder +20%
      • semi-module has a workaround with only +4%
    • solved in Coq with a PR merged 3 weeks ago by Quentin:
      • mathcomp -8%
      • semi-module +4%, algebra +17%, preorder +6%
    • what do we do? Plan:
      • add all PR with workaround for semi-module
      • Remove the workaround for the Rocq prover 9.1
  • Feedback on experiments with category for multivariate polynomials
    • Meeting last afternoon,
    • Consensus: dump category.v into multinomials as an ad-hoc dev (without making a general) an and live with it for the time being.
    • Required extensions of HB:
      • automated support of forgetful functors
      • automated support of full subcategories
      • change of subject for naturality
      • have setoid rewrite (modulo A) work fine with HB (in category.v is using =1 under \o and under functor application).
    • Working group with Florent in Lyon early 2025
  • Best name for non-trivial rings
    • ntRing, nontrivRing, nonzeroRing, nontrivalRing -> nzRing
    • the order of stuff, is it a prefix, as in nzComRing etc
    • nontrival rings are useful for the degree of X, and in computer algebra, for the rest of math we prefer possibly trivial rings
    • Requires: new feature of HB to deprecate structures (math-comp/hierarchy-builder#436)
    • Unsolved: up to where goes the nontriviality? zero field (probably not), zero unitring ? zero integral domain?
  • Dependent eq_fun
    • =1 is for nondep functions, should we generalize to dependent functions?
    • Cyril remembers the generalization to be non trivial, but we should try again and see.
Add a custom footer

Clone this wiki locally