error: could not detect configuration of Lake installation

Stream: general

[Asei Inoue]

This raises an error:

❯ git clone https://github.com/lean-ja/lean-by-example.git
Cloning into 'lean-by-example'...
remote: Enumerating objects: 4641, done.
remote: Counting objects: 100% (681/681), done.
remote: Compressing objects: 100% (307/307), done.
remote: Total 4641 (delta 410), reused 563 (delta 368), pack-reused 3960
Receiving objects: 100% (4641/4641), 1.11 MiB | 2.58 MiB/s, done.
Resolving deltas: 100% (3213/3213), done.

~ took 2s
❯ cd .\lean-by-example\

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

I don't know how to resolve this.

[Asei Inoue]

my OS: Windows 11

[Asei Inoue]

elan toolchain:

lean-by-example on  main
❯ elan toolchain list
leanprover/lean4:nightly
leanprover/lean4:stable (default)
leanprover/lean4:v4.10.0-rc1
leanprover/lean4:v4.8.0
leanprover/lean4:v4.8.0-rc1
leanprover/lean4:v4.8.0-rc2
leanprover/lean4:v4.9.0
leanprover/lean4:v4.9.0-rc2
leanprover/lean4:v4.9.0-rc3

[Asei Inoue]

lake build also does not work.

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

[Kevin Buzzard]

For me lake update works fine:

$ lake update
No files to download
Decompressing 4799 file(s)
Unpacked in 11518 ms
Completed successfully!
info: mdgen: cloning https://github.com/Seasawher/mdgen to '././.lake/packages/mdgen'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '././.lake/packages/mathlib'
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: mathlib: running post-update hooks
$

This is on commit a881e6777e8c3f9c5f58766f697f52f1f2d2964a of the repo.

[Asei Inoue]

this problem is Windows specific?

[Kevin Buzzard]

I don't know. But I'm on Ubuntu.

[Asei Inoue]

I tested this on devcontainer (mcr.microsoft.com/devcontainers/base:jammy). It works fine on Ubuntu...

[Asei Inoue]

(outdated)

[Asei Inoue]

(deleted)

[Asei Inoue]

(deleted)

[Asei Inoue]

(deleted)

[Asei Inoue]

(del)

[Asei Inoue]

(deleted)

[Asei Inoue]

I tried to reproduce this issue on GitHub Action.

Here is my workflow file:

name: CI on Windows

# https://docs.github.com/en/actions/using-jobs/using-concurrency#example-only-cancel-in-progress-jobs-or-runs-for-the-current-workflow
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

on:
  pull_request:
  push:
    branches:
      - main
  workflow_dispatch:

jobs:
  build:
    runs-on: windows-latest
    steps:
      - name: checkout
        uses: actions/checkout@v4

      - name: install elan
        run: |
          curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
          echo 1 | powershell -ExecutionPolicy Bypass -f elan-init.ps1
          del elan-init.ps1
        shell: pwsh

      - name: run lake build
        run: |
          echo "::group::add PATH"
          $ENV:Path+=";$env:USERPROFILE\.elan\bin"
          echo "::endgroup::"

          echo "::group::Mathlib Cache"
          lake exe cache get
          echo "::endgroup::"

          echo "::group::lake build"
          lake build --quiet
          echo "::endgroup::"
        shell: pwsh

but this workflow does not raise an error!!
see: https://github.com/Seasawher/lean-by-example-fork/actions/runs/9873274985/job/27265175764

I don't understand this issue.

[Kim Morrison]

@Asei Inoue, have you tried deleting your .elan and reinstalling elan?

[Mac Malone]

As kim suggested, this error means that your Lake installation is likely corrupted. Thus, deleting and reinstalling the the current toolchain (either via elan uninstall or reinstalling elan altogether) is likely the best solution.