Jumping to Lean 4 module

Stream: lean4

[Patrick Massot]

I’m sure someone already asked but I couldn’t find it on Zulip. When I use the jump to definition, whenever I end up in the Lean 4 code base I get an error message about module not being enabled there, and nothing works. Is there anything I can do?

[Julian Berman]

That doesn't seem to happen here, jumping into core seems to work fine. I take it this breakage happens for you both in nvim and VSCode? What's your default toolchain set to?

[Robert Maxton]

I have the same problem, though I've never used nvim and I'm on Windows

[Eric Wieser]

I think this is because lake doesn't work inside lean4 (there is no lakefile), and so there is nothing to read to determine if the module feature is enabled.

[Marc Huisinga]

We've recently diagnosed this as an Elan bug that occurs only on Windows. cc @Sebastian Ullrich

[Marc Huisinga]

Eric Wieser said:

I think this is because lake doesn't work inside lean4 (there is no lakefile), and so there is nothing to read to determine if the module feature is enabled.

Elan should set the correct override in the toolchain directory.

[Michael Rothgang]

I recall Patrick using Linux, though --- so this cannot explain their issue :thinking:

[Marc Huisinga]

In that case the following would be helpful for debugging:

• The output of the 'Show Setup Information' command when looking at the tab for the core file that has the error about module
• The output of elan dump-state in src/lean of the toolchain folder that you expect to be used (e.g. for current Mathlib, this is ~/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/src/lean/)

[Patrick Massot]

Today I’m on a different computer and it works…

[Patrick Massot]

I cannot run VSCode on the computer that doesn’t work, I’ll do it tonight. But the elan dump-state look the same on both machines.

[Patrick Massot]

On the machine that works:

{
  "elan_version": {
    "current": "4.1.2",
    "newest": {
      "Ok": "4.1.2"
    }
  },
  "toolchains": {
    "installed": [
      {
        "resolved_name": "leanprover/lean4-nightly:nightly-2025-05-23",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-05-23"
      },
      {
        "resolved_name": "leanprover/lean4:v4.17.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.17.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.18.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.18.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.19.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.19.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.19.0-rc3",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.19.0-rc3"
      },
      {
        "resolved_name": "leanprover/lean4:v4.20.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.20.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.20.0-rc5",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.20.0-rc5"
      },
      {
        "resolved_name": "leanprover/lean4:v4.20.1",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.20.1"
      },
      {
        "resolved_name": "leanprover/lean4:v4.21.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.21.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.21.0-rc3",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.21.0-rc3"
      },
      {
        "resolved_name": "leanprover/lean4:v4.22.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.22.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.22.0-rc2",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.22.0-rc2"
      },
      {
        "resolved_name": "leanprover/lean4:v4.22.0-rc3",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.22.0-rc3"
      },
      {
        "resolved_name": "leanprover/lean4:v4.22.0-rc4",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.22.0-rc4"
      },
      {
        "resolved_name": "leanprover/lean4:v4.23.0-rc2",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.23.0-rc2"
      },
      {
        "resolved_name": "leanprover/lean4:v4.24.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.24.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.25.0-rc2",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.25.0-rc2"
      },
      {
        "resolved_name": "leanprover/lean4:v4.26.0-rc2",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.26.0-rc2"
      },
      {
        "resolved_name": "leanprover/lean4:v4.7.0",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.7.0"
      },
      {
        "resolved_name": "leanprover/lean4:v4.8.0-rc2",
        "path": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.8.0-rc2"
      }
    ],
    "default": {
      "unresolved": {
        "Remote": {
          "origin": "leanprover/lean4",
          "release": "stable",
          "from_channel": "stable"
        }
      },
      "resolved": {
        "live": {
          "Ok": "leanprover/lean4:v4.25.1"
        },
        "cached": "leanprover/lean4:v4.24.0"
      }
    },
    "active_override": {
      "unresolved": {
        "Remote": {
          "origin": "leanprover/lean4",
          "release": "v4.26.0-rc2",
          "from_channel": null
        }
      },
      "reason": {
        "InToolchainDirectory": "/home/pmassot/.elan/toolchains/leanprover--lean4---v4.26.0-rc2"
      }
    },
    "resolved_active": {
      "live": {
        "Ok": "leanprover/lean4:v4.26.0-rc2"
      },
      "cached": "leanprover/lean4:v4.26.0-rc2"
    }
  }
}

[Patrick Massot]

On the one that doesn’t work PastedText.txt

[Patrick Massot]

The second version is too long for a Zulip message.

[Sebastian Ullrich]

Yes, that part looks fine