Proviola：一种证明重放工具

为了改进与证明助手（PA）交互的现有模型，特别是在证明的存储和重放方面，我们引入了三个相关概念：证明电影，由记录用户输入和相应PA响应的帧组成；摄像机，将用户与PA的交互会话拍摄成电影；以及proviola，它逐帧向第三方重放电影。在本文中，我们描述了电影数据结构，并讨论了基于ProofWeb系统的摄像机和proviola的原型实现。ProofWeb通过Web界面（客户端）将PA交互与驻留在服务器上的实际PA解耦。我们的摄像机通过“监听”ProofWeb通信来拍摄电影。开发电影的首要原因是将形式化证明的审查与用于开发它的PA解耦：电影概念使用户能够讨论小的代码片段，而无需安装PA或向其中加载整个库。其他优势包括开发单独的评论轨道来讨论或解释PA交互的可能性。我们断言，组合的摄像机+proviola在客户端（用户）和服务器（PA）之间提供了一个通用层。最后，基于我们拍摄Coq标准库的经验，我们声称电影是存储在形式化数学百科全书中合适类型的数据。