error on v4.10.0-rc1

Stream: general

[Asei Inoue]

I get a this error when running lean --run Tactic.lean on https://github.com/Seasawher/mathlib4-tactics

❯ lean --run Tactic.lean
Tactic.lean:1:0: error: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.lean' in the search path entries:
c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.10.0-rc1\lib\lean
Tactic.lean:2:0: error: expected token
Tactic.lean:4:11: error: unknown constant 'CoeFun'
Tactic.lean:4:11: error: unknown constant 'sorryAx'
Tactic.lean:5:2: error: unknown constant 'Pure.pure'
Tactic.lean:5:2: error: unknown constant 'sorryAx'
Tactic.lean:5:2: error: unknown constant 'sorryAx'

[Asei Inoue]

What I tried:

• remove .lake directory and re-run
• restart file of Tactic.lean

[llllvvuu]

I get this with any project that imports a package. e.g.

echo "import Batteries" > repro.lean
lean repro.lean

is enough to error. But the language server works fine.

[Kim Morrison]

Try lake env lean, instead of just lean.

[Asei Inoue]

@Kim Morrison Same error:

mathlib4-tactics on  main via 🐍 v3.11.5
❯ lake env lean --run Tactic.lean
Tactic.lean:1:0: error: object file '.\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Tactic.olean' of module Mathlib.Tactic does not exist
Tactic.lean:2:0: error: expected token
Tactic.lean:4:11: error: unknown constant 'CoeFun'
Tactic.lean:4:11: error: unknown constant 'sorryAx'
Tactic.lean:5:2: error: unknown constant 'Pure.pure'
Tactic.lean:5:2: error: unknown constant 'sorryAx'
Tactic.lean:5:2: error: unknown constant 'sorryAx'

[Asei Inoue]

Note: my PC is on Windows OS.

[llllvvuu]

Kim Morrison said:

Try lake env lean, instead of just lean.

It works for me, thanks!

re: @Asei Inoue your error looks different than before

[llllvvuu]

Maybe you need to lake exe cache get and/or lake build

[Asei Inoue]

@llllvvuu oh that's right. Tactic.lean:1:0: error: object file '.\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Tactic.olean' of module Mathlib.Tactic does not exist is new error...

[Asei Inoue]

it works to me.

[Asei Inoue]

@llllvvuu @Kim Morrison Thank you!!

but why lean --run doesn't work? is it a deprecated way?

[Asei Inoue]

I get an error again on editor. Infoview says "import outdated, must be rebuilt" and I get a following error when rebuilt terminates:

`c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.10.0-rc1\bin\lake.exe setup-file C:/Users/11325/mathlib4-tactics/Option.lean Init Mathlib.Tactic` failed:

stderr:
✔ [699/2182] Built Mathlib.Algebra.Order.Monoid.OrderDual
...
✖ [1021/2182] Building Mathlib.Data.Set.UnionLift
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.10.0-rc1\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false .\.\.lake/packages\mathlib\.\.\Mathlib\Data\Set\UnionLift.lean -R .\.\.lake/packages\mathlib\.\. -o .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Data\Set\UnionLift.olean -i .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Data\Set\UnionLift.ilean -c .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Data\Set\UnionLift.c --json
info: stderr:
failed to open '.\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Data\Set\UnionLift.olean': 32
error: Lean exited with code 1
✔ [1022/2182] Built Mathlib.Algebra.Star.Pi
...
✖ [1034/2182] Building Mathlib.Order.ConditionallyCompleteLattice.Basic
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.10.0-rc1\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false .\.\.lake/packages\mathlib\.\.\Mathlib\Order\ConditionallyCompleteLattice\Basic.lean -R .\.\.lake/packages\mathlib\.\. -o .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Order\ConditionallyCompleteLattice\Basic.olean -i .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Order\ConditionallyCompleteLattice\Basic.ilean -c .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Order\ConditionallyCompleteLattice\Basic.c --json
info: stderr:
failed to write '.\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Order\ConditionallyCompleteLattice\Basic.olean': 13 Permission denied
error: Lean exited with code 1
✔ [1051/2182] Built Mathlib.Algebra.Group.Subsemigroup.Basic
...
✔ [2162/2182] Built Mathlib.Algebra.Ring.Action.Invariant
Some builds logged failures:
- Mathlib.Data.Set.UnionLift
- Mathlib.Order.ConditionallyCompleteLattice.Basic
error: build failed

[Asei Inoue]

... is trancated long long log.

[Asei Inoue]

my file is:

import Mathlib.Tactic
#help option

def main : IO UInt32 :=
  return 0

(this file is named "Option.lean")

[Asei Inoue]

strangely, lake env lean --run Option.lean does not raise an error...

[Kim Morrison]

lean will work, but you need to set many more options. lean itself knows nothing about lake, so it knows nothing about dependencies or source locations.

[Kim Morrison]

I think of you run lake env by itself it prints out the settings it passes to lean.

[llllvvuu]

It's funky that there is even a build happening at all, since lake exe cache get is supposed to avoid that. The permission issue is also funky. If deleting .lake and re-doing the lake exe cache get doesn't fix it (you can test this by just running lake build and it should not build any Mathlib), then maybe someone who knows more about Windows can help

[Asei Inoue]

I still have error...

[Kim Morrison]

... perhaps you should tell us what the error is, in that case!