how to use import?

Stream: lean4

[Kreijstal]

As asked here https://proofassistants.stackexchange.com/questions/2526/how-to-run-lean4-with-mathlib-manually
Basically, I have lean isntalled, and mathlib is installed too, but imports don't seem to work? maybe I am doing it wrong?

[Ruben Van de Velde]

How did you create your project? Did you create a project?

[Kreijstal]

i'm using the already existing project from MIL, shouldn't that work?

[Ruben Van de Velde]

Can the rest of MIL import mathlib?

[Kreijstal]

how can I test?

[Kreijstal]

should I simply try
lean --run?

[Ruben Van de Velde]

Are you running from vs code or some other way?

[Kreijstal]

lean --run .\MIL\Common.lean
.\MIL\Common.lean:1:0: error: unknown package 'Mathlib'

[Kreijstal]

as I said, I want to run it from the terminal

[Kreijstal]

I guess MIL can't import Mathlib when run from lean --run either

[Ruben Van de Velde]

Try lake build

[Kreijstal]

lake build&&lean --run MIL/Common.lean
MIL/Common.lean:1:0: error: unknown package 'Mathlib'

[Kreijstal]

Not sure why would it be different

[Richard Copley]

Start here and click on Using Lake (build system) in the menu on the left. Read the whole page, then follow the instructions in 'Working on an existing project'. The instructions use MIL as their example, so it should be easy to follow the steps and set up the project correctly.

When you get to the step which says "Launch VS Code", do this instead:

• change directory to "mathematics_in_lean" and run lake build

That is all. There is no need to run a file of mathematical proofs. (What would it do?)

[Kyle Miller]

lake is responsible for running lean for you. You can do lake build --verbose to see the full command line invocations it runs. It sets up environment variables so that lean can find everything.

[Kreijstal]

ahh, I see, well I wanted to use rational numbers in lean, not as a proof, but just import them, to use them, maybe I am doing things wrong?

[Kreijstal]

and I want to run this program from the terminal, so vscode doesn't help me much here

[Kyle Miller]

You can get lake to run programs too. This is how for example lake exe cache works in mathlib. I think this is all mathlib needs to add to the lakefile to get lake to be able to do this.

[Kreijstal]

in this case, how to tell lake to run file.lean?

[Kreijstal]

lake script run file.lean doesn't seem to work

[Damiano Testa]

Does lake env lean file.lean do what you want?

[Kreijstal]

@Damiano Testa
the answer was lake env lean --run file.lean thank you so much guyss

[Kreijstal]

is there a way to run --verbose with lake env? I don't see the command line invocations of lake in this case

[Kyle Miller]

If you do lake env by itself at least it will print out the values of all the environment variables it sets

[Kyle Miller]

And it looks like lake env does not do anything with the verbosity setting. It computes the environment and then just runs the provided command with IO.Process.spawn.