Moving RPINF from Aesop into core

Stream: lean4

[Jannis Limperg]

@Xavier Généreux and I recently merged a new, optimised implementation of forward reasoning into Aesop. Unfortunately, this makes Aesop around 8% slower in Mathlib. :upside_down:

The reason for this is that the new implementation uses a custom normal form, RPINF (reducible proof-irrelevant normal form). This normal form is computed by traversing each expression in the goal, which incurs a large interpretation overhead.

To reduce the overhead, the RPINF function should be precompiled. We could enable precompilation for Aesop, but this increases Aesop build time and all import times by a lot. So as a stop-gap, I suggest moving the RPINF function into core. This makes Aesop 9% faster, rather than 8% slower, relative to the previous Aesop version. The RPINF function is not particularly complex and is implemented in a single file, so should hopefully not add a high maintenance burden.

Does this make sense?

[Henrik Böving]

precompileModules is per lean_lib. Could you not have an AesopNative library that contains the implementation of RPINF, enable precompileModules for that and import that from Aesop?

[Jannis Limperg]

I think so. This would address the Aesop build time concern. I believe the import time increase happens if precompilation is enabled anywhere in the import tree, but I'll check this.

[Jannis Limperg]

@Sebastian Ullrich it seems like the speed center is failing again for this run for #22408, which enables precompilation for the RPINF function in Aesop. Could you take a look at this? :thank_you: (Btw, it seems like the pheidippides runner has been down for a few days now.)

[Sebastian Ullrich]

Is that the same failure as last time? I guess the fix never landed in mathlib master?

[Jannis Limperg]

Oh, I didn't realise you fixed the script in the PR; I thought this was server-side. I'll PR the fix.

[Eric Wieser]

is precompileModules supported by lake exe cache?

[Sebastian Ullrich]

I guess we'll find out! (or rather, we already have)