Commit 2025-07-25 00:21 37fa5281

fix: make compile_inductive% work correctly with new compiler (#27401) The implementation of compile_inductive% made assumptions about the implementation of the old compiler that are no longer true. In particular, it looked for compiler IR decls in the kernel env, but these now exist in a private environment extension. The main use of this check is to avoid recompiling a sizeOf definition multiple times within its originating module, so to fix this we just disable the recursive recompilation of inductives within the module of their definition. This means that they will require explicit compile_inductive% directives themselves, which were already being supplied anyways. Fixes #27017.