I have a file which contents are:

import Mathlib.Data.Rat.Basic

I save it as file.lean in a lean project and run it like this

lean --run .\file.lean

I get

.\file.lean:1:0: error: unknown package 'Mathlib'

but if I do

> ls .\lake-packages\    

    Directory: C:\fakepath\mathematics_in_lean\lake-packages

Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
d-----        30.10.2023     01:25                aesop
d-----        30.10.2023     00:33                Cli
d-----        30.10.2023     01:24                mathlib
d-----        30.10.2023     01:24                proofwidgets
d-----        30.10.2023     01:25                Qq
d-----        30.10.2023     01:25                std

So it should work, right?

I don't want it to run on vscode, just run on the terminal.


2 Answers 2


I've had the same problem. It was crucial for me to run Lean code using terminal. After trial and error, this is the only way I've managed to do that:

  1. Go to the directory where your *.lean file is:
cd /path/to/lean_file/
  1. Run your *.lean file using this command:
lake env lean file_name.lean

This command works slow, but it does the job.


To build a single file in a Lean project from the command line, you should be using lake build Path.To.File, which would build Path/To/File.lean.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.