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 architecture 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 undesired 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 significant 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.