path="." in leanpkg.toml

Stream: general

[Eric Wieser]

Is this supported? I tried running leanpkg test in such a project (https://github.com/eric-wieser/logical_verification_2021/runs/2952123633?check_suite_focus=true), and it decided to go try and build _targets/mathlib/scripts/lint_mathlib.lean

[Eric Wieser]

Ah, nevermind:

WARNING: leanpkg configurations not specifying path = "src" are deprecated.

[Sebastian Ullrich]

(for exactly this reason)

[Eric Wieser]

I made a PR at https://github.com/blanchette/logical_verification_2021/pull/1 for the project in question

[Sebastian Ullrich]

Fwiw, this has been "fixed" in Lean 4. By compiling only files reachable from the root file via imports instead of all files contained in path, we can't accidentally escape the package files.