Rudi Grinberg (Aug 19 2020 at 19:44): Rudi Grinberg (Aug 19 2020 at 19:44):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?
Gaëtan Gilbert (Aug 19 2020 at 19:54):https://github.com/coq/coq/pull/12567
Last updated: Sep 23 2023 at 06:01 UTC