POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 16:45 - 17:07 at Kelvin Lecture - Session 4

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.