Lean4 LSP documentation? Want to make a "diagram chaser".

Stream: lean4

[Daniel Donnelly]

Hello! I want to either interact with Lean4 (or Coq) and the user's Lean4 files using a Web Extension for VSCode and a WebView. Would the widgets extension do what I need? I basically need an iframe capability and that iframe will load Quiver CD editor: https://q.uiver.app either locally or remote, but I have experience loading it locally in a Django template. It would be nice to use the latest https://q.uiver.app without editing its source code, because varkor the author is always adding features to it. Anyway, some guidance would be appreciated. Any idea where I can find more info about the LSP interface used by Lean4 to communicate with VSCode? What I will do is compare that to Coq's documentation, and determine which one would be easiest to get working first. Eventually both PA's would be supported. Ideally, I would like the user to be able to draw a commutative diagram in Quiver and have code be automatically generated that creates those objects in Lean4. I don't care if this is extremely difficult to do. I don't care if I'm restricted to R-modules, whatever I can do in this area, I really want to make happen. This would fall under a "Visual Diagram Chasing" software category.

[Wojciech Nawrocki]

The widget system is exactly what enables this kind of use case :) the tutorial is your best bet. Btw, I am working on showing but not editing diagrams here

[Kevin Buzzard]

Ideally, I would like the user to be able to draw a commutative diagram in Quiver and have code be automatically generated that creates those objects in Lean4. I don't care if this is extremely difficult to do.

That's a great attitude, but I also suspect that this will be possible to do (from what I've seen of Lean 4), so I'm super-keen to see what you can come up with!

I don't care if I'm restricted to R-modules

I don't think you will be -- we have a working theory of diagrams in arbitrary abelian categories (as well as a proof that R-modules are an abelian category), which we had to build for, amongst other things, the liquid tensor experiement.

This would be a much-needed feature. If you look around in Lean 3's maths library you will see that right now it's a huge mouthful to state things like the snake lemma (just a huge list of maps and then a list of statements that various compositions equal other compositions). Any way of packaging these things up in a more visual way would be brilliant.

[Daniel Donnelly]

Wojciech Nawrocki said:

The widget system is exactly what enables this kind of use case :) the tutorial is your best bet. Btw, I am working on showing but not editing diagrams here

That is awesome! I will look into those today.

[Daniel Donnelly]

Kevin Buzzard said:

Ideally, I would like the user to be able to draw a commutative diagram in Quiver and have code be automatically generated that creates those objects in Lean4. I don't care if this is extremely difficult to do.

That's a great attitude, but I also suspect that this will be possible to do (from what I've seen of Lean 4), so I'm super-keen to see what you can come up with!

I don't care if I'm restricted to R-modules

I don't think you will be -- we have a working theory of diagrams in arbitrary abelian categories (as well as a proof that R-modules are an abelian category), which we had to build for, amongst other things, the liquid tensor experiement.

This would be a much-needed feature. If you look around in Lean 3's maths library you will see that right now it's a huge mouthful to state things like the snake lemma (just a huge list of maps and then a list of statements that various compositions equal other compositions). Any way of packaging these things up in a more visual way would be brilliant.

Thank you for the positive feedback! I really want to chase diagrams with a computer. I always mess them up on paper. :)

[Daniel Donnelly]

@Wojciech Nawrocki What is preventing you from rendering object / arrow labels with KaTeX? I have experience getting KaTeX called from a Qt/C++ application. Maybe with enough unicode support, such a thing is not really necessary. But a button to output to Quiver format would be nice. Quiver (https://q.uiver.app) would in turn export to TikzCD which it does already, so you could design your theory in Lean4 and then publish to paper without having to manually edit text of diagrams which is meant to be a visual editing experience. Also, I have made several diagram editors so far in my own research, and I found the best way to get things to look right is to align everything to a fixed grid as Quiver does. If you want to support 3D-looking diagrams, you simply change the grid to isometric tiling (or something like that).

[Daniel Donnelly]

@Wojciech Nawrocki How does one get/git your code for that? Might as well not re-invent the wheel :)

[Daniel Donnelly]

image.png

Lean4 is not recognizing widget...

[Mauricio Collares]

Are you using a recent version of Lean (4.0.0-m5 or a recent nightly)? What's the error message you're getting?

[Mauricio Collares]

If so, try adding

import Lean.Widget
open Lean Widget

to the start of your sample code

[Daniel Donnelly]

Mauricio Collares said:

If so, try adding

import Lean.Widget
open Lean Widget

to the start of your sample code

image.png

Tried adding that import (2 lines), and error message is:

unknown attribute [widget]

[Daniel Donnelly]

Also on gitpod the Rubiks cube example shows nothing when I hover over #widget

[Mauricio Collares]

I think those are two separate errors: Your test1.lean file is not accompanied by a lean-toolchain file, so you're probably getting an old version of Lean when executing your sample, which is independent of the Rubik's cube sample.

The Rubik's cube sample is not working for the opposite reason: Its lean-toolchain file was recently updated to a "too new" version, and this wasn't caught because this particular sample is, as far as I can tell, not tested by CI (cc @Chris Lovett).

[Daniel Donnelly]

How do I add a lean-toolchain file and why didn't the widgets doc say to do this? :/

[Mauricio Collares]

The previous version of Lean used was leanprover/lean4:nightly-2022-08-08, so if you replace the lean-toolchain file by a single line containing leanprover/lean4:nightly-2022-08-08 the Rubik's cube example should work.

[Mauricio Collares]

I think the doc doesn't mention it because it assumes your "default" lean version is new enough.

[Mauricio Collares]

Can you hit Ctrl+Shift+P and then type "Select Lean Toolchain"? If that works (I am not a VSCode user, sorry), then selecting a new enough toolchain should make your test1.lean file work. You can also create a lean-toolchain file with a single linbe containing a particular Lean version (in the above format).

[Daniel Donnelly]

image.png

[Daniel Donnelly]

object file 'c:\Users\fruit\.elan\toolchains\leanprover--lean4---nightly-2022-08-08\lib\lean\Init.olean' of module Init does not exist

[Daniel Donnelly]

Mauricio Collares said:

Can you hit Ctrl+Shift+P and then type "Select Lean Toolchain"?

No such tools found in the command pallete

[Edward Ayers]

make sure you are in a lean file

[Daniel Donnelly]

Still same issue - last mentioned error message:

object file 'c:\Users\fruit\.elan\toolchains\leanprover--lean4---nightly-2022-08-08\lib\lean\Init.olean' of module Init does not exist

[Edward Ayers]

can you change import Lean.Widget to import Lean

[Mauricio Collares]

I am stumped, because this file definitely exists in the corresponding nightly archive. Maybe the Windows experts know what's going on (hopefully @Edward Ayers's suggestion works). I would just try a different nightly version (the next day's, say).

[Edward Ayers]

Just to double check, you are using this extension: https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

[Daniel Donnelly]

@Edward Ayers I'm using the Lean4 that comes up in extensions and it's updated to the latest version.

[Edward Ayers]

What does #eval Lean.versionString give?

[Edward Ayers]

Should be "4.0.0-nightly-2022-08-08"

[Daniel Donnelly]

@Edward Ayers 4.0.0-nightly-2022-08-09 because I just changed by one day a second ago.

[Edward Ayers]

ok but did you get that from #eval?

[Edward Ayers]

Sometimes vscode can be using a different version if it was manually set with "Select Lean Toolchain"

[Daniel Donnelly]

image.png
I think it's working now . No errors. Is that the normal operation for this helloworld example?

[Edward Ayers]

add the line #widget helloWidget .null

[Edward Ayers]

click on the #widget

[Daniel Donnelly]

@Edward Ayers yes I see that in the docs now. It works! :D

[Edward Ayers]

nice!

[Daniel Donnelly]

image.png

[Edward Ayers]

great!

[Daniel Donnelly]

So how would I start development on that CD editor by @Wojciech Nawrocki ?

[Daniel Donnelly]

viewer

[Daniel Donnelly]

I'm unsure how to get the code going by that "commit page" here: https://github.com/leanprover-community/mathlib4/pull/363

[Edward Ayers]

I think pull the branch for his PR, confirm that you can view the diagrams and then start hacking :)

[Mauricio Collares]

(deleted)

[Edward Ayers]

Daniel Donnelly said:

I'm unsure how to get the code going by that "commit page" here: https://github.com/leanprover-community/mathlib4/pull/363

you need to add his fork as a remote and then check it out

[Daniel Donnelly]

@Edward Ayers So I use TortoiseGit to clone it, but are there instructions on how to install the extension (another dev version of it) into vscde?

[Edward Ayers]

# do this in your mathlib4 directory
git remote add vtec git@github.com:Vtec234/mathlib4.git
git fetch vtec
git checkout squares

[Edward Ayers]

Daniel Donnelly said:

Edward Ayers So I use TortoiseGit to clone it, but are there instructions on how to install the extension (another dev version of it) into vscde?

You don't need a different version of the vscode extension

[Daniel Donnelly]

@Edward Ayers where do I do that from? VScode?

[Daniel Donnelly]

I tried from Git Bash in windows, and it said I'm not in a git repo

[Edward Ayers]

yeah you need to get mathlib4 first

[Daniel Donnelly]

I see, I see, let me google for it

[Edward Ayers]

So in a folder where you want to put mathlib, do this:

git clone git@github.com:leanprover-community/mathlib4.git
cd mathlib4
git remote add vtec git@github.com:Vtec234/mathlib4.git
git fetch vtec
git checkout squares
code .

[Daniel Donnelly]

I downloaded it. But how then do I tell VScode to use that copy of mathlib?

[Wojciech Nawrocki]

Daniel Donnelly said:

Wojciech Nawrocki What is preventing you from rendering object / arrow labels with KaTeX? I have experience getting KaTeX called from a Qt/C++ application. Maybe with enough unicode support, such a thing is not really necessary. But a button to output to Quiver format would be nice. Quiver (https://q.uiver.app) would in turn export to TikzCD which it does already, so you could design your theory in Lean4 and then publish to paper without having to manually edit text of diagrams which is meant to be a visual editing experience. Also, I have made several diagram editors so far in my own research, and I found the best way to get things to look right is to align everything to a fixed grid as Quiver does. If you want to support 3D-looking diagrams, you simply change the grid to isometric tiling (or something like that).

Note that the object/arrow labels are Lean expressions, and they are interactive (you can click to see the type, go to definition, etc.). Rendering general Lean expressions as LaTeX would be a larger project.

[Wojciech Nawrocki]

See the last sentence here for why I didn't use Quiver.

[Edward Ayers]

Daniel Donnelly said:

I downloaded it. But how then do I tell VScode to use that copy of mathlib?

develop in mathlib4 directly is the easiest way (hit code . in your mathlib4 folder)

[Daniel Donnelly]

brb

[Daniel Donnelly]

@Edward Ayers everything seems to be working with your commands except:

$ git fetch vtec
git@github.com: Permission denied (publickey).
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.

What public key do I edit on github? I could generate a new one with puttygen

[Daniel Donnelly]

It's weird because I've been gitting code all day, and for some reason for this it doesn't work.

[Wojciech Nawrocki]

You could git remote set-url vtec https://github.com/Vtec234/mathlib4

[Daniel Donnelly]

@Wojciech Nawrocki wow that worked! I will keep a note file for me with all these commands ...

[Mauricio Collares]

(Off-topic: Why would the clone work over SSH but not the fetch? Sure, different remotes, but they're both github repos)

[Wojciech Nawrocki]

Basically the git protocol requires authentication, whereas https only requires it for pushing

[Daniel Donnelly]

@Wojciech Nawrocki I have written an ArrowStyle class in PyQt5 for a diagram editor of mine (not ready to release), but the arrow styles work beautifully. I don't know if that would help here other than I could possibly translate the code over to JS

[Daniel Donnelly]

It supports up to 3 lines, bezier, up to 6 heads, veetail, and dashed/dotted lines for "there exists".

https://youtu.be/TSTdyRDvSss Arrow styling starts at 1:20

[Wojciech Nawrocki]

Arrow styles would be great! To make that work with my widget, you'd indeed need to translate these to some JS code which generates the SVG for Penrose to use

[Daniel Donnelly]

Wojciech Nawrocki said:

Arrow styles would be great! To make that work with my widget, you'd indeed need to translate these to some JS code which generates the SVG for Penrose to use

I'll make a ToDo list for myself. I think though that perhaps the style should be optional, but a double head will always mean epimorphism, or something like that, if present.

[Daniel Donnelly]

@Wojciech Nawrocki so how do I test your code? For example where do I place a lean4 test file or is there an example already somewhere within mathlab4?

[Daniel Donnelly]

Well we shouldn't constrain the artistry of the user. Maybe a double headed arrow could mean other things, but we should have some defaults, and the epimorphism default maps of course to the standard double headed arrow.

[Wojciech Nawrocki]

You need to run lake build widgetCommDiag in the mathlib4 directory (this needs node.js installed), and then you can open CommDiag.lean

[Daniel Donnelly]

Wojciech Nawrocki said:

You need to run lake build widgetCommDiag in the mathlib4 directory (this needs node.js installed), and then you can open CommDiag.lean

That worked except I'm clicking around on the CommDiag.lean file and am getting:
Error updating: Error fetching goals: Rpc error: InvalidParams: Incorrect position 'file:///c%3A/Users/fruit/OneDrive/Desktop/Lean4Widgets/mathlib4/Mathlib/Tactic/Widget/CommDiag.lean:175:10' in RPC call.

Once I have it working, what do I do to display something in the infoview?

[Daniel Donnelly]

Will come back to this later. I have to help watch my grandma for a few hours.

[Wojciech Nawrocki]

Daniel Donnelly said:

Wojciech Nawrocki said:

You need to run lake build widgetCommDiag in the mathlib4 directory (this needs node.js installed), and then you can open CommDiag.lean

That worked except I'm clicking around on the CommDiag.lean file and am getting:
Error updating: Error fetching goals: Rpc error: InvalidParams: Incorrect position 'file:///c%3A/Users/fruit/OneDrive/Desktop/Lean4Widgets/mathlib4/Mathlib/Tactic/Widget/CommDiag.lean:175:10' in RPC call.

Once I have it working, what do I do to display something in the infoview?

At the top of the file there is an #exit statement that you have to remove, then it should work. There are examples at the bottom which display a diagram.

[Daniel Donnelly]

@Wojciech Nawrocki what version (nightly) of Lean4 are you using to develop with? I think it's best to match these, and also:
image.png

cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains errors is the error - all code up to the first widget declaration works, and then @ [widget] is underscored with red.

[Wojciech Nawrocki]

What is the error on line 47? When you have mathlib4 open as a folder in vscode, it should always use the right version of Lean as specified in lean-toolchain

[Chris Lovett]

Hi Daniel, I just updated to latest mathlib4 which is using leanprover/lean4:nightly-2022-09-05 and and tried what you are doing, and it compiles fine, but you will get that error if the javascript file you are pointing to doesn't exist. If this is the problem the error on line 47 should say "no such file or directory (error code: 2)".

image.png