Mathlib missing when using Lean with Docker on command line

Stream: lean4

[Ben]

I'm new to Lean and am interested in a non-standard use case. I'm not using VSCode or Emacs to run Lean interactively. Instead, I have a Dockerfile and want to run Lean on the command line.

I've posted a question to Proof Assistants on Stack Exchange. If there's a good channel to ask in Zulip I'm not sure which channel is most relevant.

[Mauricio Collares]

You're not supposed to run lean test.lean directly. You can run lake build ProjectName.test instead. The reason lake build by itself does nothing is because it builds the ProjectName.lean file at the root of your project, which you probably haven't edited.

[Mauricio Collares]

If you encounter cache issues, it's a known issue with the most recent unstable version of lean. Take a look at #general > Updating to 4.15.0 @ 💬 for how to revert to v4.15.0

[Ben]

Mauricio Collares said:

You're not supposed to run lean test.lean directly. You can run lake build test instead.

Here's what I get when, in /opt/new_project/project_name/, I run that:

$ lake build test
Build completed successfully.

But nothing is produced from that successful build as far as I can tell

[Mauricio Collares]

If test.lean contains errors, do you get an error when running lake build test or lake build ProjectName.test?

[Mauricio Collares]

Build artifacts are in .lake/build by default

[Ben]

Thanks for the feedback! As you might be able to tell, I'm new to Lean. The lack of documentation for my use case is challenging.

No errors from the build. Interestingly, when I run

lake build ProjectName.test
⣾ [371/635] Running Mathlib.Tactic.Simps.Basic (+ 7 more)

it looks like Mathlib is being found...

Regarding the version, I do have the latest:

lean --version
Lean (version 4.16.0-rc1, aarch64-unknown-linux-gnu, commit 0c9a488bea56, Release)

so I've added rev = "v4.15.0" to lakefile.toml

The build command did produce test.c in .lake/build/ir/ProjectName/test.c

Is there no way to just run lean test.lean? I have to compile the file to .c as part of a project?

[Mauricio Collares]

Bare lean does not handle external packages, but if you really want you can use lake lean test.lean

[Mauricio Collares]

It still generates a test.c file, though

[Ben]

Mauricio Collares said:

Bare lean does not handle external packages, but if you really want you can use lake lean test.lean

Perfect! Now I get

cd /opt/new_project/project_name
lake lean ProjectName/test.lean
TopologicalSpace.{u} (X : Type u) : Type u

[Mauricio Collares]

Note that lake build ProjectName.test also "runs" your #check commands and the like, so it should be indistinguishable from the above command (I think?)

[Ben]

No. Here's what I get:

root@7d9883e60726:/opt/new_project/project_name# ls
lakefile.toml  lake-manifest.json  lean-toolchain  ProjectName  ProjectName.lean  README.md
root@7d9883e60726:/opt/new_project/project_name# ls ProjectName
Basic.lean  test.lean
root@7d9883e60726:/opt/new_project/project_name# lake lean ProjectName/test.lean
TopologicalSpace.{u} (X : Type u) : Type u
root@7d9883e60726:/opt/new_project/project_name# lake lean ProjectName.test
error: no such file or directory (error code: 2)
  file: ProjectName.test

[Mauricio Collares]

That's not the command I suggested :) lake build and lake lean expect different arguments. But I'm not saying you should use lake build, I was just pointing out an alternative:

$ lake build ProjectName.test
ℹ [635/635] Built ProjectName.test
info: ././././ProjectName/test.lean:2:0: TopologicalSpace.{u} (X : Type u) : Type u
Build completed successfully.

$ lake lean ProjectName/test.lean
TopologicalSpace.{u} (X : Type u) : Type u

[Ben]

Ah, thanks for explaining. My mistake for not reading carefully.

Would you like to claim credit on Stack Exchange for answering my question? (Or should post the answer?)

[Mauricio Collares]

No need, thanks for asking! But I'm happy with you (or someone else) posting it as an answer there.