Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface
复制标题
Coq 文档的异步处理：从内核到用户界面
DOI：
10.1007/978-3-319-22102-1_4
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Enrico Tassi
中科院分区：
文献类型：
--
作者：
Bruno Barras;C. Tankink;Enrico Tassi
本文所描述的工作通过完全重新设计Coq系统处理正式文档的方式来提高Coq系统的反应性。通过将这些工作细分为独立的任务，系统可以优先考虑用户直接感兴趣的任务，并推迟其他任务。在用户端，基于PIDE中间件的现代接口以一致的方式聚合和呈现证明器的输出。最后，延迟的任务利用现代并行硬件进行处理，以提供更好的可扩展性。
The work described in this paper improves the reactivity of the Coq system by completely redesigning the way it processes a formal document. By subdividing such work into independent tasks the system can give precedence to the ones of immediate interest for the user and postpone the others. On the user side, a modern interface based on the PIDE middleware aggregates and presents in a consistent way the output of the prover. Finally postponed tasks are processed exploiting modern, parallel, hardware to offer better scalability.