Commit 2023-06-23 04:45 e0d81340

fix: compile inductives recursively (#5039) The compileSizeOf addition inadvertently broke the tryToCompileAllInductives test (which is disabled on master because it is too expensive); if you actually run it there are hundreds of failures (421 / 1134 success), where it should only have failed a small handful of times. The reason for the failure is that compiling a T.sizeOf function requires U.rec and U.sizeOf if the definition of inductive type T uses U, so now we process them recursively. In addition there are a few more fixes for completeness:

• The UInt8, UInt16 etc types were generating invalid IR because Expr.proj doesn't work on them. We can work around this by using UInt8.val etc instead.
• The Float type needs a further hack because Float.val also fails; we implement this and Float.mk using unsafeCast, which is fine since they are conversions to and from floatSpec.float which is an opaque type.
• instSizeOfName and Name.sizeOf were manually implemented as noncomputable so they need a compile_def%. All together this unblocks essentially all the inductive types in Lean, and now the tryToCompileAllInductives test has 1131 / 1134 successes, where the three failures are Acc.below, HEq and Acc which are all expected because large-eliminating Props are not implemented. (We could special case implement these like with UInt8 et al, but these represent a general class of unimplemented inductives while UInt8 is special cased by the code generator.)