Warning: this is likely very naive.
I'm wondering if it's possible to ship coq's standard library in a separate package. The main reason why I thought of this is that dune's CI needs coq to test the coq rules, and coq's installation ends up dominating dune's CI times. I'm conjecturing that there's a lot of unnecessary coq code being built here. It would be nice to depend on just the compiler.
Of course, this split could have other benefits. For example, users can upgrade the standard library without updating the compiler (when it's possible).
Was this ever discussed before?
Last updated: Feb 06 2023 at 11:03 UTC