Integrating Dependency Building with Document Checking in Coq
summary
Prototype integrates a build system into coq-lsp by handling Require as an effect using algebraic effects in OCaml 5, so the server checks dependencies on demand and records reverse dependencies in three document states (initial, pending, completed). Empirical data shows the standard library’s 585 files lead to 65,000 .vo passes in practice, costing roughly 8% of total time; the prototype memoizes requires, halves some memory use when sharing parsed files, and currently runs as a single-threaded prototype that works and yields measurable savings.
AI-written summary · about
chapters (10)
- 0:00Co LSP introduction
- 3:32Design key ideas
- 5:18Algebraic effects for dependencies
- 7:26Document states and incremental checking
- 10:17Handling updates and cycles
- 11:00Demand-driven vs batch builds
- 12:45Performance gains from require handling
- 14:51Future work and error recovery
- 16:16Q&A timeline and setup
- 17:23Q&A input formats and parallelism
related talks
21mLive Verification in an Interactive Proof Assistant
26mIntegrating graphical proofs in Coq
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
56mSession with the Coq Development Team
07h 18mFull Workshop
15mBuild Scripts with Perfect Dependencies
16mThe Modular Imperative: Rethinking LLMs for Maintainable Software
58mDespagghetifying code with NDepend