Integrating Dependency Building with Document Checking in Coq
Recent years have seen a trend towards more integrated tooling in programming environments. For example, Rust’s Salsa combines the Rust compiler with an incremental build system in order to provide a query-based reactive archi- tecture that language servers and tools can build on. In this abstract, we explore the integration of a build system with coq-lsp, an incremental document checking system for Coq. We believe our approach opens the door to significant usability and performance improvements. We guarantee that the user will never Require an out of date library, an unde- sired action that is a common source of frustration among Coq users. On the performance front, we can share .vo file parsing among all the files in a theory, which saves a signifi- cant amount of time. Moreover, this integration allows for users to have very different build strategies tailored to their particular needs. We have implemented a prototype of this system for coq-lsp; the implementation relies on algebraic effects in OCaml 5.0, dispatching an effect every time a Require statement is found.
(coqpl24-paper6.pdf) | 338KiB |
Sat 20 JanDisplayed time zone: London change
16:00 - 17:30 | |||
16:00 22mTalk | InducTeX: A MetaCoq plugin for typesetting inductive definitions CoqPL Jacco Krijnen Utrecht University File Attached | ||
16:22 22mTalk | VsCoq 2, new foundations CoqPL File Attached | ||
16:45 22mTalk | Integrating Dependency Building with Document Checking in Coq CoqPL File Attached | ||
17:07 22mTalk | A diagram editor to mechanize categorical proofs CoqPL Ambroise Lafont Ecole Polytechnique File Attached |