Sphinx try it! with leanprover-community web editor

Stream: general

[Kevin Buzzard]

I have some Sphinx notes which use the same set-up as TPIL, and in particular there is Lean code with "Try it!" and people can click on "Try it!" and get taken to the official Lean web editor.

I wanted to direct them instead to the Leanprover-community web editor, for better mathlib, so I changed a line in lean_sphinx.py : I changed this line

https://github.com/leanprover/theorem_proving_in_lean/blob/48e7584a01559530c2a4273a9094c62d3b00ccd4/lean_sphinx.py#L24

from uri = 'https://leanprover.github.io/live/3.4.1/#code=' to uri = 'https://leanprover-community.github.io/lean-web-editor/#code=' and crossed my fingers. A simple test indicated that it worked, and it was only later when it was deployed and students were using it that I realised it wasn't working :-/ Only the first line of code was passed to the web editor; the rest was being lost. So is there some slight syntax difference between what the two web editors are expecting?

[Kevin Buzzard]

For example compare this (working) with this (not working). The only difference is that I compiled with the URL change in lean_sphinx.py -- the working one is Jeremy's version pointing to the classical Lean web editor, and the broken one creates links to the community web editor...which don't work :-(

[Kevin Buzzard]

Just click on "Try it!" in any of those files to see the phenomenon.

[Bryan Gin-ge Chen]

I can look into this. I think I changed the way that the code in the URL gets (un)escaped, and apparently newlines = signs are encoded differently.

[Bryan Gin-ge Chen]

See if changing this line to this works:

    uri += urlquote(code, safe='~()*!.\'')

[Bryan Gin-ge Chen]

Equals signs have to be %-encoded in the code URLs for the new web editor since it allows having either code=something or url=something in the hash params of the URL.

[Kevin Buzzard]

Yes, I thought it was newlines, but you're right: my lines often end with := and it's the = that gets truncated. Many thanks @Bryan Gin-ge Chen for moving so fast on this! I'll chase this up again in a few days' time so I'm ready for this coming Thursday.