×

Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit. (English) Zbl 1294.68129

Aspinall, David (ed.) et al., Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 285, 101-114 (2012).
Summary: After several decades, most proof assistants are still centered around TTY-based interaction in a tight read-eval-print loop. Even well-known Emacs modes for such provers follow this synchronous model based on single commands with immediate response, meaning that the editor waits for the prover after each command. There have been some attempts to re-implement prover interfaces in big IDE frameworks, while keeping the old interaction model. Can we do better than that?{
}Ten years ago, the Isabelle/Isar proof language already emphasized the idea of proof document (structured text) instead of \(proof script\) (sequence of commands), although the implementation was still emulating TTY interaction in order to be able to work with the then emerging Proof General interface. After some recent reworking of Isabelle internals, to support parallel processing of theories and proofs, the original idea of structured document processing has surfaced again.{
}Isabelle versions from 2009 or later already provide some support for interactive proof documents with asynchronous checking, which awaits to be connected to a suitable editor framework or full-scale IDE. The remaining problem is how to do that systematically, without having to specify and implement complex protocols for prover interaction.{
}This is the point where we introduce the new Isabelle/Scala layer, which is meant to expose certain aspects of Isabelle/ML to the outside world. The Scala language (by Martin Odersky) is sufficiently close to ML in order to model well-known prover concepts conveniently, but Scala also runs on the JVM and can access existing Java libraries directly. By building more and more external system wrapping for Isabelle in Scala, we eventually reach the point where we can integrate the prover seamlessly into existing IDEs (say Netbeans). To avoid getting side-tracked by IDE platform complexity, our current experiments are focused on jEdit, which is a powerful editor framework written in Java that can be easily extended by plugin modules. Our plugins are written again in Scala for our convenience, and to leverage the Scala \(actor library\) for parallel and interactive programming. Thanks to the Isabelle/Scala layer, the Isabelle/jEdit implementation is very small and simple.
For the entire collection see [Zbl 1284.68005].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Asperti, A.; Sacerdoti Coen, C.; Tassi, E.; Zacchiroli, S., User interaction with the matita proof assistant, Journal of automated reasoning, 39, (2007) · Zbl 1132.68673
[2] Aspinall, D., Proof general: A generic tool for proof development, () · Zbl 0971.68627
[3] Aspinall, D.; Autexier, S.; Lüth, C.; Wagner, M.; Autexier, S.; Benzmüller, C., Towards merging Plato and PGIP, User interfaces for theorem provers, (UITP 2008), Entcs, 226, (2009)
[4] Aspinall, D.; Lüth, C.; Winterstein, D.; Kauers, M.; Kerber, M.; Miner, R.; Windsteiger, W., A framework for interactive proof, Towards Mechanized Mathematical Assistants (CALCULEMUS and MKM 2007), Lnai, 4573, (2007)
[5] Charles, J.; Kiniry, J.; Autexier, S.; Benzmüller, C., A lightweight theorem prover interface for eclipse, User interfaces for theorem provers, (UITP 2008), Entcs, 226, (2009)
[6] Dixon, L.; Fleuriot, J.D., A proof-centric approach to mathematical assistants, Journal of applied logic: special issue on mathematics assistance systems, 4, (2006) · Zbl 1107.68096
[7] Gast, H.; Autexier, S.; Benzmüller, C., Managing proof documents for asynchronous processing, User interfaces for theorem provers, (UITP 2008), Entcs, 226, (2009) · Zbl 1291.68342
[8] Gast, H., Towards a modular extensible Isabelle interface, in: S. Berghofer and M. Wenzel, editors, Theorem Proving in Higher-Order Logics (TPHOLs) - Emerging Trends, TU München, Institut für Informatik, 2009.
[9] Haller, P.; Odersky, M., Event-based programming without inversion of control, ()
[10] Kaliszyk, C.; Autexier, S.; Benzmüller, C., Web interfaces for proof assistants, User Interfaces for Theorem Provers (UITP 2006), Entcs, 174, (2007) · Zbl 1278.68266
[11] Matthews, D. C. J. and M. Wenzel, Efficient parallel programming in Poly/ML and Isabelle/ML, in: ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010), co-located with POPL (2010).
[12] Odersky, M. et al., An overview of the Scala programming language, Technical Report IC/2004/64, EPF Lausanne (2004).
[13] Wenzel, M., Parallel proof checking in Isabelle/Isar, in: G. Dos Reis and L. Théry, editors, ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS) (2009).
[14] Wenzel, M.; Berghofer, S., The isabelle system manual (for isabelle2009-1)
[15] ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.