General Organization

Please continue porting when you have the time, but always follow the process we used during the porting week, escpecially

• ticking/unticking the boxes of PR 733,
• declaring you start working on on zulip in the channel HB-mathcomp-<your file without .v>,
• and joining jitsi channels if you can (so that if people read zulip, they can just come and join you), following the naming conventions.

Also, ask about blocking issues right away.

Status

You can check the current graph.

• A black name means nothing it's either untouched or incomplete, but no one is currently working on it.
• A blue name means it is currently taken by someone, please coordinate on zulip/jitsi,
  • if it is on a blue disk it means it is incomplete and unreliable for further porting operations,
  • if it is on a yellow disk, it means it is compiling with possible problems, but one can carefully port reverse dependencies,
  • if it is on a green disk, it means someone is revising a so-called finalized file... (e.g. for backward compatible enhancements)
• A green name means it is not currently taken, so you may take it:
  • if it is on a yellow disk, it means it is compiling with possible problems, but one can carefully port reverse dependencies. This also means: please come back,
    • try to solve the "TODO", "FIXME" (this may require further modification in HB)
    • and adapt the documentation.
  • if it is on a green disk, it means there is nothing more to do (or no one is aware of mistakes so far).

As of 2021-04-13 several files should be fixed and documented, and only fieldext is accessible to porting (note that from now on, the maximal file parallelization is two).

FIXME codification

Please use the exact strings below as a comment to facilitate grep (copy paste to be sure)

• FIXME: rewrite pattern means that there was a discrepancy in rewrite pattern matching between the new and the old version,
• FIXME: extra unfold means an extra step of unfolding was needed,
• FIXME: notation printing the printing does not look nice anymore,
• FIXME: explicit Pack means you had to write Pack explicitly,
• FIXME: doc means that this is not documented.
• FIXME: generic_norm generic norm (of type M -> R instead of M -> M), will be required by MathComp Analysis

Q&A / FAQ

See also https://github.com/math-comp/hierarchy-builder/wiki/FAQ (for issues that are general to HB, not specific to the mathcomp port)

You may enter issues that have no solution yet.

• Issue: [...]

  Solution: [...]

• Issue: An HB.instance fails with a crazy type error

  Solution: check that all required files are imported, typical missing: choice, countalg

• Issue: How do I print or check the contents of a structure/factory/mixin.

  Solution: Print Mixin.axioms_, Print Factory.axioms_, Print Structure.type or Print Structure.type_. (Ultimately there should be a command)

• Issue: when using notation [the Structure.type of t] when t : Set (e.g. nat), error The term "s" has type "eqType" while it is expected to have type "Set".

  Solution: add a : Type like [the Structure.type of t : Type]