Minutes July 27 2022 - math-comp/math-comp GitHub Wiki
- math-comp port completed (besides the doc)
- wait to complete the port of mathcomp-analysis to be sure
- HB.about useful but does not list up all the factories
- we want to know the set of factories that could help instantiate a structure
but not the ones that are already instantiated
- it does not look too difficult to implement but a concrete issue would make the work easier
- Enrico worrying about reported locations
- doc?
- insert a pointer to HB's doc or wiki to know how to instantiate a structure
- maybe better to have the factories in the documentation
- HB.about was originally here for the doc
- think of directives from the header that would trigger Coq type-checking to populate the documentation
- perf? no big issue with mathcomp-analysis so far, haven't touched
measure.v yet though
- TODO: release of HB for compatibility with 8.16
- mathcomp/HB tutorial for this summer?