In math comp we are considering switching some records to primitive, but the current syntax for that is very ugly, see
math-comp/math-comp#591
since one has to Set/Unset before/after each record declaration.

This is very low prio, but it usually happens that when touching Prims or some other file high in the dependency graph, we get spurious diffs in many other files. Since we check-in the snapshot, and we need to have it up-to-date, we get very verbose commits when nothing relevant changed. Plus, when something did change, it's hard to spot.

Example: I removed a few lines in prims and get things

We would like to be able to modify IRs at various levels to simulate the effects of a compiler change. In most cases the plumbing for this would be very difficult, but labLang is nearly identical in scope to a traditional assembly language and it would be possible to dump labLang as editable assembly in arch-specific syntax.

Have a theory that the garbage collector is slow because it copies

As per the GNU make specification if possible.

• In many cases, especially from lean, a function is defined as inductive depending on a family, e.g. cases_on.
• Subsequently this is applied to a constant family.
• In this case, _.induc should simplify to _.rec