precompileModules

Stream: lean4

[Jannis Limperg]

I just tried to enable Lake's new precompileModules option for Aesop. It seems to work in principle (yay!) and makes things noticably faster (big yay!), but I encountered some issues. Repro branch: https://github.com/JLimperg/aesop/tree/precompileModules

(1) When I load an Aesop module in VSCode or Emacs, I get errors like

error loading library, Aesop-Builder-Default: cannot open shared object file: No such file or directory

(2) When I open a test file (which depends on Aesop) in VSCode or Emacs, I get errors like

`/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/lake print-paths Init Aesop` failed:

stderr:
info: > /home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/leanc -c -o ./build/ir/Aesop.o ./build/ir/Aesop.c -O3 -DNDEBUG
error: stderr:
In file included from ./build/ir/Aesop.c:4:
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/include/lean/lean.h:8:10: fatal error: 'stddef.h' file not found
#include <stddef.h>
         ^~~~~~~~~~
1 error generated.
error: external command /home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/leanc exited with status 1
error: build failed

(3) When I run lake clean && lake build, I get errors like this:

> LEAN_PATH=./build/lib LD_LIBRARY_PATH=/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/lib:./build/lib /home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/lean ./././Aesop.lean -R ././. -o ./build/lib/Aesop.olean -i ./build/lib/Aesop.ilean -c ./build/ir/Aesop.c --load-dynlib=libAesop-Check.so --load-dynlib=libAesop-Nanos.so --load-dynlib=libAesop-Util-UnionFind.so --load-dynlib=libAesop-Util-Basic.so --load-dynlib=libAesop-Util-UnorderedArraySet.so --load-dynlib=libAesop-Util.so --load-dynlib=libAesop-Frontend-ElabM.so --load-dynlib=libAesop-Percent.so --load-dynlib=libAesop-Rule-Name.so --load-dynlib=libAesop-Index-Basic.so --load-dynlib=libAesop-Index.so --load-dynlib=libAesop-Rule-BranchState.so --load-dynlib=libAesop-RuleTac-Basic.so --load-dynlib=libAesop-Rule-Basic.so --load-dynlib=libAesop-Rule.so --load-dynlib=libAesop-Builder-Basic.so --load-dynlib=libAesop-Builder-Apply.so --load-dynlib=libAesop-RuleTac-Cases.so --load-dynlib=libAesop-Builder-Cases.so --load-dynlib=libAesop-Builder-Constructors.so --load-dynlib=libAesop-Builder-NormSimp.so --load-dynlib=libAesop-Builder-Tactic.so --load-dynlib=libAesop-Builder-Default.so --load-dynlib=libAesop-Builder-Forward.so --load-dynlib=libAesop-Builder.so --load-dynlib=libAesop-RuleSet.so --load-dynlib=libAesop-Frontend-RuleExpr.so --load-dynlib=libAesop-Frontend-Attribute.so --load-dynlib=libAesop-Options.so --load-dynlib=libAesop-RuleTac-Apply.so --load-dynlib=libAesop-RuleTac-Forward.so --load-dynlib=libAesop-RuleTac-Tactic.so --load-dynlib=libAesop-RuleTac.so --load-dynlib=libAesop-Search-Expansion-Simp-Basic.so --load-dynlib=libAesop-Search-Expansion-Simp-SimpAll.so --load-dynlib=libAesop-Search-Expansion-Simp-SimpGoal.so --load-dynlib=libAesop-Search-Expansion-Simp.so --load-dynlib=libAesop-Tracing-Init.so --load-dynlib=libAesop-Tracing.so --load-dynlib=libAesop-Constants.so --load-dynlib=libAesop-Tree-BranchState.so --load-dynlib=libAesop-Tree-UnsafeQueue.so --load-dynlib=libAesop-Tree-Data.so --load-dynlib=libAesop-Tree-Traversal.so --load-dynlib=libAesop-Tree-RunMetaM.so --load-dynlib=libAesop-Tree-TreeM.so --load-dynlib=libAesop-Tree-AddRapp.so --load-dynlib=libAesop-Tree-State.so --load-dynlib=libAesop-Tree-Check.so --load-dynlib=libAesop-Tree-Format.so --load-dynlib=libAesop-Tree-ExtractProof.so --load-dynlib=libAesop-Tree-ExtractSafePrefixes.so --load-dynlib=libAesop-Tree-Free.so --load-dynlib=libAesop-Tree.so --load-dynlib=libAesop-Search-Queue.so --load-dynlib=libAesop-Profiling.so --load-dynlib=libAesop-Search-SearchM.so --load-dynlib=libAesop-Search-RuleSelection.so --load-dynlib=libAesop-Search-Expansion.so --load-dynlib=libAesop-Search-Main.so --load-dynlib=libAesop-Frontend-Command.so --load-dynlib=libAesop-Frontend-Tactic.so --load-dynlib=libAesop-Frontend.so --load-dynlib=libAesop-BuiltinRules-Assumption.so --load-dynlib=libAesop-BuiltinRules-ApplyHyps.so --load-dynlib=libAesop-BuiltinRules-DestructProducts.so --load-dynlib=libAesop-BuiltinRules-Intros.so --load-dynlib=libAesop-BuiltinRules-Split.so --load-dynlib=libAesop-BuiltinRules-Subst.so --load-dynlib=libAesop-BuiltinRules.so --load-dynlib=libAesop-Main.so
stderr:
Error: index out of bounds
backtrace:
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7f0cb62e7f4e]
./build/lib/libAesop-Frontend-RuleExpr.so(initialize_Aesop_Frontend_RuleExpr+0x36e3)[0x7f0cb28cae93]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_run_mod_init+0x28)[0x7f0cb62db208]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_registerInitAttrUnsafe___spec__14+0x190)[0x7f0cb5d98ea0]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_registerInitAttrUnsafe___lambda__3+0xce)[0x7f0cb5d9a75e]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_registerInitAttrUnsafe___lambda__3___boxed+0x3a)[0x7f0cb5d9aada]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_apply_3+0x628)[0x7f0cb62f4738]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_registerParametricAttribute___rarg___lambda__1+0x5b)[0x7f0cb5f5c00b]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_apply_3+0x666)[0x7f0cb62f4776]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l___private_Lean_Environment_0__Lean_finalizePersistentExtensions_loop+0x8bd)[0x7f0cb505594d]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_importModules___lambda__3+0x818)[0x7f0cb505c918]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_apply_2+0x382)[0x7f0cb62f3342]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_apply_1+0x16a)[0x7f0cb62f24ea]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_withImporting___rarg+0x62)[0x7f0cb516f3c2]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_importModules___lambda__4___boxed+0x3d)[0x7f0cb505d19d]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_apply_2+0x382)[0x7f0cb62f3342]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_apply_1+0x16a)[0x7f0cb62f24ea]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe)[0x7f0cb51e40fe]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0xc)[0x7f0cb51e430c]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_apply_1+0x156)[0x7f0cb62f24d6]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_profileit+0x63)[0x7f0cb623bbe3]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x54)[0x7f0cb51e4224]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_import_modules+0x103)[0x7f0cb505d003]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(l_Lean_Elab_processHeader+0x35)[0x7f0cb45db045]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_run_frontend+0x294)[0x7f0cb4d6abf4]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(+0x2b50c5f)[0x7f0cb61d5c5f]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/../lib/lean/libleanshared.so(lean_main+0x1dbb)[0x7f0cb61d7d5b]
/lib64/libc.so.6(+0x2934a)[0x7f0cb348f34a]
/lib64/libc.so.6(__libc_start_main+0x7c)[0x7f0cb348f3fc]
/home/jannis/.elan/toolchains/leanprover--lean4---nightly-2022-07-04/bin/lean(_start+0x2e)[0x20180e]

However, these errors don't seem to be fatal: the build succeeds and I can still successfully run the test suite.

[Sebastian Ullrich]

The first two should be https://github.com/leanprover/lake/issues/93. I should probably look into the bounds panic, even if it is not fatal as you said. At least we have a stacktrace now.

[Wojciech Nawrocki]

Hi! I am working on a package with precompileModules := true in the lakefile, and I can see that .so files are being built. However ps faux on an example file just shows /home/nawrocki/.elan/toolchains/leanprover--lean4---nightly-2022-07-14/bin/lean --worker file:///home/nawrocki/lean-smt/Test/BitVec/AES.lean, i.e. no --load-dynlib or whatever options are passed to the worker. Is there a separate mechanism for loading them, or should that flag be there? This is on nightly-2022-07-14.

[Mac]

Wojciech Nawrocki said:

no --load-dynlib or whatever options are passed to the worker. Is there a separate mechanism for loading them

Yep this is right, The worker, during its lake print-paths invocation gets back a list of dynlibs to load, which it then does -- no flags needed.

[Wojciech Nawrocki]

Ah cool, thanks!

[Wojciech Nawrocki]

More questions :D How do I load the precompiled modules into a command-line invocation of Lean? To get imports to work I usually write lake env lean Foo.lean, but on the command line this does not load the shared libraries even when precompileModules := true in the lakefile. I was caught unaware and wondering why something that was instant in the editor was so slow on the command line. So what magic invocation should I use? Obviously lake env lean --load-dynlib=lib1.so --load-dynlib=lib2.so Foo.lean manually is non-ideal

[Mac]

@Wojciech Nawrocki such a command does not yet exist. In my view, the best way to do this would be to support specifying Lean dynlibs/plugins through an environment variables (see my proposal) -- i just haven't got around to this yet.

[Mac]

I am a little curious as to what you are using this for. Generally lake env is used to run custom executables that run their own frontend (and thus don't usually have their own --load-dynlib) options anyway.

[Mac]

One more note: Even with environment variables, passing dynlibs through something like lake env would require a significant change in how it works. Currently, lake env does not build anything. However, Lake only knows what dynlibs their are after a build, so lake env would need to be augmented to build the whole package before executing the subcommand.

[Mac]

(This should not be difficult to do, but it would be a notable change in behavior.)

[Wojciech Nawrocki]

I am a little curious as to what you are using this for.

It's for running .produced/.expected style tests in CI, as in here. Note that we shell out to a lean process (actually without lake env in this case, but in another repo I am running lake env lean towards the same end from a shell script).

[Wojciech Nawrocki]

I suppose running the frontend directly from the Lake script would not help either.

[Mac]

@Wojciech Nawrocki Some notes on that code (hopefully this is helpful):

• Scripts are run in ScriptM, not plain IO. This means you have access to Lake's computed Workspace. Thus, for example, you can do let lean <- getLean to get the already detected Lean. rather than re-detecting it your self.
• Since that script already assumes the tests requisite modules are built, you could just pass the dynlib from the module you want directly in the script (e.g., (<- findModule? <mod-name>).get!.dynlibFile to get the file and then pass --load=dynlib={file} to the lean invocation).
• Also, for LEAN_PATH, you can use <- getAugmentedLeanPath instead of computing it yourself.

[Wojciech Nawrocki]

Thanks for the tips! For the dynlibs though, I assume I would have to manually grab it for every module? Is there a quick way to do what Lake already does when invoking lean and get all the transitively required dynlibs?

[Sebastian Ullrich]

Note that there is no need for passing the transitive closure on Unix, the root .so is sufficient. But I suppose it would be preferable if your tests worked on Windows as well.

[Mac]

Wojciech Nawrocki said:

Thanks for the tips! For the dynlibs though, I assume I would have to manually grab it for every module? Is there a quick way to do what Lake already does when invoking lean and get all the transitively required dynlibs?

@Wojciech Nawrocki No, because things like external libraries dynlibs can only be determined after a build. If you want to do that you essentially need to invoke buildImportsAndDeps like print-paths does.

[Wojciech Nawrocki]

Sebastian Ullrich said:

Note that there is no need for passing the transitive closure on Unix, the root .so is sufficient. But I suppose it would be preferable if your tests worked on Windows as well.

Indeed it looks like the shared libraries load their dependency .sos. However with just precompileModules := true, there is no root shared lib. As in, I get libFoo-Mod1.so, libFoo-Mod2.so etc but there is no build/lib/libFoo.so.

[Wojciech Nawrocki]

Since this is the case, I guess at least on Unix lake build does not in fact have to do this:

LEAN_PATH=./build/lib LD_LIBRARY_PATH=/home/nawrocki/.elan/toolchains/leanprover--lean4---nightly-2022-07-29/lib:./build/lib /home/nawrocki/.elan/toolchains/leanprover--lean4---nightly-2022-07-29/bin/lean ./././Smt/Tactic/Smt.lean -R ././. -o ./build/lib/Smt/Tactic/Smt.olean -i ./build/lib/Smt/Tactic/Smt.ilean -c ./build/ir/Smt/Tactic/Smt.c --load-dynlib=libSmt-Data-Sexp.so --load-dynlib=libSmt-Dsl-Sexp.so --load-dynlib=libSmt-Term.so --load-dynlib=libSmt-Solver.so --load-dynlib=libSmt-Commands.so --load-dynlib=libSmt-Graph.so --load-dynlib=libSmt-Util.so --load-dynlib=libSmt-Attribute.so --load-dynlib=libSmt-Translator.so --load-dynlib=libSmt-Tactic-WHNFConfigurableRef.so --load-dynlib=libSmt-Tactic-WHNFConfigurable.so --load-dynlib=libSmt-Tactic-WHNFSmt.so --load-dynlib=libSmt-Tactic-EqnDef.so --load-dynlib=libSmt-Query.so

[Wojciech Nawrocki]

Mac said:

Wojciech Nawrocki No, because things like external libraries dynlibs can only be determined after a build. If you want to do that you essentially need to invoke buildImportsAndDeps like print-paths does.

I will try this since it sounds like the only cross-platform solution.

[Wojciech Nawrocki]

Is it possible to specify in thelakefile to produce libFoo.so during the build? I am looking through the list of lean_lib arguments and tried nativeFacets := #[Module.oFacet, Module.dynlibFacet] but that fails with a cyclic dependency error (anyhow it doesn't sound like this would do the right thing). I can run lake build Foo:shared on the command line but wanted to default to that.

[Mac]

@Wojciech Nawrocki Unforunately, no, there is no way to default a library to produce something other than the lean binaries currently.

[Mac]

This was something I considered and thought of adding a facet parameter to defaultTarget. Thus, it is on the TODO list, but as I only have a week left in my internship it may be a while before its complete (at least by me).

[Alexander Bentkamp]

Wow, I really underestimated what impact precompileModules would have. On my test example, the time my tactic takes went down from 1800ms to 550ms, just by enabling precompileModules!

[Patrick Massot]

Which tactic is that?

[Alexander Bentkamp]

duper, the successor to Lean3's super.

[Alexander Bentkamp]

https://github.com/abentkamp/duper

[Alexander Bentkamp]

It's mostly @Josh Clune working on this now

[Patrick Massot]

Nice! Is it already usable?

[Alexander Bentkamp]

No, we are currently a bit underwhelmed by the performance :-). The precompileModules brings us much closer to what we would expect, but there must be some other performance bottlenecks that we need to figure out...

[Marc Huisinga]

If you're using Array, HashMap and such, you must be very careful that all the operations you expect to be O(1) are indeed O(1)

[Marc Huisinga]

E.g. Array.data is not (c.f. here, here, here and finally here) and for most mutations you need to ensure that the reference count is 1 / the array is being used linearly for array operations to be fast

[James Gallicchio]

Hey, I'm having the same issue (1) as Jannis's original question -- I'm almost positive something is just wrong with my lakefile. Thoughts?

import Lake
open System Lake DSL

package leancolls {
  precompileModules := true
}

@[defaultTarget]
lean_lib LeanColls

@[defaultTarget]
lean_exe test {
  root := `Main
}

target leancolls_array.o (pkg : Package) : FilePath := do
  let oFile := pkg.buildDir / "c" / "leancolls_array.o"
  let srcJob ← inputFile <| pkg.dir / "bindings" / "leancolls_array.c"
  buildFileAfterDep oFile srcJob fun srcFile => do
    let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
    compileO "leancolls_array.c" oFile srcFile flags

extern_lib libleancolls_array (pkg : Package) := do
  let name := nameToStaticLib "leancolls_array"
  let ffiO ← fetch <| pkg.target ``leancolls_array.o
  buildStaticLib (pkg.buildDir / "c" / name) #[ffiO]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "master"

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

The C FFI code is in a file bindings/leancolls_array.c

[James Gallicchio]

I'm on 09-05 nightly, and my VS Code extension is version v0.0.95 which seems to include the fixes above

[James Gallicchio]

Oh, wait, I wrote buildStaticLib (pkg.buildDir / "c" / name) #[ffiO] instead of "lib"... :face_palm:

[James Gallicchio]

https://github.com/leanprover/lake/blob/master/examples/ffi/lib/lakefile.lean I was copying this example... Maybe it needs updating?

[Mac]

James Gallicchio said:

Oh, wait, I wrote buildStaticLib (pkg.buildDir / "c" / name) #[ffiO] instead of "lib"... :face_palm:

I am not sure what you mean. Also you should probably not be passing a simple string as a path, as the current working directory can very based on were a package is in the dependency hierarchy. You may however want to use pkg.libDir?

[Mac]

Fyi, I am still not sure what the issue is. The FFI example builds and works so it should be a proper model for user code.

[Mac]

Oh, you may have been talking about this issue raised in a previous Zulip thread. Yeah, the FFI example likely needs an update in that case. However, its been a while and don't exactly remember why it the FFI example worked for me in the past when I tested it interactively but it doesn't now -- I will have to go take a look sometime.

[James Gallicchio]

Yeah -- I don't know enough to understand why the issue occurred, but it seems like the output needs to be in the "lib" directory in my use case. Not sure why