running compiled tactic

Stream: lean4

[Tomas Skrivan]

What is the current status of compiling tactics? I wrote simproc that I want to run compiled. Is the only option adding precompileModules := true to my lakefile and compile my whole library? And that is not feasible as I would have to compile mathlib. Can I select just one file to compile?

[Sebastian Ullrich]

I think this is effectively a Lake feature request for applying options to a subset of a library (and/or robust support for overlapping libraries)? This also came up at https://github.com/leanprover-community/mathlib4/pull/3575#discussion_r1173937573. /cc @Mac Malone

[Mac Malone]

While precompiling a subset of a package is certainly part of this feature request, that is not the whole problem here. When a module is precompiled, Lake also precompiles any of its transitive imports. This is because definitions within the module may make use of functions inits imports and the compiled shared library cannot have any unresolved symbols to such functions. So, if the simproc @Tomas Skrivan wants compiled makes use of some mathlib utiltities, he would have to compile those modules as well. However, if he can isolated the code he wants precompiled into a module with no such imports, he can avoid this issue.

To precompile a single module, you can define an overlapping lean_lib whose root is just that module or subtree and set precompileModules := true only on it. That is, the issue @Sebastian Ullrich linked has since been resolved by lean4#64425cb and lean4#2937. For example:

package scilean where
  -- options shared across package Lean libraries

lean_lib SciLean where
  -- options for SciLean (and below) modules without a more specific library

lean_lib SciLean.Tactic.MySimpProc where
  -- options for SciLean.Tactic.MySimpProc (and below) modules
  precompileModules := true

[Tomas Skrivan]

When running lake build I get the expected

...
[1730/1732] Linking SciLean.Tactic.LSimp.LetNormalize
[1731/1732] Building SciLean

but when I run

lake env lean SciLean/Tactic/LSimp/LetNormalizeTest.lean

I'm still getting

interpretation of SciLean.Tactic.let_normalize took 23.1ms

[Sebastian Ullrich]

Rebuild with lake build -v to see the correct lean invocation :)

[Tomas Skrivan]

Ohh so running lean env lean *.lean is not enough? Do I have to really call lake env lean SciLean/Tactic/LSimp/LetNormalizeTest.lean --load-dynlib=./.lake/build/lib/libSciLean-Tactic-LSimp-LetNormalize-1.so?

I would love to run the compiled tactic in my editor, the speed gain is insane :)

interpretation of SciLean.Tactic.let_normalize took 0.00367ms

(not sure why does it still say "interpretation")

[Sebastian Ullrich]

Oh it should just work in your editor! If it doesn't, that's a bug. It's only when you go the manual lean way that you have to be that specific.

[Sebastian Ullrich]

(not sure why does it still say "interpretation")

Looks like an edge case, the interpreter is the one responsible for locating and invoking native code but we could avoid the profile entry if the top function is already native

[Tomas Skrivan]

Ohh there is a bug in emacs command (lean4-std-exe)

[Tomas Skrivan]

When I look at the output in the infoview it shows the blazing speed :)

[Tomas Skrivan]

Why doesn't mathlib compile tactics this way?

[Sebastian Ullrich]

The PR I linked above was exploring that! At that point, it turned out the minor speedups did not warrant looking into resolving the remaining issues. In the end, Mathlib spends most of its tactic time in core code. The precompilation overhead, for both precompiling and runtime-loading, also increases for tactics with many dependencies.

[Tomas Skrivan]

I believe the recently added tactic fun_prop could greatly benefit from that.

Is there at least a way to compile it in my project? i.e. depend on mathlib and add to my project

lean_lib mathlib_tactics_compile where
  precompileModules := true
  roots := #[`Mathlib.Tactic.FunProp]

I'm getting an error

error: 'Mathlib.Tactic.FunProp': no such file or directory (error code: 2)
  file: ./././Mathlib/Tactic/FunProp.lean

and modifying lakefile of mathlib seems to invalidate cache

[Mario Carneiro]

You should be able to do this, but I think you need to use a file in the current project as your roots, so just have a MathlibTacticsCompile.lean file containing import Mathlib.Tactic.FunProp and make a lib from that

[Tomas Skrivan]

That is a neat trick. I will try it out tomorrow.