Unknown Package MIL

Stream: new members

[Peter Dolland]

I have MIL.lean and the MIL folder on another place than on my project folder. So VSCode does not know it. What I have to do to integrate it?

[Kevin Buzzard]

You won't be able to use imports in VS Code unless you open the root directory of a lean project. This is just how the extension works.

[Peter Dolland]

Kevin Buzzard schrieb:

You won't be able to use imports in VS Code unless you open the root directory of a lean project. This is just how the extension works.

I copied MIL* in my project folder, but this had no effect. Do I have to build something new? My lakefile:

import Lake
open Lake DSL

package «start» {
-- add any package configuration options here
}

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «Start» {
-- add any library configuration options here
}

... nothing about MIL?

[Peter Dolland]

My work around is to copy my lean sources into the MIL project folder. But I do not like this. I would prefer to keep my trials separate.

[Alex J. Best]

You want to have a project that depends on MIL? Then you can add a dependeny on it via lake https://github.com/leanprover/lean4/tree/master/src/lake#adding-dependencies and let lake handle downloading it and putting it in a place that lean can find it (with lake build)

[Peter Dolland]

Thank you! It has worked.