Blog post doing crazy things with Lean InfoView?

Stream: general

[samuela]

IIRC there was a blog post floating around a few months ago in which an absolute madlad succeeded in completing all kinds of shenanigans with Lean InfoView widgets, including but not limited to playing a video. However, I am now failing to find the link. Does anyone else recall this and have the link by any chance?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Maybe https://unnamed.website/posts/bad-apple-lean-tactic/?

[samuela]

Yes, exactly!

[samuela]

Thank you!

[Floris van Doorn]

I'm glad that Lean has reached the Bad Apple stage of adoption.

I tried to run some code locally and to play an embedded video in the widget, but it's not working for me. A video element loads, but the video doesn't:
image.png
(it loads fine in my browser).

[Eric Wieser]

This might be a cross-origin issue, where you can't load the video from a local file

[Floris van Doorn]

For those that are confused about what's going on in this thread: there's a random internet meme/challenge to get some random black-and-white video (called "Bad Apple") to run on all kinds of software and hardware that were explicitly not designed for displaying videos.

[Niels Voss]

I particularly like this quote from the article: "One thing that Lean surprisingly excels at is the editor experience. It’s like an interactive Jupyter notebook and the infoview displays a lot of useful real-time information about types and tactic states." I wonder how much more is required from the UI side to make Lean like running a Juypter notebook.

[Shreyas Srinivas]

This is not surprising to ITP users (even here, lean is leagues ahead of other ITPs imo). But in the rest of the programming world, you have to go through this manual process of loading files into a REPL program in a terminal, and explicitly running commands to extract many pieces of information, that lean infoview gives right away

[Shreyas Srinivas]

There was/is a lean 4 Jupyter kernel. As far as I can tell, it never got widespread adoption.