Zulip Chat Archive

Stream: general

Topic: LEAN_PATH


view this post on Zulip Patrick Massot (Aug 14 2018 at 21:55):

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).


Last updated: May 09 2021 at 19:11 UTC