Map of monads

Stream: mathlib4

[Adam Topaz]

It seems that our Lean4 monad map isn't rendering very well: https://github.com/leanprover-community/mathlib4/wiki/Monad-map

At least on my computer (with firefox), I see many of the nodes rendered as plaintext html tags. Is anyone else seeing a similar issue?

[Damiano Testa]

I see the plaintext html tags also on Chrome on my mobile (Android).

[Adam Topaz]

Is this just an issue with how github renders markdown?

[Eric Rodriguez]

did this use to work?

[Adam Topaz]

it did. But I assume that github's markdown rendering engine changed.

[Eric Wieser]

Yeah, it looks like a mermaid update, GitHub bug, or stricter escaping rules broke this

[Thomas Murrills]

It seems like using mermaid's click functionality for nodes instead of html or markdown provides a partial workaround? Weirdly, I get a clickable hand and a tooltip showing the link, but clicking doesn't work. However, command-clicking does work. Not sure what to make of that...I'm asking on the mermaid discord server.

[Thomas Murrills]

In the meantime it also seems there's also a github discussion about the issue.

[Thomas Murrills]

For the time being I updated it to use the partially-working click functionality (meaning you have to command/ctrl click to follow the link) so that it's at least readable. :)

[Eric Wieser]

Perhaps it's time to migrate this to the docs

[Eric Wieser]

Where we can presumably load mermaid without the security restrictions

[Damiano Testa]

With Chrome on Linux, the Monad map is again not working:

Unable to render rich display

Lexical error on line 20. Unrecognized text.
... MetaM -. TermElabM.run ..- TermElabM;
-----------------------^

For more information, see https://docs.github.com/get-started/writing-on-github/working-with-advanced-formatting/creating-diagrams#creating-mermaid-diagrams

[Thomas Murrills]

Fixed :) (At least, on Firefox on Mac. But I think this was due to a change on github's end anyway.)

[Damiano Testa]

Thanks! It is fixed for me too!

[Thomas Murrills]

GitHub notified me (via discussion update) that anchor links are working again for mermaid! :) I updated the monad map so that

1. all nodes have links
2. all edge labels have links (new)
3. all links point directly to the docs page for that declaration instead of a search query for the declaration

[Thomas Murrills]

Also, apparently Simp.M no longer exists (there used to be both Simp.M and SimpM), so I removed it. (SimpAll.M still exists, but I figured the map was good enough without it.)

[Thomas Murrills]

Going from a declaration to a URL might exist somewhere in docgen, but in case the map needs to be updated at some point, here's the quick code I used to generate anchors (#docs_url is included just for completeness):

import Lean
import ImportGraph.RequiredModules

open Lean Elab Command

def toDocsURL (n : Ident) : CommandElabM String := do
  let n ← resolveGlobalConstNoOverload n
  let some module := (← getEnv).getModuleFor? n
    | throwError "could not find module for {n}"
  let path := module.toStringWithSep "/" true
  return "https://leanprover-community.github.io/mathlib4_docs/" ++ path ++ ".html#" ++ n.toString

elab "#docs_url " n:ident : command => do logInfo (← toDocsURL n)

-- Note: ident's are printed as strings with a leading "`", so drop it
elab "#anchor " n:ident : command => do logInfo <|
  "<a href='" ++ (← toDocsURL n) ++ "'>" ++ (s!"{n}</a>").drop 1

[Eric Wieser]

You can find out that "somewhere" by looking at where docs#Nat leads to (before the redirect)

[Thomas Murrills]

Ah, ok—simply fully resolving the name would have been enough, then! (It's easy to move to ?pattern= style with a regex replacement, but it turns out the redirect takes a second extra when following the link—so I figure I'll leave it as is, at the cost of slightly busier source for that diagram. Hopefully none of these declarations will be moving very soon. :) )