Running lean from command line

Stream: lean4

[Tomaz Gomes Mascarenhas]

Hi! So, I was trying to compile a file inside a lake project from command line (I want to build a testing script), with lean --load-dynlib=<path-to-lib.so> file.lean which was working fine. Now I added mathlib4 as a dependency of the project, and I got error: unknown package 'Mathlib' when trying to run the same command. I tried to build Mathlib's shared library and add it to the command, getting lean --load-dynlib=<path-to-lib.so> --load-dynlib=<path-to-Mathlib.so> file.lean, but then I get the error:

libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, /home/tomazgomes/Desktop/Projects/masters/lean-smt/lake-packages/mathlib/build/lib/libMathlib.so: undefined symbol: l_Lean_NameMapExtension_find_x3f___rarg___boxed

What should I do?

[James Gallicchio]

I'm not sure how to get things running without Lake. Is there a particular reason you're avoiding using Lake?

[Tomas Skrivan]

I'm not by a computer right now but I got this working few months back.

Make sure your Lean and mathlib versions are matching, include mathlib oleans in LEAN_PATH environment variable(not sure if I remember the variable name correctly).

However, I'm not familiar with your error and I have no clue if my suggestion will solve it.

[Tomas Skrivan]

Also you might have to provide paths for *.olean and *.so for Std4, quote4, ... i.e. mathlib's dependencies

[Sebastian Ullrich]

Do not set LEAN_PATH manually. Use lake env

[Tomas Skrivan]

I was doing it to create shared library that I then loaded from a different application. It was a pain to get it working, especially with some dependencies like mathlib. Later I figured out how to do it with lake and my life was much happier :)

I would strongly suggest to think hard if you can achieve what you want with lake.

[Tomaz Gomes Mascarenhas]

James Gallicchio said:

I'm not sure how to get things running without Lake. Is there a particular reason you're avoiding using Lake?

I need a way to compile just a file as opposed to the entire project. Is there a way to do it using lake?

[James Gallicchio]

I think you should be able to make a target with that file as its root? see lake readme

[Tomas Skrivan]

This function generates a target for every directory in Wrangles directory and the root Lean file is Main.lean. Likely you can modify this approach.

[Kevin Buzzard]

Tomaz Gomes Mascarenhas said:

James Gallicchio said:

I'm not sure how to get things running without Lake. Is there a particular reason you're avoiding using Lake?

I needed a way to compile just a file as opposed to the entire project. Is there a way to do it using lake?

I've only ever used lake with Mathlib but lake build +Mathlib.Path.To.File will just compile that one file and all its dependencies.

[Tomaz Gomes Mascarenhas]

Kevin Buzzard said:

Tomaz Gomes Mascarenhas said:

James Gallicchio said:

I'm not sure how to get things running without Lake. Is there a particular reason you're avoiding using Lake?

I needed a way to compile just a file as opposed to the entire project. Is there a way to do it using lake?

I've only ever used lake with Mathlib but lake build +Mathlib.Path.To.File will just compile that one file and all its dependencies.

Thanks! I will use this approach to build a single file. The only problem is that it seems that, by default, no logs (and outputs of commands like #check) are printed while building with lake. Is there a way to print them?