Dynkin diagrams

Stream: general

[Oliver Nash]

I just spent the morning messing around with our VS code widget for the first time. I can't really justify spending any more time on this since it's just a toy but I thought I'd share what I have in case someone else fancies picking up where I've left off.

[Oliver Nash]

The following gist https://gist.github.com/ocfnash/fb61a17d0f1598edcc752999f17b70c6 (which works against Mathlib master) allows you to create pictures like this:

[Oliver Nash]

image.png

[Oliver Nash]

Perhaps some small room for improvement when it comes to styling ;-)

[Oliver Nash]

Just to emphasise the point: this is Lean reading our Mathlib definition for the Dynkin diagram of E₈ and rendering it.

[Eric Wieser]

I thought about this when looking at your PR, but thought "there's no way Oliver will want to spend the time on that"!

[Eric Wieser]

Is there a way to tell lean "use this widget view in the goal state"?

[Gabriel Ebner]

Eric Wieser said:

Is there a way to tell lean "use this widget view in the goal state"?

Not at the moment. But the goal state is defined in mathlib, so you can contribute a PR. :smile:

[Mario Carneiro]

you can use a custom tactic mode

[Eric Wieser]

Another thing that would be cool would be to somehow take the output of a #html command and insert it into doc-gen - or even allow docstrings to contain such a command which is parsed and executed by doc-gen

[Eric Wieser]

There's a lean4 example that adds a DSL for html, https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/Webserver.lean#L162-L165.

How hard would it be to write an HTML parser in lean3 meta? I know it's harder than the lean4 approach, and I think docs#lean.parser isn't up to the job, but presumably docs#parser would be.

I don't think we can support that syntax in lean3, but something like html!"<div>${some_var}</div>" would be almost as good.

[Oliver Nash]

Oh wow, Lean 4 really is full of treats. I have no idea how hard it would be to do something along the lines of what you suggest in Lean 3.

[Mario Carneiro]

There is a format! macro in lean 3 that does a simpler version of this

[Eric Wieser]

The format! does parsing character by character using pattern matching, which feels way more painful than a monadic approach using docs#parser

[Mario Carneiro]

you sure about that?

meta def foo (baz : format) := format!"bla {baz}"
#print foo
-- meta def foo : format → format :=
-- λ (baz : format), id_rhs format (to_fmt "bla " ++ to_fmt baz ++ to_fmt "")

It uses character parsing in order to parse the expression, but the generated code is just string appends

[Mario Carneiro]

In this case you would be using a format! like macro for the frontend, which uses docs#parser to parse the expression and produces appropriate applications of html constructors

[Mario Carneiro]

format! doesn't need any fancy parsing because it's just looking for uses of {

[Eric Wieser]

I think I meant to say what you said. Yes, the parser should be building a pexpr not an html object

[Wojciech Nawrocki]

Hello, I ported this to Lean 4 :) The server-side code is here and it looks like this. PR TBD

[Oliver Nash]

Nice work!

[Yaël Dillies]

Do you think we could adapt this to Hasse diagrams (representing orders)?

[Oliver Nash]

It could certainly be done for appropriate values of "we".

[Eric Wieser]

Am I right in saying that drawing a hasse diagrams is essentially just a task of drawing a directed graph from a boolean adjacency matrix?

[Eric Wieser]

In which case, my response would probably be "just output some stuff for graphviz, because graph layout is hard and probably out of scope"

[Alex J. Best]

For import graphs we have a super simple implementation of graphviz output at https://github.com/alexjbest/dag-tools/blob/master/src/dag.lean#L39
It would be really really cool if it was possible to load external js in the widget view to render this automatically, but unfortunately this seems quite hard due to various security type features of vscodes web views

[Yaël Dillies]

Outputting stuff for graphviz should work out. Is going through the adjacency relation how the Dynkin stuff works?

[Oliver Nash]

Sort of but it's pretty hacky. The function get_edge_html consumes a pair of natural numbers representing two nodes and returns a list of edges (which in this case is always of length 0 or 1).