Isabelle/Scala：在IDE中实现异步交互式证明文档的支持

可在www.sciencedirect.com在线获取理论计算机科学电子笔记285（2012）101-114www.elsevier.com/locate/entcs使用Isabelle/Scala和Isabelle/jEdit进行Makarius Wenzel马卡留斯·温泽尔1，2Universit'eParis-Sud11，LRIOrsay，法国摘要几十年后，大多数证明助手仍然以基于TTY的交互为中心，处于紧密的读取-评估-打印循环中。即使是著名的Emacs模式，这种证明器也遵循这种同步模型，基于具有即时响应的单个命令，这意味着编辑器在每个命令之后等待证明器。已经有一些尝试在大型IDE框架中重新实现prover接口，同时保持旧的交互模型。我们能做得更好吗？十年前，Isabelle/Isar证明语言已经强调了证明文档（结构化）的概念文本）而不是证明脚本（命令序列），尽管实现仍然模拟TTY交互，以便能够与当时新兴的Proof General接口一起工作。在最近对Isabelle内部进行了一些修改之后，为了支持理论和证明的并行处理，结构化文档处理的原始思想再次浮出2009年或更高版本的Isabelle已经提供了一些对异步检查的交互式证明文档的支持，这些文档正在等待连接到合适的编辑器框架或全尺寸IDE。剩下的问题是如何系统地做到这一点，而不必为证明者交互指定和实现复杂的协议。这就是我们引入新的Isabelle/Scala层的地方，它旨在公开某些方面伊莎贝尔/ML的秘密 Scala语言（由Martin Odersky编写）非常接近ML为了方便地对众所周知的prover概念进行建模，Scala也可以在JVM上运行，并且可以直接访问现有的Java库。通过在Scala中为Isabelle构建越来越多的外部系统包装，我们最终达到了可以将证明器无缝集成到现有IDE（比如Netbeans）中的地步。为了避免受到IDE平台复杂性的影响，我们目前的实验主要集中在jEdit上，这是一个用Java编写的功能强大的编辑器框架，可以很容易地通过插件模块进行扩展。为了方便起见，我们的插件再次使用Scala编写，并利用Scalaactor库进行并行和交互式编程。由于Isabelle/Scala层，Isabelle/jEdit实现非常小而简单。关键词：Isabelle，Scala，jEdit，异步证明处理，编辑器和IDE框架的重用1介绍从TTY循环到一般证明Milner的LCF传统中的交互式证明器最初的LCF系统具有TTY-1由BMBF项目“Verisoft”部分支持的研究2makarius@sketis.net1571-0661 © 2012由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2012.06.009102M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101基于读取-评估-打印顶层的ML编程语言，以及后来的系统，如Coq [15，§4]和Isabelle [15，§6]已经对此进行了温和的改革，例如通过引入自己的ML之外的命令语言。如果我们重新考虑著名的Proof General/ Emacs接口[2]，它可以被视为各种证明器的巨大成功，它的交互模型与TTY模型紧密相连。 证明器命令以顺序（同步）方式一个接一个地发出，而每个结果立即显示在单独的窗口中（通常一个用于目标输出，一个用于其他响应）。主编辑器窗口分为两部分：已处理的文本的锁定区域和未处理文本的可编辑区域。因此，ProofGeneral提供了一个逐步执行证明脚本的简单比喻。用户可以通过assert和retract命令在两个编辑器区域之间移动边界这个模型非常适合许多现有证明器的顶层循环。主要的额外需求是用于向后移动的撤消功能。请注意，原始的HOL家族[15，§1]缺乏这一点，因此证明一般支持一直是非常有限。Proof General风格的交互大大增强了TTY模型，但仍然围绕着一个接一个命令的想法。例如，用于Coq [15，§4.2]的SSREFLECT脚本语言利用了许多小命令的快速输入，并通过证明状态输出从证明器立即反馈。即使使用ProofGeneral作为首选界面，这也是TTY风格的交互。超越一般证明？证明一般已经能够主导互动定理社区多年。它的基本交互模型已经被模仿了好几次，例如CoqIde [15，§4.6]，ProofWeb [10]或Matita [1]。还有一些没有被广泛使用的Proof General的克隆。这是否意味着Proof General模型及其典型实现是定理证明器用户界面的最后一句话近年来，我们看到了两个挑战其主导地位的主要我们观察到以下主要缺点一般证明。(i) 底层编辑器框架的弱点Classic Proof General使用相对强大的Emacs环境，尽管它已经相当古老了。有些分支，如XEmacs，实际上是不维护的。GNU Emacs 23分支在过去的几年里已经迎头赶上Emacs平台也有一些基本的限制，例如其LISP引擎的单线程执行模型。大多数Proof General重制版使用更弱的编辑器：CoqIde使用现有的GTk小部件在OCaml中实现了自己的编辑器。这对于初学者来说已经足够了，但是很多Coq的高级用户在某个时候会切换回Proof General/Emacs虽然OCaml/GTk原则上是多线程的，但CoqIdeM. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101103实现者已经报告了GUI组件和用户线程的集成的稳定性问题。此外，OCaml不支持多核硬件上线程的真正并行执行，将应用程序限制在CPU资源的一小部分。已经有各种尝试将Proof General背后的主要思想移植到全面的IDE环境中，特别是Proof General/ Eclipse（主要用于Isabelle）[4]，Provereditor（用于Eclipse和Coq）[5]和I3 P [8]（用于NetBeans和Isabelle）。我们希望用功能齐全的IDE支持来取代相对简单的编辑器工具，尽管由于典型IDE的庞大规模，这带来了额外的挑战(ii) 互动模式的弱点如上所述，我们可以将Proof General交互理解为普通TTY模式的附加功能.特别是，只有一个焦点，即上一个命令已成功执行且系统等待用户输入下一个命令的点。这对应于TTY循环的提示，并且标记固有的顺序/同步协议。到目前为止，对这种概念上的限制的关注要少得多，我们认为这比关于底层编辑器平台的问题更重要。在Proof General/ Eclipse [4]中，PGIP的复杂协议定义仅仅是对经典Proof General交互进行了编码。除此之外，最近的一些工作[3]探索了PLATΩ中的多焦点编辑，基于文档子树上的并发XML更新协议。这种情况是我们开发Isabelle/Scala和Isabelle/jEdit项目的起点。我们希望克服传统证明一般的局限性，这两个wrt。底层编辑器技术和交互模型。在§2中，我们概述了一个异步交互模型，它继续了我们以前在批处理模式下并行证明检查的在第3节中，我们介绍了Isabelle/Scala层作为ML和JVM世界之间的中介库，它提供了对原始进程间通信的重要抽象在§4中，我们报告了我们的示例应用程序Isabelle/jEdit，它借鉴了§2和§3的结果。随着我们的前进，进一步的相关工作被引用，同时涵盖特定的方面。2并行证明检查和异步交互复杂GUI应用程序的多线程非常重要，原因有二。首先，它有助于系统地构建交互式应用程序，例如避免阻止用户输入。其次，大约5年前主流多核硬件的出现使得任何CPU密集型应用程序都不可避免地需要并行处理。在批处理模式下有效并行证明检查的问题已经针对Isabelle和底层Poly/ML平台进行了处理，参见[13]和[11]。我们的证明器和ML实现的以下主要优点允许在现有系统上改进并行证明处理• 形成项目的理论的DAG结构化开发图 这个恩-104M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101支持并行make工具风格的简单并发加载，如GNU make-j。 在系统中几乎不需要改变以在最外层实现这种并行性，但是加速因子受到理论依赖性的限制，理论依赖性通常是相对线性的。• 完全指定的顶层定理和证明不相关的最实用的目的。最初的LCF家族是围绕推理内核的思想构建的，该推理内核仅检查证明，而不必保留显式记录。即使在基于类型论的系统中，如Coq，证明通常是不透明的，并且不会在涉及所得定理的进一步证明中考虑。 当- ever的结果命题被预先指定时，我们可以很容易地分叉证明过程，并在加载整个理论子图的最后加入所有内容。该方案可以很好地饱和104个内核[13，§5]。• 使用Isar结构化证明语言的严格模块化证明 这是对结构良好的ISAR证明文本的特别奖励。Isar证明语言的设计遵循的原则是，可以快速检查主大纲，而耗时的自动推理仅限于终端子证明的证明例如 后者可以以与上述类似的方式分叉/接合这种额外的并行性潜力在4-8个核心之外变得非常重要在大型应用程序中，如AFPwww.example.com中http://afp.sf。net/entries/JinjaThreads.shtml中，子结构的并行检查产生了很大的差异，顶层并行的总运行时间为30分钟，而子证明中的并行运行时间为8分钟。• 基于不可变值的Isabelle/ML编程风格 由于Isabelle的主要部分的实现非常干净，几乎到处都是不可变的数据结构，因此在大规模上更改底层执行模型相对容易。只有一小部分不纯的代码必须被删除。总之，Isabelle理论和证明的并行批处理在原则上相对容易实现，因为它可以被理解为某些符号证明表达式的“评估过程”的适当困难的部分是从头开始构建并行ML的基本基础设施[13][11]，并最终获得合理的加速因子（例如4核3.0，8核5.0并行证明处理如何影响交互模型？我们已经解释了为什么TTY模型本质上是顺序的，一个接一个地缓慢地工作，等待证明器的结果，直到当前命令完成，如顶层命令提示符所示为了利用丰富的理论和证明结构，不仅是并行批处理，而且在交互模式下，我们需要重新考虑证明器toplevel本身。在Isabelle 2009/2009-1中，已经有一个简单的异步顶层，它支持异步文档模型，如下所示。• 显式操作begin document和end document限定了M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101105下面进一步操作。 这样的文档被理解为具有纯功能更新操作的持久实体。有明确的版本标识符。对通过begin document创建的初始根进行操作会产生一个随时间演变最终的文档选择一条成功的路径，最终提交到理论数据库• 定义命令操作识别一段源文本（在Proof General术语中为这样的命令本质上代表了对证明者的语义状态（包括理论和证明上下文、目标状态等）的函数。与证明者的交互意味着以各种方式组成这样的函数，每个函数都导致部分评估的证明尝试。• 编辑文档操作通过插入和移除如上定义的命令的原语来更新文档这会产生一个新的文档，其中有一个新的标识符，并且证明器最终会报告内部状态的变化。异步顶层维护大量这样的相关文档版本，它们通常共享公共子结构。根据证明者管理的并行评价进程，新文件版本产生的结果在收到时即予以报告。消息由特定文档版本中的相应命令明确标识（顶层提示被废除）。上面的原语粗略地描绘了编辑器和证明器之间的协议，它可以给用户一种连续检查文本的印象，并在它逐渐出现时提供编辑器从不等待证明者，也从不阻止用户输入。证明者可以自由地安排部分证明文档的评估，以尽可能地利用并行性的潜力。即使没有并行检查，证明器也可以以允许用户彼此独立地编辑证明的方式来安排文档处理，而不需要昂贵的整个脚本重放。我们期望通过这种证明文档处理机制的解耦，对交互式证明开发的效率产生巨大影响尽管如此，在这个原始接口上将编辑器连接到证明器仍然非常困难，因此我们在Isabelle/Scala层引入了一个更抽象的编程API3用于证明器交互为了理解Isabelle/Scala层的关键作用，我们首先重新考虑连接两个完全不同的世界的基本问题：在标准ML（特别是Poly/ML）中实现的证明器，普遍使用纯高阶函数技术，以及更请注意，Coq和Matita是在OCaml中实现的，并且该平台有基本的GUI库，可以用作某些编辑器功能的起点。根据CoqIde和Matita GUI背后的人私下或公开的报告[1]，我们得出结论，OCaml/GTk是少数GUI106M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101文档模型尽管如此，平台仍然存在，并且存在需要大量开发资源的技术问题。即使基本的GUI层可以完美地工作，高级编辑器或IDE框架仍然缺乏。我们真正的任务是构建证明器，而不是从头开始重新实现编辑器或IDE。因此，我们更喜欢链接到现有的框架，即使这意味着要适应两个不同的过程：ML与JVM。显式的进程间通信肯定会引起一些额外的问题，而非异构语言的情况会使事情进一步复杂化。PGIP [4]通过定义各种自治组件之间的这些组件与这里涉及的独立编程语言环境相一致：ML中的证明器进程，Java中的编辑器，Haskell中的代理3我们认为，在这些过程的边界切割的概念组件复杂的系统集成，即使没有（可选）之间的代理。这里定义的协议套件涵盖了证明者或编辑者在各自的过程边界上偶然暴露的许多细节。实现和维护如此复杂的协议是非常困难的。我们在证明器和编辑器之间架起桥梁的方法是非常不同的，参见图1。我们没有使用复杂的协议，而是在每一方假设一个相对对文档的操作是通过静态类型的库函数而不是原始协议消息进行的。APIAPIFig. 1. 编辑器和证明器之间的中介文档模型-概念视图。图2解释了如何实际实现这一点。库实现有一个私有的内部协议;只有相当多的抽象概念在任何一方的API中公开。将库实现分为两个部分（ML与JVM）是通过在Isabelle/Pure的主源代码树中并排维护这些双语模块来解决的，并且对应的ML结构/函子与Scala对象/类/特征具有相同的名称。Scala [12]的灵活性允许在JVM端模仿Isabelle/ML编程风格。4例如，为了表示抽象XML树，xml.ML在33有趣的是，PGIP代理在某种程度上是一种增强某些证明器功能的手段，而不必修改证明器本身，也不必在Java中进行复杂的符号计算。4Scala中的高阶函数式编程工作得非常好，与最佳实践Isabelle/ML相比，代码的压缩因子为1.5- 2 . 0 。伊莎贝尔：SML编辑器：JVMM. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101107图二、通过内部协议和适配器库实现文档模型几行代码和几页中的各种支持函数。相应的xml.scala使用了3行Scalacase类，以及与ML版本大小相似的各种基本方法（在不可变对象上）。当然，在功能上有相当大的重叠，但每一边也有其独特的部分。例如，Scala端提供了 一 个 函 数 ， 将 纯 XML 树 转 换 为 一 个 对 象 （ 可 变 的 ）org.w3c.dom.Document，因为某些现有的Java组件偶尔会需要这个，比如HTML呈现引擎。为了在两个进程之间传输这些无处不在的XML树，内部协议使用简单而高效的YXML编码[14，§4.12]。因此，我们将完全公开的XML文档交换的艰巨任务缩小到我们自己发明的非常简单的传输格式，它可以在1/2页上指定，并在1/2天内有效地实现。保持进程间通信的私密性（这些细节往往很微妙）具有更大的实际优势。特别是，我们可以很容易地改变协议，以适应新的要求。在Isabelle/Scala层的简短历史中，内部协议已经经历了几次实质性的变化，既涉及底层异步文档模型的核心思想，也涉及提高性能和健壮性的边缘这样的议定书修订只需要一方同意自己的意见，而不是一个议定书委员会一遍又一遍地谈判。Isabelle/Scala API级别的潜在不兼容性可以很容易地在客户端代码中解决，因为签名是静态类型的。超越单纯的连通性Isabelle/Scala 不仅仅是ML 和JVM 世界的简单和健壮的连接。在使用Isabelle/jEdit应用程序时，与可以异步更新的持久文档的一般概念相比，编辑器端的即时GUI编程需求被证明是微不足道的。这意味着概念上更深层次的部分独立于特定的编辑器，可以在Isabelle/Scala库中进行通用处理。其基本思想是在版本控制下，使用类似ML的Scala结构（元组、列表、选项、函数）对不可变文档族进行建模。并发性和真正的并行性是通过Scala的actor库实现的[9]，它提供了一个非常好的抽象，通过显式消息通道链接的独立功能实体。遵循ML与再次，我们还提供了一些简单的Scala附加的Actor库，以模仿值为导向API议定书内部编辑器：JVM伊莎贝尔：SMLAPIScalaSML108M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101Isabelle/ML中围绕期货的并行性[11，§4]。异步文档模型的这些更高级的方面将需要在今后的工作中进一步阐述例如，目前的历史只适用于单个理论，而忽略了多个编辑器所需的隐式理论图。尽管如此，目前的Isabelle/Scala层足以支持我们的Isabelle/jEdit应用程序，并支持对一般方法的一些实际评估。4应用程序：Isabelle/jEdit在讨论Isabelle/jEdit的内部结构之前，我们首先说明它是如何向最终用户呈现的，参见图3。在静态屏幕截图中很难捕捉到异步校样编辑的动态过程。一般的外观类似于Eclipse或Netbeans中现有的Java IDE：用户可以随意输入文本，编辑器通过后台部分处理的文档中的语义信息逐步提供有用的反馈。这实现了基于我们的异步证明器顶层的连续证明检查。许多信息可以直接附加到源文本，通过着色，工具提示，弹出窗口等，因此我们解决了证明编辑的挑战，而没有[6]中提出的目标状态。图3.第三章。Isabelle/jEdit的主编辑器窗口，带有语义突出显示除了主编辑器之外，我们还提供传统的证明器输出窗口M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101109帧，例如，参见图4中对应于最后一次放映命令（红色）。图四、显示证明状态的Output dockable实例实际上，show的结果消息中报告的错误是在文本的不同位置引起的，即光标位置处的无意义的假设语句，这在该证明上下文中是不允许的。颜色的动态变化已经表明文本中存在这样一个结构性错误：在插入assume命令后，相应的show命令变为红色。通过直接在文本中突出显示这些非局部错误，我们已经在小范围内超越了Proof General模型。 需要进一步的改进，以实现一个可行的编辑模型，特别是对ISAR的证明- ISAR已被锁定到TTY循环更多已经超过十年4.1jEdit编辑器框架jEdit编辑器http://www.jedit.org被宣传为与功能齐全的IDE（如Eclipse或Netbeans）相比，jEdit要小得多，并且更专注于文本编辑的主要任务 这个主要的jEdit功能是由jedit.jar（在jEdit 4.3.2 中大小为4MB）提供的，并且可以从存储库中下载许多插件。 对于这些框架来说，插件的质量差别很大，从核心jEdit开发人员编写的主要插件到感兴趣的用户的临时实验。插件一个jEdit插件由一个普通jar的主要JVM对象代码，以及一些通过JVM属性文件的元数据和一些明智的XML使用组成组件通过BeanShell中的代码片段粘合在一起，BeanShell本质上是Java的轻量级解释版本。甚至还有一个交互式BeanShell控制台（作为标准插件），它公开了运行编辑器环境的JVM类的名称空间。这让人想起了Emacs临时缓冲器，它可以直接访问LISP运行时环境。通过学习文档、示例插件、编辑器的源代码和一些主要的插件，开始实现jEdit插件是非常容易的。jEdit控制台插件极大地帮助了交互式探索和调试。另外，整个应用程序可以在现有JVM调试工具的控制下运行，比如Netbeans的Java源代码级调试器。110M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101综合应用除了使用官方的jEdit发行版和一些插件外，还可以使用jEdit作为针对特定目的的集成应用程序的基础。例如，MathPiperhttp://www.mathpiper.org通过将jEdit与其他一些数学应用程序捆绑在一起提供了一个http://www.geogebra.org在这种情况下，MathPiper启动了一个定制版本的jEdit，其中一些预加载的插件在jEdit的“可停靠窗口管理器”的子窗口中运行一 个 类 似 的 衍 生 应 用 程 序 是 ActiveMath 项 目 www.example.com 的OQMathJEdithttp://www.activemath.org。CZT套件http://czt.sourceforge.net还包括一些jEdit插件，可用作Z规范语言的小型IDE的基础。与大型IDE框架相比，这种工具集成非常简单，只要组件可以作为常规jar使用即可。从历史上看，这通常意味着Java作为实现语言，但最近一些替代的基于JVM的语言已经获得了足够的关注，被JVM社区视为“高性能语言”。 除了Groovy、Jython、JRuby等各种脚本语言之外，还有两种函数式语言在主流世界中获得了关注：Clojure http://clojure.org（大致上是使用LISP 表 示 法 的 Haskell 的 无 类 型 版 本 ） 和 Scala http://www.scala-lang.org，其高级函数式面向对象编程的复杂集成和对现有Java类库的直接访问。4.2Isabelle/jEdit主Isabelle/jEdit插件由10个小的Scala文件（总大小为42KB）组成，这些文件增加了一些关键的jEdit组件，以提供前面概述的防异步文档编辑的隐喻Isabelle/jEdit将jEdit 4.3.2框架与我们自己的Isabelle插件（用Scala编写）以及其他一些现成的jEdit插件集成在一起。主要的jEdit发行版基本上没有变化，但是整个jEdit安装都是以“预封装”的形式呈现给用户的，可以通过常规的Is- abelle工具包装器立即启动。除了某些默认属性之外，Java运行时的启动阶段和核心jEdit组件经过微调，以处理重要的细节，例如Isabelle特定的文本编码UTF-8-Isabelle，以及定制的IsabelleTextUnicode字体，该字体实际上包含用户期望从多年的Proof General X-Symbol支持中获得的常用Isabelle符号。Isabelle插件组件核心功能直接与jEdit的关键编辑器概念相关联，如下所示。• 我们的文档模型通过Isabelle/Scala的异步文档模型在后台提供的语义信息来增强jEditBuffer我们M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101111维护一个从Buffer到Document Model的部分函数-每个与Isabelle理论文件相关的Buffer都通过添加一个Document Model的实例来5由于实际的文档模型是由Isabelle/Scala层维护的编辑端在这里需要做的很少。的主要职责文档模型如下。· 维护一个指向Isabelle/Scala证明文档模型持久历史的指针这影响了文本的输入和呈现：所有操作都与历史中的这个显式标识点相关，该点表示为唯一的版本标识符。· 输入连接涉及一个常规事件处理程序，用于对jEdit生成的纯文本执行插入和删除操作。这些事件在本地存储，并最终与历史标识符一起转发到底层文档模型。Isabelle/Scala库根据证明语言的命令结构将文本编辑转换为更大的块。这种多阶段的编辑管道将编辑器与证明器分开：这里不涉及锁定或用户可以在任何时候输入到编辑器中，而不受证明者的响应的影响，证明者的响应可能要晚得多，比如说在20 ms之内。. . 200毫秒· 表示连接涉及与实现语义语法突出显示的证明器相关联的令牌标记，这意味着来自证明器的真实信息用于指示某些文本片段的正式状态。这避免了基于编辑器的语法表的典型挫折，该语法表以粗略的方式近似语法突出显示在这里，我们使用证明器提供的信息，证明器因此，我们可以突出Isabelle的术语语言，它在理论来源中嵌入为“内部syn- tax”，或者嵌入ML的Isar文本，它反过来通过反引号引用正式实体，以及所有这些都穿插着一些嵌套的注释。• 我们的文档视图以与上面类似的方式增加了jEditTextArea。它涵盖了呈现文本编辑器的即时视觉方面，允许对同一内容进行多个视图。jEditTextArea使插件能够提供自定义绘图器，这些绘图器可以直接访问Java图形上下文，以几乎任意的方式修改视觉外观。我们使用这个工具来表示命令状态（未处理：粉红色，已完成：淡蓝色，失败：红色），两者都作为源文本的背景（作为在Proof General中），并在文本视图的右边距中显示为小刻度（与常见IDE中一样）。在TextArea中有额外的连接来跟随光标的移动：它会影响其他插件组件，特别是prover输出窗口。5幸运的是，jEdit开发人员并不坚持纯静态的类层次结构，而是提供了一个合适的后门，让 人想起普通的旧对象属性列表。112M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101我们提供了一些独立的这些很容易实现为Java Swing框架的子类，并通过一些基本的XML配置声明为jEdit编辑器管理任意数量的此类可停靠对象的实例，可以作为自由浮动的窗口，也可以停靠在主编辑器视图的边缘。Isabelle/jEdit提供了以下可停靠类。• Outputdockable使用基础文档模型的历史点显示光标所指命令的结果消息（包括证明状态）。Isabelle消息包含以标记树表示的丰富信息。这通 过 在 内 部 将 其 映 射 到 XHTML ， 并 让 Lobo 浏 览 器http://lobobrowser.org通过给定的CSS显示它来呈现 因此，我们几乎免费获得了相当灵活的输出设备。 证明一般风格的语法突出显示的自由与。绑定变量、类型变量等。 可以重用现有的CSS为Isabelle的HTML演示理论源码。由证明器提供的进一步语义信息，例如对形式实体（类型、常量等）的引用， 可以链接到Scala内部操作来实现hyperref，尽管这还没有完全激活。• Protocoldockable使用XML表示法显示证明器输入和输出消息的原始流请注意，内部协议使用YXML的更高效的传输语法。在Swing文本组件中显式打印所有协议消息会导致明显的速度降低，因此这实际上只是为了调试。O现成的插件jEdit存储库还提供了非常有用的“元插件”，可以很容易地为我们的讽刺的是，这样的基本功能通常需要在更大的IDE中从头开始重新实现Isabelle/jEdit应用程序重用以下jEdit插件。• 使用我们的Scala子插件控制台，以提供常规的读取-评估-打印循环。它使用EPF Lausanne的Scala编译器套件提供的现有类Interpreter。需要注意的是，解释器实际上与应用程序本身运行在同一个JVM环境中。如果最终用户真的需要在编程语言级别访问应用程序，这可能是可行的，但Scala控制台已经被证明是一个不可避免的开发工具，在文化上非常接近OCaml或Poly/ML的传统顶层循环。此外，它提供了应用程序的即时• SideKick提供的一个树形视图的关于buffer的源程序，也可用于完成M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101113弹出窗口和工具提示。• 源代码编辑器中简单可点击引用的超链接为我们的目的设置这样的插件通常很简单。它需要阅读一些示例源代码（Java），并在0.5-2页的Scala中实现我们的prover-specific还有一些通用的jEdit插件可以直接在我们的上下文中使用，而不需要任何额外的配置。例如，Highlight插件提供了基于用户给出的正则表达式的即兴语法高亮。5结论弥合ML和Java从我们自己在过去两年中与JVM世界的接触，以及与其他证明器接口开发者的讨论中，我们可以说，在这些不同的世界之间显然存在着文化鸿沟。交互式证明器通常使用标准ML、OCaml或Haskell编写，使用基于高阶原理的深度编程技术（递归λ-演算与Hindley-Milner类型、monads以及最近的趋势，甚至是依赖类型编程语言）。相比之下，工业强度的Java框架更广泛而不是更深入，具有巨大的IDE和重型工具，通过“重构”等来（重新）生成代码，很少有人被这两种工作方式所吸引，甚至更少有人同时在这两种工作方式中获利。证明者社区偶尔会尝试将GUI技术引入他们的小世界，通常使用OCaml或Haskell中的GTk。尽管如此，我们可以说，即使是OCaml或Haskell背后的相对较大的社区也尚未大规模地提供对主流GUI框架的访问，并且完全缺少复杂的编辑器或IDE框架。我们对这个文化问题的回答是：保持ML作为证明器的干净实现Scala中的高阶编程工作得非常好，我们可以访问有趣的框架，这些框架碰巧是用一种稍微奇怪的语言（Java）实现的。Scala也有相当不错的标准库可供操作，包括作为并行和交互组件的有效模型的actor对常规使用的证明器IDE技术一旦连接到当代IDE的基本技术问题得到解决，我们就需要详细说明与已建立的编程语言IDE相反的证明编辑的真正需求例如，对日志基础的完全形式化检查我们的异步证明文档模型通过将未完成的证明尝试建模为一流的文档版本，并允许各个证明步骤逐步产生结果，甚至产生分歧来解决这个问题。当这些想法被扩大到图书馆维护的水平时，114M. Wenzel/Electronic Notes in Theoretical Computer Science 285（2012）101与外部版本控制相结合，比如通过Mercurial及其高效持久历史模型。可行的证明程序IDE支持将是进入这些和其他实际使用的正式证明领域的先决条件PIDE宣言http://bitbucket.org/pide/pide/wiki/Home提供了一些进一步的观点。引用[1] Alberti ， A. ， C. Sacerdoti Coen ， E. Tassi 和 S. Zacchiroli ， User interaction with the Matita proofassistant，Journal of Automated Reasoning39（2007）。[2] 阿斯皮纳尔，D.，Proof General：一个用于证明开发的通用工具，在：S。Graf和M. Schwartzbach，编辑，欧洲软件理论与实践联合会议（ETAPS），LNCS1785（2000）。[3] Aspinall ， D. ， S. 奥 特 克 西 耶 角 Luth 和 M.Wagner ， Towa RDM RGP ， in ： S.Autexier 和 C.Benzmüller，editors，UserInterfa cesforTheoremP rover（2008），ENTCS226（2009）.[4] A spinall，D.，C. Lu′th和D. 王文，一种新的计算机辅助设计方法，北京：北京大学出版社。Kauers，M.Kerber，R. Miner和W. Windsteiger，editors，Towards Mechanical Mathematical Assistants（CALCULEMUSand MKM 2007），LNAI4573（2007）.[5] Charles，J.和J. Kiniry，Eclipse的轻量级定理证明器接口，在：S。Autexier和C. Benzmüller，editors，UserInterfa cesforTheoremP rover（2008），ENTCS226（2009）.[6] 迪 克 森 湖 和 j.d. Fleuriot ， A proof-centric approach to mathematical assistants ， Journal of AppliedLogic：Special Issue on Mathematics Assistance Systems4（2006）.[7] 加斯特，H.，为您的产品提供最佳的质量保证，包括： Autexier和C. Benzmüller，editors，User Interfacesfor Theorem Provers（CUP 2008），ENTCS 226（2009）.[8] 加斯特，H.，一个模块化的可扩展的Isabelle接口，在：S。Berghouth和M. Wenzel，editors，Theo remProvinginHigher-OrderLogics（TPHOL）-EmergingTrends，TUMuénchen，InstitutfuürInformatik，2009.[9] Haller，P. and M. Odersky，基于事件的编程没有控制反转，在：联合模块化语言会议，Springer LNCS，2006年。[10] Kaliszyk，C.， 网络接口为p ro的助理，在：S。 Autexier和C. Benz müller，editors，UserInterfaces forTheorem Provers（CUP 2006），ENTCS 174（2007）.[11] Matthews，D. C. J.和M. Wenzel，Eachicient 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.例如，Scala编程语言概述，技术报告IC/2004/64，EPF Lausanne（2004）。[13] Wenzel ， M. ， 在 Isa b e l le/Isar 中 检 查 的 Pa ra llelp ro ， in ： G.Do s R e i s andL. 2009 年 ，ACMSIGSAM 2009机械化数学系统编程语言国际研讨会（PLMMS）。[14] Wenzel ， M. 和 S. Berghabel ， “The Isab