Coq Call 2022 02 09
- February 09, 2022, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- Status of the
mind_finitefield of inductive types (reflect the keyword use at definition time or tell if the type is really non-recursive, independently of the keyword) see e.g. #8226 [HH] - Unifying the name of functions for destructing sequences of lambda/prod and letins (#15582) [HH]
- Satisfied with intermediate status of parametricity-based implementation of Boolean equality (#15527)?
- Need an assignee for https://github.com/coq/coq/pull/15549 (Ali)
- Display git hash in non-release versions: https://github.com/coq/coq/pull/15639 (Ali)
- Pros: Easy to copy and paste for users of
opam masteretc. Makes debugging "version master" from ancient issues easier. Everybody else does it. - Cons: Not clear how to make reproducible. Depends on git. Messes up build order.
- Pros: Easy to copy and paste for users of
- If Emilio is present, what to do about https://github.com/coq/coq/pull/15645 (Ali)
- Making Ltac2 independent (Ali)
- Would be nice for HoTT to use the Ltac2 library without any of the stdlib.
- Hackathon: (Ali)
- We have some more requested sessions, any takers? https://github.com/coq/coq/wiki/CoqWG-2022-02#requested
- [mind_finite] Decision to have the flag reflect the actual recursivity but keeping compatibility as much as possible.
- PR 15582: let's continue uniformizing the names
- https://github.com/coq/coq/pull/15527: would need more manpower to go beyond, but a good first step.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.