LEAN_PATH

Stream: general

[Patrick Massot]

I'm trying to use Lean from outside a project folder, using the LEAN_PATH environment variable. But it looks like it doesn't use the olean in this case (at least it starts eating up 380% CPU). I tried typing: LEAN_PATH="/home/pmassot/.elan/toolchains/3.4.1/lib/lean/library/:/home/pmassot/lean/perfectoid-spaces/_target/deps/mathlib/:." lean t2.lean in order to use the (compiled) mathlib that I have in the perfectoid project to execute t2.lean (which is a tiny test file).