error: could not detect the configuration of the Lake ...

Stream: lean4

[Asei Inoue]

why this error ocurrs? how to fix this?

❯ lake build
error: could not detect the configuration of the Lake installation

My environment:

• Windows 11

❯ lake --version
Lake version 5.0.0-daa2218 (Lean version 4.11.0-rc1)

[Kevin Buzzard]

Are you running the command in the root directory of a correctly formatted lean project?

[Asei Inoue]

Yes.

[Asei Inoue]

the repository to build is lean-by-example (see https://github.com/lean-ja/lean-by-example)

git clone https://github.com/lean-ja/lean-by-example.git
cd lean-by-example
lake build

[Kim Morrison]

Can't reproduce on macos. For me it builds fine (with many warnings, but that's the repositories problem!)

[Asei Inoue]

it seems to be my elan problem

[Asei Inoue]

with many warnings, but that's the repositories problem!

Repo warnings are intended.

[Asei Inoue]

many lake commands does not run.

lean-by-example on  main
❯ lake update
error: could not detect the configuration of the Lake installation

lean-by-example on  main
❯ lake build
error: could not detect the configuration of the Lake installation

lean-by-example on  main
❯ lake exe cache get
error: could not detect the configuration of the Lake installation

[Asei Inoue]

Can't reproduce

I think elan or lake in my local environment is broken, but I'm not sure why.

[Asei Inoue]

CI is working correctly and is not a Windows problem..

[Asei Inoue]

@Kim Morrison How do I uninstall elan?

[Kim Morrison]

Just delete ~/.elan.

[Asei Inoue]

I have removed ~/.elan and tried to reinstall elan.

But following errors occur.

PS C:\Users\井上亜星\lean-by-example> Start-BitsTransfer -Source "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -Destination "elan-init.ps1"
Start-BitsTransfer : オブジェクト参照がオブジェクト インスタンスに設定されていません。
発生場所 行:1 文字:1
+ Start-BitsTransfer -Source "https://raw.githubusercontent.com/leanpro ...
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    + CategoryInfo          : NotSpecified: (:) [Start-BitsTransfer], NullReferenceException
    + FullyQualifiedErrorId : System.NullReferenceException,Microsoft.BackgroundIntelligentTransfer.Management.NewBitsTransferCommand

PS C:\Users\井上亜星\lean-by-example> Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
Set-ExecutionPolicy : 'Set-ExecutionPolicy' コマンドはモジュール 'Microsoft.PowerShell.Security' で見つかりましたが、このモジュールを読み込むことができませんでした。詳細
については、'Import-Module Microsoft.PowerShell.Security' を実行してください。
発生場所 行:1 文字:1
+ Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
+ ~~~~~~~~~~~~~~~~~~~
    + CategoryInfo          : ObjectNotFound: (Set-ExecutionPolicy:String) [], CommandNotFoundException
    + FullyQualifiedErrorId : CouldNotAutoloadMatchingModule

PS C:\Users\井上亜星\lean-by-example> $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:stable
.\elan-init.ps1 : 用語 '.\elan-init.ps1' は、コマンドレット、関数、スクリプト ファイル、または操作可能なプログラムの名前として認識されません。名前が正しく記述されている
ことを確認し、パスが含まれている場合はそのパスが正しいことを確認してから、再試行してください。
発生場所 行:1 文字:7
+ $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4: ...
+       ~~~~~~~~~~~~~~~
    + CategoryInfo          : ObjectNotFound: (.\elan-init.ps1:String) [], CommandNotFoundException
    + FullyQualifiedErrorId : CommandNotFoundException

PS C:\Users\井上亜星\lean-by-example> Write-Host "elan-init returned [$rc]"
elan-init returned []
PS C:\Users\井上亜星\lean-by-example> del .\elan-init.ps1
del : パス 'C:\Users\井上亜星\lean-by-example\elan-init.ps1' が存在しないため検出できません。
発生場所 行:1 文字:1
+ del .\elan-init.ps1
+ ~~~~~~~~~~~~~~~~~~~
    + CategoryInfo          : ObjectNotFound: (C:\Users\井上亜星\l...e\elan-init.ps1:String) [Remove-Item], ItemNotFoundException
    + FullyQualifiedErrorId : PathNotFound,Microsoft.PowerShell.Commands.RemoveItemCommand

PS C:\Users\井上亜星\lean-by-example> if ($rc -ne 0) {
>>     Read-Host -Prompt "Press ENTER to continue"
>> }
>> exit

[Asei Inoue]

my PC broken...? I cannot reisntall elan.

[Asei Inoue]

help me please...

I cannot develop Lean repos locally now...

[Julian Berman]

My powershell is.. near nonexistent -- do you have access to gitbash/etc.? to be able to run the "normal" shell script? Perhaps you'll have more luck with that?

[Asei Inoue]

run on git bash

井上亜星@LAPTOP-D4PFQO86 MINGW64 ~
$ cd lean-by-example/

井上亜星@LAPTOP-D4PFQO86 MINGW64 ~/lean-by-example (main)
$ lake build
error: could not detect the configuration of the Lake installation

[Kim Morrison]

The suggestion was to run the elan installed script under gitbash

[Asei Inoue]

@Kim Morrison @Julian Berman

do you have access to gitbash/etc.?

Elan re-installation via gitbush works. but lake build command still raises an error.

井上亜星@LAPTOP-D4PFQO86 MINGW64 ~/lean-by-example (main)
$ lake build
error: could not detect the configuration of the Lake installation

My attempt:

1. remove ~/.elan directory
2. install elan
3. run lake build on lean-by-example

[Sebastian Ullrich]

Is it the same in a standard Windows shell?

[Asei Inoue]

Note: It may be related to the version of Lean or whether it depends on Mathlib.

井上亜星@LAPTOP-D4PFQO86 MINGW64 ~/concreteSemantics (main)
$ lake build
info: downloading component 'lean'
189.8 MiB / 189.8 MiB (100 %)  16.8 MiB/s ETA:   0 s
info: installing component 'lean'
笞 [3/4] Built ConcreteSemantics.Basic
warning: .\.\.\.\ConcreteSemantics\Basic.lean:39:8: declaration uses 'sorry'
Build completed successfully.

井上亜星@LAPTOP-D4PFQO86 MINGW64 ~/concreteSemantics (main)
$ cat lean-toolchain
leanprover/lean4:v4.9.0

[Asei Inoue]

Is it the same in a standard Windows shell?

you mean command prompt? It also fails.

C:\Users\井上亜星\lean-by-example>lake build
error: could not detect the configuration of the Lake installation

[Sebastian Ullrich]

I cannot reproduce on latest lean-by-example, which now uses rc2

[Asei Inoue]

Yes, CI on Windows also does not reproduce this error… this is deep mistery…

[Sebastian Ullrich]

Oh, but my user name is ASCII. That may or may not be the issue.

[Sebastian Ullrich]

Could you check if leanprover/lean4-pr-releases:pr-release-4860 still has this issue? Creating a new empty project and trying to build it should be sufficient

[Yuyang Zhao]

A student had the same problem on v4.10.0 and v4.11.0. It was fine on v4.8.0-rc2. The error disappeared after switching to an ASCII user name.

[Eric Wieser]

I guess this also reproduces for a non-ascii folder name in an ascii user account?