cannot open shared object file

Stream: lean4

[Jon Eugster]

I'm trying to modify the web editor to allow different lean versions and packages imported. Currently I hit a weird error:

error loading library, libAuto-Lib-Containers-1.so:
  cannot open shared object file: No such file or directory

on importing a package import Auto. Does anybody know what .so files are and where this error might be generated? I assume somewhere in lean core or maybe lake (?) but I currently don't even know where to start looking...

[Mac Malone]

.so files are Linux shared library files. These -1 files are generated by Lake as part of the precompileModules feature. It compiles each individual module of a library into its own -1 native shared library and loads them via lean's --load-dynlib option. This enables the use of user @[extern] functions at elaboration-time.

[Jon Eugster]

Thanks Mac! I had another go at this and adding precompileModules := false to the package and all dependencies to prevent any .so file from being generated fixed everything. looks like lean4web (at when running an old lean version v4.3.0-rc1) does not handle these files well.

[Jon Eugster]

which is apparently only a matter of calling lake serve -- instead of lean --server :open_mouth: