publication . Article . Preprint . 2018

Isabelle/jEdit as IDE for Domain-specific Formal Languages and Informal Text Documents

Wenzel, Makarius;
Open Access English
  • Published: 01 Nov 2018 Journal: Electronic Proceedings in Theoretical Computer Science (issn: 2075-2180, Copyright policy)
  • Publisher: Open Publishing Association
Abstract
Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores possibilities to use it as a general IDE for formal languages that are defined in user-space, and embedded into informal text documents. It covers overall document structure with auxiliary files and document antiquotations, formal text delimiters and markers for interpretation (via control symbols). The ultimate question behind this: How far can we stretch a plain text editor like jEdit in order to support semantic text processing, with support by the underlying PIDE framework?
Subjects
acm: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSComputingMethodologies_DOCUMENTANDTEXTPROCESSING
free text keywords: Computer Science - Human-Computer Interaction, Mathematics, Electronic computers. Computer science, QA1-939, QA75.5-76.95

[1] David Aspinall, Christoph Lu¨th & Daniel Winterstein (2007): A Framework for Interactive Proof. In M. Kauers, Manfred Kerber, Robert Miner & Wolfgang Windsteiger, editors: Towards Mechanized Mathematical Assistants (CALCULEMUS and MKM 2007), LNAI 4573, Springer, doi:10.1007/978-3-540-73086-6 15.

[2] Stefan Berghofer (2017): The HOL-SPARK Program Verification Environment. Part of Isabelle distribution. http://isabelle.in.tum.de/website-Isabelle2017/dist/library/HOL/HOL-SPARK-Manual/ document.pdf.

[3] Leonardo Mendonc¸a de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn & Jakob von Raumer (2015): The Lean Theorem Prover (System Description). In Amy P. Felty & Aart Middeldorp, editors: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, Lecture Notes in Computer Science 9195, Springer, doi:10.1007/978-3-319-21401- 6 26.

[4] Carst Tankink (2014): PIDE for Asynchronous Interaction with Coq. In Christoph Benzmu¨ller & Bruno Woltzenlogel Paleo, editors: User Interfaces for Theorem Provers (UITP 2014), EPTCS 167, doi:10.4204/EPTCS.167.9. [OpenAIRE]

[5] Makarius Wenzel (2010): Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. In C. Sacerdoti Coen & D. Aspinall, editors: User Interfaces for Theorem Provers (UITP 2010), ENTCS, doi:10.1016/j.entcs.2012.06.009. [OpenAIRE]

[6] Makarius Wenzel (2013): READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking. In Cezary Kaliszyk & Christoph Lu¨th, editors: User Interfaces for Theorem Provers (UITP 2012), EPTCS 118, doi:10.4204/EPTCS.118.4. [OpenAIRE]

[7] Makarius Wenzel (2014): Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. In Gerwin Klein & Ruben Gamboa, editors: Interactive Theorem Proving - 5th International Conference, ITP 2014, Vienna, Austria, Lecture Notes in Computer Science 8558, Springer, doi:10.1007/978-3-319-08970-6 33. [OpenAIRE]

[8] Makarius Wenzel (2014): System description: Isabelle/jEdit in 2014. In Christoph Benzmu¨ller & Bruno Woltzenlogel Paleo, editors: User Interfaces for Theorem Provers (UITP 2014), EPTCS 167, doi:10.4204/EPTCS.167.10. [OpenAIRE]

[9] Makarius Wenzel (2017): Isabelle/jEdit. Part of Isabelle distribution. http://isabelle.in.tum.de/ website-Isabelle2017/dist/Isabelle2017/doc/jedit.pdf.

Abstract
Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores possibilities to use it as a general IDE for formal languages that are defined in user-space, and embedded into informal text documents. It covers overall document structure with auxiliary files and document antiquotations, formal text delimiters and markers for interpretation (via control symbols). The ultimate question behind this: How far can we stretch a plain text editor like jEdit in order to support semantic text processing, with support by the underlying PIDE framework?
Subjects
acm: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSComputingMethodologies_DOCUMENTANDTEXTPROCESSING
free text keywords: Computer Science - Human-Computer Interaction, Mathematics, Electronic computers. Computer science, QA1-939, QA75.5-76.95

[1] David Aspinall, Christoph Lu¨th & Daniel Winterstein (2007): A Framework for Interactive Proof. In M. Kauers, Manfred Kerber, Robert Miner & Wolfgang Windsteiger, editors: Towards Mechanized Mathematical Assistants (CALCULEMUS and MKM 2007), LNAI 4573, Springer, doi:10.1007/978-3-540-73086-6 15.

[2] Stefan Berghofer (2017): The HOL-SPARK Program Verification Environment. Part of Isabelle distribution. http://isabelle.in.tum.de/website-Isabelle2017/dist/library/HOL/HOL-SPARK-Manual/ document.pdf.

[3] Leonardo Mendonc¸a de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn & Jakob von Raumer (2015): The Lean Theorem Prover (System Description). In Amy P. Felty & Aart Middeldorp, editors: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, Lecture Notes in Computer Science 9195, Springer, doi:10.1007/978-3-319-21401- 6 26.

[4] Carst Tankink (2014): PIDE for Asynchronous Interaction with Coq. In Christoph Benzmu¨ller & Bruno Woltzenlogel Paleo, editors: User Interfaces for Theorem Provers (UITP 2014), EPTCS 167, doi:10.4204/EPTCS.167.9. [OpenAIRE]

[5] Makarius Wenzel (2010): Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. In C. Sacerdoti Coen & D. Aspinall, editors: User Interfaces for Theorem Provers (UITP 2010), ENTCS, doi:10.1016/j.entcs.2012.06.009. [OpenAIRE]

[6] Makarius Wenzel (2013): READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking. In Cezary Kaliszyk & Christoph Lu¨th, editors: User Interfaces for Theorem Provers (UITP 2012), EPTCS 118, doi:10.4204/EPTCS.118.4. [OpenAIRE]

[7] Makarius Wenzel (2014): Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. In Gerwin Klein & Ruben Gamboa, editors: Interactive Theorem Proving - 5th International Conference, ITP 2014, Vienna, Austria, Lecture Notes in Computer Science 8558, Springer, doi:10.1007/978-3-319-08970-6 33. [OpenAIRE]

[8] Makarius Wenzel (2014): System description: Isabelle/jEdit in 2014. In Christoph Benzmu¨ller & Bruno Woltzenlogel Paleo, editors: User Interfaces for Theorem Provers (UITP 2014), EPTCS 167, doi:10.4204/EPTCS.167.10. [OpenAIRE]

[9] Makarius Wenzel (2017): Isabelle/jEdit. Part of Isabelle distribution. http://isabelle.in.tum.de/ website-Isabelle2017/dist/Isabelle2017/doc/jedit.pdf.

Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Article . Preprint . 2018

Isabelle/jEdit as IDE for Domain-specific Formal Languages and Informal Text Documents

Wenzel, Makarius;