Für viele moderne Programmiersprachen existieren weitgehende Möglichkeiten, um Code aus dem Editor heraus zu analysieren und erforschen, wie zum Beispiel der Anzeige projektweiter Referenzen eines Bezeichners. Während das Language Server Protocol es relativ einfach macht, solche Daten in verschiedenen Editoren zu präsentieren, kann das Sammeln dieser Daten über die verschiedenen Dateien eines Projekts hinweg weiterhin eine Herausforderung darstellen. Dies gilt insbesondere für Sprachen, die in interaktiven Theorembeweisern wie dem an unserem Lehrstuhl mitentwickelten Theorembeweiser Lean 4 verwendet werden: nicht nur können einzelne Teile des Codes wie Beweise Verarbeitungszeiten zwischen Sekunden und Minuten erfordern, Teile einer Datei sowie die Dateien eines Projekts können normalerweise nur in einer festen Reihenfolge abgearbeitet werden. Eine schnelle Namensanalyse des gesamten Projekts beim Laden in den Editor ist damit quasi ausgeschlossen.
In dieser Arbeit soll das Finden von solchen Referenzen in Lean 4 und Integration in Leans Implementierung des Language Server Protocols unter den genannten Einschränkungen erforscht werden. Da eine Online-Analyse wie beschrieben nicht praktikabel sein dürfte, sollten stattdessen entsprechende Metadaten für Lean-Dateien im Dateisystem abgelegt und für eine teilweise Offline-Analyse im Language Server verwendet werden. Wesentliche Gesichtspunkte der Arbeit sind, wann, wo und in welcher Form welche Daten hierfür abgelegt werden sollten, und wie diese für die Analyse herbeigezogen werden können, um eine praktikable und skalierbare Lösung zu erhalten.
Voraussetzungen
- Kenntnisse in funktionaler Programmierung
- Kenntnisse in Theorembeweisen oder abhängigen Typen werden nicht benötigt
Schlüsselworte
Lean
Veröffentlichungen
Betreuer
Studenten
