LeanInk/Alectryon

Stream: lean4

[Sebastian Ullrich]

That the state on <;> is different from that on the preceding tactic should be considered a bug in Lean 4 itself. If we fix it, LeanInk should automatically remove the bubble in front of the operator.

[Sebastian Ullrich]

Eric Rodriguez said:

maybe a green-colour bubble is good to signal that it's not got any state information?

That's a nice idea, though it would need an Alectryon extension

[Arthur Paulino]

Can we move the Alectryon/LeanInk discussion to another thread? I think it deserves it.
Another issue that I found is when reading on a smartphone, in which hovering is just impossible (and a big chunk of the screen is taken by a white block that shows nothing)

[Eric Rodriguez]

funnily enough, I was just looking to see how easy my idea of green blobs would be, and saw that that is by design, Arthur:
image.png

[Sebastian Ullrich]

Note that the Alectryon default style is centered, we chose windowed because it makes better use of wide screens. Definitely not the right default for smartphones though, yes.

[Sebastian Ullrich]

Not sure @Niklas Bülow considered smartphones when implementing the type hover, I definitely didn't :)

[Eric Rodriguez]

I think this was Clément's code, unless the styling was changed in LeanInk

[Sebastian Ullrich]

The hover code is not new, yes, but it's not an issue for goals since you can just click on them instead. Which is not true for the type hover extension.

[Arthur Paulino]

My concern is that some types of content require different focuses. Being able to see tactic states might be useful when the focus is on the Lean code itself, with the help of the text for the reader to understand the code. This is ideal for teaching, for example.

Reading books like TPIL4 or the Lean 4 Manual is a very different experience though. Alectryon/LeanInk might feel a bit distracting when the focus is on the text itself and the Lean code blocks play a minimal role and don't really have that much to be shown by the hovering feature

[Gabriel Ebner]

Note that the Alectryon default style is centered, we chose windowed because it makes better use of wide screens. Definitely not the right default for smartphones though, yes.

The first thing I did when trying it out was to switch back to centered mode. The windowed version is very distracting because it follows the mouse cursor so it flickers a lot. And you can't even scroll the right pane because the goal state is gone once you move the mouse there (not that the scrolling works with centered mode). Apparently you can disable the hovering, but then you can't see the goals at all.

At least on firefox, the hypotheses have a weird row-wrapping layout, where you can have a small single-hypothesis on the right of a large multi-line hypothesis. (On chromium, the hypotheses are layed out vertically as expected. Not sure why this is different.)

There also seem to be some performance issues. One of the other files (Formal.html) takes more than 10 seconds to load on my machine (it's also three megabytes large).

The vertical scrollbar looks like a bug.

Copy/paste doesn't work (the pasted text contains newlines after every token). On chromium triple-click doesn't work and only selects a few characters (on firefox it selects the whole line).

It would be great if it also showed term-mode goals.

[Gabriel Ebner]

All of the hovers could benefit from a short delay before opening automatically (like the hover in vscode).

[Gabriel Ebner]

The type hovers should probably show the full name, and not .plus : ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (plus a b) Ty.nat. (see also: newlines from copy/paste)

[Gabriel Ebner]

This is probably in the works already, but go-to-definition would be very welcome.

[Sebastian Ullrich]

At least a few in there that we can address directly in LeanInk instead of in Alectryon, yay :sweat_smile: . Though the term goals would likely exacerbate the performance issues. We should probably give the experimental minification flag a try. https://github.com/cpitclaudel/alectryon#reducing-page-and-cache-sizes-experimental

[Leonardo de Moura]

@Gabriel Ebner Yes, the issues you have described above are quite annoying. I don't know how long it will take to fix them, but it would be great if we could decide on a common format for writing new documentation. It would be great if we could make this decision independently of the system we use to convert our docs into web pages. For tutorial-like examples, I found a .lean file with text in comments way more pleasant to write than a .md file with quoted lean code. When we talked with Clement, he mentioned that he uses some Emacs magic that switches between the two modes. I would love to have that working on our VS Code and Emacs modes. I would also love to have tools that convert the file https://github.com/leanprover/lean4/blob/master/doc/examples/tc.lean into an input file for mdbook, sphynx, and whatever we decide to use to render it.
Another possible direction for interacting with the documentation while we read it is VS Code. I think this scenario is very attractive because we cannot only visualize the types and tactic state, but also modify the examples.

[Matthew Ballard]

Open VS Code-Server seems like it might be useful along those lines

[Gabriel Ebner]

but it would be great if we could decide on a common format for writing new documentation. It would be great if we could make this decision independently of the system we use to convert our docs into web pages.

:+1: I didn't look at the leanink syntax until now. The first thing I noticed is that it uses both a new comment syntax /-| as well as a new markup language (reStructuredText), duplicating the /-! syntax with the markdown markup. Is there a chance we could standardize on one syntax and markup language?

Note that we need markdown support in leanink/alectryon anyhow to render doc strings (which I assume we want).

I think we should also standardize the markup with the doc-gen extensions. (Thinking of latex formulas and links to Lean declarations here.)

[Leonardo de Moura]

Is there a chance we could standardize on one syntax and markup language?

Yes, of course.

Note that we need markdown support in leanink/alectryon anyhow to render doc strings (which I assume we want).

Yes, we do.

I think we should also standardize the markup with the doc-gen extensions. (Thinking of latex formulas and links to Lean declarations here.)

Yes, that would be great.

[Gabriel Ebner]

For tutorial-like examples, I found a .lean file with text in comments way more pleasant to write than a .md file with quoted lean code.

You're not the only one. All the exercises in Jasmin's course are written in this way (with the text in module doc strings). The latest version of mathematics in lean also follows this approach. I think both of them use some preprocessing to separate the master file into lecture notes / exercise files / solutions though.

[Gabriel Ebner]

When we talked with Clement, he mentioned that he uses some Emacs magic that switches between the two modes.

I'm not completely sure what the advantages of this switching are. We already have syntax highlighting for nested markdown blocks in vscode, and converting the file to markdown won't give us much more than that. We could add a preview command (like the markdown extension).

Maybe we can do something more fancy once this lands: https://github.com/microsoft/vscode/issues/85682

[Eric Rodriguez]

My thoughts for this in the Lean3 extension for VSCode (that I didn't get around to do) was a spit view, a la Markdown writing/preview. Non-trivial to implement in the VSCode extension, though.

[Leonardo de Moura]

@Gabriel Ebner Any suggestions for an initial standard for syntax and markup language?

[Gabriel Ebner]

Another possible direction for interacting with the documentation while we read it is VS Code. I think this scenario is very attractive because we cannot only visualize the types and tactic state, but also modify the examples.

We have already been moving a bit into that direction with https://github.com/leanprover/vscode-lean4/issues/47 Integrating the docview with the generated documentation is a good idea. You get the example source code in one tab, and the rendered documentation in the other tab.

This would also reduce the need for the (slow and limited) javascript version. Instead of opening each code snippet in the javascript version, we could open the whole documentation in a gitpod/codespaces container.

[Sebastian Ullrich]

Gabriel Ebner said:

I'm not completely sure what the advantages of this switching are.

Clement mentioned further features of the Markdown major mode such as a navigable document outline. And yes, I did mention we could in theory have the Lean language server report the Markdown document structure :) .

[Gabriel Ebner]

Any suggestions for an initial standard for syntax and markup language?

I think it would be best to take what we already have. That is, /-! comments and markdown.

[Sebastian Ullrich]

I didn't actually know we accepted multiple module docstrings in a file when Niklas started working on Lean 4 support for Alectyron, until it came up in the context of doc-gen4. "Module docstring" and "literate comment" has slightly different connotations for me, but being able to use both meanings separately in a single file does not seem like an important use case.

[Gabriel Ebner]

Practically speaking, mathlib already uses module doc strings as a form of literate programming (in the sense that it interleaves code with explanatory text). https://leanprover-community.github.io/mathlib_docs/order/conditionally_complete_lattice.html#complete-lattice-structure-on-codewith_top-with_bot-%CE%B1code

[Leonardo de Moura]

Gabriel Ebner said:

Practically speaking, mathlib already uses module doc strings as a form of literate programming (in the sense that it interleaves code with explanatory text). https://leanprover-community.github.io/mathlib_docs/order/conditionally_complete_lattice.html#complete-lattice-structure-on-codewith_top-with_bot-%CE%B1code

Are the /-! comments always being rendered at the top of the page?

[Gabriel Ebner]

No, as you can see in the link they are interleaved with the declarations (which appear in the source file order).

[Leonardo de Moura]

Nice.

[Matthew Ballard]

Gabriel Ebner said:

This would also reduce the need for the (slow and limited) javascript version. Instead of opening each code snippet in the javascript version, we could open the whole documentation in a gitpod/codespaces container.

Would someone need a gitpod/codespaces subscription to access it?

[Gabriel Ebner]

I think gitpod has a free tier which should be enough for casual users. As far as I know, code spaces is still in semi-private beta.

[Matthew Ballard]

Gitpod spun off their browser-based VS Code into an open source project.

[Matthew Ballard]

Would a self-hosted playground-style server with this as the frontend be feasible? It seems like it would be lower friction for curious users.

[Gabriel Ebner]

Yes, the purpose of having a hosted vscode version is to lower friction. You can always clone the repo yourself and run it on your local vscode. The target audience is precisely those users who want to know more about Lean, but don't want to bother with a local installation.

[Gabriel Ebner]

I'm not sure if we can handle more users with a self hosted version than with the free tier though.