License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.24
URN: urn:nbn:de:0030-drops-183991
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18399/
Nawrocki, Wojciech ;
Ayers, Edward W. ;
Ebner, Gabriel
An Extensible User Interface for Lean 4
Abstract
Contemporary proof assistants rely on complex automation and process libraries with millions of lines of code. At these scales, understanding the emergent interactions between components can be a serious challenge. One way of managing complexity, long established in informal practice, is through varying external representations. For instance, algebraic notation facilitates term-based reasoning whereas geometric diagrams invoke spatial intuition. Objects viewed one way become much simpler than when viewed differently. In contrast, modern general-purpose ITP systems usually only support limited, textual representations. Treating this as a problem of human-computer interaction, we aim to demonstrate that presentations - UI elements that store references to the objects they are displaying - are a fruitful way of thinking about ITP interface design. They allow us to make headway on two fronts - introspection of prover internals and support for diagrammatic reasoning. To this end we have built an extensible user interface for the Lean 4 prover with an associated ProofWidgets 4 library of presentation-based UI components. We demonstrate the system with several examples including type information popups, structured traces, contextual suggestions, a display for algebraic reasoning, and visualizations of red-black trees. Our interface is already part of the core Lean distribution.
BibTeX - Entry
@InProceedings{nawrocki_et_al:LIPIcs.ITP.2023.24,
author = {Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel},
title = {{An Extensible User Interface for Lean 4}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {24:1--24:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18399},
URN = {urn:nbn:de:0030-drops-183991},
doi = {10.4230/LIPIcs.ITP.2023.24},
annote = {Keywords: user interfaces, human-computer interaction, Lean}
}
