Setup issues for contributing to mathlib4

Stream: mathlib4

[Jean Abou Samra]

Hi, I'm new here. I installed Lean by unpacking https://github.com/leanprover/lean4/releases/download/v4.17.0-rc1/lean-4.17.0-rc1-linux.tar.zst and adding the bin/ directory to my path.

I am not using Elan nor VS Code (the reasons would be off-topic).

The Lean LSP works in my editor, and I'm able to use mathlib in a package created with lake (after adding it to the dependencies in the lakefile.toml, fixing lean-toolchain and running lake update then lake exe cache get).

However, when I try to contribute to mathlib itself, after doing lake exe cache get, a lake build succeeds, but I can't use the LSP. It fails on imports from mathlib itself, telling me: “Unknown module prefix 'Mathlib'. No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries: /…/lib/lean”.

What might be going on?

[Julian Berman]

(The only community supported setup is using elan, so I suspect for many people discussing some other setup is entirely offtopic for mathlib itself, and by doing so you're on your own there, but I sympathize, as I too occasionally use some other setup.)

You'll have to be a bit more specific though on exactly what you ran and what you did -- in particular, running lake update is not part of contributing to Mathlib typically, and I don't know what you mean by "fixing" lean-toolchain, nothing should be touched there even from the rest of what you mention.

[Jean Abou Samra]

Sorry, copy-paste mistake, I did not run lake update in the mathlib repo (edited the OP).

[Jean Abou Samra]

By "fixing" lean-toolchain I mean the curl command here: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#in-an-existing-project

[Jean Abou Samra]

(It changed the contents from leanprover/lean4:4.17.0-rc1 to leanprover/lean4:v4.17.0-rc1, which seems a little strange to me, but I did not investigate. In any case, the LSP worked on this test package with mathlib dependency.)

[Julian Berman]

So.. it didn't change them in other words? That simply means you have the same version now as what Mathlib is using right now, which is all fine.

[Julian Berman]

And you're saying everything works fine in your project depending on Mathlib?

[Julian Berman]

And now you have a separate directory with a new clone of Mathlib itself, and in there stuff doesn't work?

[Jean Abou Samra]

Julian Berman said:

So.. it didn't change them in other words? That simply means you have the same version now as what Mathlib is using right now, which is all fine.

Mind the v added to the version.

[Jean Abou Samra]

Julian Berman said:

And now you have a separate directory with a new clone of Mathlib itself, and in there stuff doesn't work?

Yes, exactly. I can use mathlib in a package I create with lake, but not contribute to mathlib itself.

[Jean Abou Samra]

This is all I did to try contributing to mathlib:

• git clone mathlib
• lake exe cache get
• Open some file in Mathlib/

[Julian Berman]

Jean Abou Samra said:

Mind the v added to the version.

(oh, I see, yes I think that seems fine, the tag is named with a v, and certainly it doesn't seem to matter if things work there)

[Julian Berman]

What editor are you in?

[Jean Abou Samra]

Helix. It auto-detected the lean command to launch the LSP.

[Julian Berman]

That sounds wrong

[Julian Berman]

Specifically you need to check that it ran lake serve, and that it did so from the right workspace root

[Julian Berman]

(which should be the directory you cloned mathlib into)

[Jean Abou Samra]

Aaah, thank you, let me see if that fixes it.

[Julian Berman]

In particular if it ran lean --server usually that means something has gone wrong (perhaps it ran lake, but in the wrong directory)

[Marc Huisinga]

Does the Helix plugin have an InfoView?

[Jean Abou Samra]

I did some debugging. For a start, Helix was configured by default to run lean --server, I changed that to use lake serve. But now what happens is that Helix correctly detects the root folder based on the presence of lakefile.lean, but still spawns the LSP process in the CWD. Nevertheless I see in the LSP conversation log that it sends

"rootPath":"/home/jean/repos/mathlib4",
"rootUri":"file:///home/jean/repos/mathlib4",
"workspaceFolders":[{"name":"mathlib4","uri":"file:///home/jean/repos/mathlib4"}]

in the initialize request. In the LSP spec (https://microsoft.github.io/language-server-protocol/specifications/specification-3-14/#workspace_workspaceFolders) it is explained that these are how the client tells the server about the project root (and possibly other workspaces).

This leaves me a bit confused. Does Lean really follow LSP conventions by requiring to be started in the root?

[Jean Abou Samra]

Marc Huisinga said:

Does the Helix plugin have an InfoView?

I'm not using a Helix plugin (I don't think these even exist yet), just Helix's built-in LSP support. What do you mean by an InfoView?

[Ruben Van de Velde]

Frankly I would suggest that you try the recommended setup with Vs code first before you try a custom one

[Kevin Buzzard]

What do you mean by an InfoView?

You would not be the first person to try Lean with a non-recommended set up and be completely unaware of the infoview, giving yourself a hugely degraded Lean experience and making things much harder for yourself, but I do not want you to be another one of these people.

Here's some code:

import Mathlib

example (a b : ℝ) : (a + b)^2 = a^2+b^2+2*a*b := by
  -- put your cursor here and look right
  ring

Click on "View in Lean 4 playground" (icon on the top right of the code) and you'll see the infoview in action in a web browser.

[Kevin Buzzard]

It's an interactive view giving you the current goal state, hypotheses, and lots of features like hovering on types and terms to see their definitions etc. It's indispensable for any nontrivial project.

[Jean Abou Samra]

So the InfoView is just the right panel on live.lean-lang.org and in VS Code? I see. I would have assumed these features would be (mostly) covered by the LSP capabilities, but I guess the protocol might not be too tailored to proof assistants. In any case, I come from other proof assistant communities and only have one drive-by contribution to make for now (a simplification of Mathlib/Algebra/Order/Ring/Defs.lean based on https://proofassistants.stackexchange.com/a/4762/).

[Jean Abou Samra]

To summarize, my setup is working (I just have to remain in mathlib4 and open files from there), and my question at this point is whether I should open a bug report for the fact that lake serve expects to be started in the project root (as my understanding is that this is contrary to normal behavior for LSP servers).

[Kevin Buzzard]

Before you waste too much time on this (based on reading the stackexchange post you linked to): if your proposal is to make some change to the order that things are done in the typeclass inference system then you might want to run the idea past the community before making the PR, because there are reasons it's set up the way it's set up, and I suspect that there won't be too much interest in a change which e.g. will make mathlib compile far slower but which will remove the use of an axiom when defining an identity map.

[Kevin Buzzard]

You might want to read the parts about "preferred" typeclass paths in https://arxiv.org/pdf/2306.00617 for example.

[Patrick Massot]

I understand people who don’t want to use VSCode, but if you use helix then you should use neovim when editing Lean code. You won’t be far from the kind of editing experience you like like but you will have almost full editor plugin features.

[Jean Abou Samra]

@Kevin Buzzard Thanks for the warning. I wanted to make a very simple change, but it's turning out a lot more complicated than I anticipated so I think I will give up on this one.

[Eric Wieser]

I think the proposed change to docs#StrictOrderedRing.toStrictOrderedSemiring is harmless, but also of minimal value