Lean on windows

Stream: general

[Apurva Nakade]

Hi, I'm helping a colleague install lean on windows. We managed to install the lean4 plugin using VSCode. But the server is not starting.

[Apurva Nakade]

Also, Lake is not installed although elan and lean both exist

[Eric Wieser]

What does elan --version give?

[Apurva Nakade]

elan 3.1.1

[Apurva Nakade]

(71ddc6633 2024-02-22)

[Eric Wieser]

And for lean?

[Apurva Nakade]

Lean v 3.4.2

[Apurva Nakade]

Is this the wrong lean?

[Eric Wieser]

But the server is not starting.

Do you have a lean project set up?

[Apurva Nakade]

No we're not able to create a project as "lake" is not a recognized command

[Eric Wieser]

There is a button in vscode that will create the project for you I think

[Eric Wieser]

That should install lake at the same time

[Apurva Nakade]

Weirdly we're not seeing a "New project" menu item nor a "forall symbol" for creating a new project

[Apurva Nakade]

Actually we just restarted the app several times and it appeared. Thanks anyways!! Hopefully it'll work now.

[Apurva Nakade]

Now lake is having issues installing leantar. Is there a way to tell lake a location where to install leantar and the cache?

[Sebastian Ullrich]

Could you please include the error messages?

[Apurva Nakade]

Installing leantar 0.1.13
Uncaught exception: no such file or directory (error code: 2) file M:\

[Apurva Nakade]

We checked the environment variables and the "HOMEDRIVE" variable is set to "M:" and we're unable to change it to "C:"

[Apurva Nakade]

We keep getting an error:

imports are out of date and must be rebuilt; use the "restart file" command in your editor.

[Kim Morrison]

Does an M drive exist? If not, this seems a fundamental problem with the system.

[Apurva Nakade]

We're trying to get the IT guys to fix the system variables (requires admin access). But is there no way to tell lake a custom location to put the .cache directory?

[Apurva Nakade]

I was hoping something like --cache-dir would exist.

[Sebastian Ullrich]

You should be able to override HOMEDRIVE and HOMEPATH locally in the shell. Otherwise this would be a feature request to Mathlib4, as cache lives there.

[Mario Carneiro]

cache will use any of several environment variables to find the cache dir. The first choice is XDG_CACHE_HOME

[Julian Berman]

Does it look at that even on Windows?

[Julian Berman]

(Looks like yes -- https://github.com/leanprover-community/mathlib4/blob/340c789afdcbe26f967370ab99449ed1c87c5019/Cache/IO.lean#L47 which is a tad surprising but nice for this issue clearly)

[Apurva Nakade]

Thanks! This is very helpful.

Should this be added to the installation somewhere? Even on Mac or Linux I would prefer to have more control over where I store the .cache

[Eric Wieser]

I think XDG_CACHE_HOME is already a standard place to store things