Nota

Stream: general

[Bryan Gin-ge Chen]

From https://willcrichton.net/nota/

Papers about programming languages involve complex notations, systems, and proofs. Static PDFs offer little support in understanding such concepts. I describe Nota, a framework for academic papers that uses the browser's interactive capabilities to support comprehension in context. Nota uses hover effects, tooltips, expandable sections, toggleable explanations, and other interactions to help readers understand a language's syntax and semantics. I demonstrate the use of Nota by rewriting a PL paper using its primitives, and also by writing this paper in Nota.

Repo is here: https://github.com/willcrichton/nota

I don't know if this will be immediately useful for anything Lean-related, but it might give some inspiration for the folks here who are interested in browser / VS Code interfaces for code / math. (Also, Lean got a mention at the end in the section on alternatives: "Perhaps the future for PL is literate Agda/Lean/Coq programs.")

[Johan Commelin]

Wow, that looks really slick!