Minimal setup for importing .lean files in the same director

Stream: new members

[Eduardo Ochs]

Hi all,

I'm trying to put this in a format that would be easy to git-clone and test, but all my attempts to write its lakefile.lean are failing miserably... here is a minimal example that shows my problem:

rm -Rfv /tmp/test/
mkdir   /tmp/test/
cd      /tmp/test/

cat > Lib.lean <<'%%%'
def a := 42
%%%

cat > Example.lean <<'%%%'
import Lib
#eval a
%%%

cat > lakefile.lean <<'%%%'
import Lake
open   Lake DSL
package  Lib
lean_lib Lib
%%%

# (find-file "/tmp/test/Example.lean")

When I open the file Example.lean in Emacs the line import Lib gives the error unknown package 'Lib'. How do I fix that?