export LEAN_PATH=../../build lean --run Package.lean