Stream: Coq users

Topic: Separate package for the standard library?

view this post on Zulip 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?

view this post on Zulip Gaƫtan Gilbert (Aug 19 2020 at 19:54):

Last updated: Feb 06 2023 at 11:03 UTC