Email Gateway (Jun 25 2026 at 14:46): Email Gateway (Jun 25 2026 at 14:46):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce what looks like a super useful tool for users working with programming languages.
ML-Lex and ML-Yacc for Isabelle
Achim D. Brucker and Burkhart Wolff
Developing concrete syntax and parsers for Domain-Specific Languages (DSLs) within interactive theorem provers, such as Isabelle, is a common task. Isabelle supports this through rich, yet often brittle to configure, mixfix annotations and syntax translations. Moreover, Isabelle provides parser combinators that can be used to build parsers for the content of cartouches. An alternative to the latter are traditional parser generators, e.g., Lex and Yacc, that take a formal grammar description as input and generate a parser. Traditionally, the use of parser generators for defining DSLs in Isabelle relies on invoking the lexer and parser as external tools, often modifying the generated source code, and importing the generated files. This requires users to manage complex external preprocessing toolchains. In this AFP entry, we address this challenge by providing a native integration of standard ML-Lex and ML-Yacc into Isabelle/HOL. In more detail, we introduce an Isar-level interface, ml_lex_yacc, that allows users to write lexical and grammatical specifications directly within theory files. The framework compiles these specifications into Standard ML structures on-the-fly, links them, and loads them into the current theory context. Moreover, the integration automatically hooks into Isabelle’s Prover IDE (PIDE), empowering users to provide real-time syntax highlighting, semantic tooltips, and precise error localization for their custom languages.
https://isa-afp.org/entries/Isabelle_Lex-Yacc.html
Larry
Email Gateway (Jun 25 2026 at 14:49):From: "\"Lammich, Peter (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
I'm getting 'could not load theory' errors on the AFP entry
Sent from Outlook for Android<https://aka.ms/AAb9ysg>
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Lawrence Paulson <lp15@cam.ac.uk>
Sent: Thursday, 25 June 2026 16:45:55
To: isabelle-users <isabelle-users@cl.cam.ac.uk>
Subject: [isabelle] Noon in the AFP: ML-Lex and ML-Yacc for Isabelle
I'm happy to announce what looks like a super useful tool for users working with programming languages.
ML-Lex and ML-Yacc for Isabelle
Achim D. Brucker and Burkhart Wolff
Developing concrete syntax and parsers for Domain-Specific Languages (DSLs) within interactive theorem provers, such as Isabelle, is a common task. Isabelle supports this through rich, yet often brittle to configure, mixfix annotations and syntax translations. Moreover, Isabelle provides parser combinators that can be used to build parsers for the content of cartouches. An alternative to the latter are traditional parser generators, e.g., Lex and Yacc, that take a formal grammar description as input and generate a parser. Traditionally, the use of parser generators for defining DSLs in Isabelle relies on invoking the lexer and parser as external tools, often modifying the generated source code, and importing the generated files. This requires users to manage complex external preprocessing toolchains. In this AFP entry, we address this challenge by providing a native integration of standard ML-Lex and ML-Yacc into Isabelle/HOL. In more detail, we introduce an Isar-level interface, ml_lex_yacc, that allows users to write lexical and grammatical specifications directly within theory files. The framework compiles these specifications into Standard ML structures on-the-fly, links them, and loads them into the current theory context. Moreover, the integration automatically hooks into Isabelle’s Prover IDE (PIDE), empowering users to provide real-time syntax highlighting, semantic tooltips, and precise error localization for their custom languages.
https://isa-afp.org/entries/Isabelle_Lex-Yacc.html
Larry
Last updated: Jul 02 2026 at 07:34 UTC