ceps
ceps copied to clipboard
coq
Boost stdlib development
This is a CEP to discuss the technical details of the corresponding point of the roadmap https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md
Rendered: https://github.com/proux01/ceps/blob/boost-stdlib-dev/text/083-boost-stdlib-dev/text.md
Could you please say more about the advantages of the proposed system over the current one -- why should we do what you say under "Motivation"? We clearly have different intuitions here, and to make a good decision we'll need to understand why we each want what we want. I have opined here.
Thanks for the CEP @proux01 , a few comments:
- I think that the CEP covers two orthogonal set of tasks, namely:
- splitting the stdlib into several packages
- removing the stdlib's special status (c.f. https://github.com/coq/coq/issues/16091 ) IMHO it would make sense to decouple these two tasks, as IMHO they do seem to have very different granularity.
- I think a critical aspect to this CEP is integration with tooling (build systems, package managers, doc, search tools, etc...) I think we have pretty good evidence that such a granular split of the stdlib has the potential to impact users pretty negatively unless tooling can compensate the added difficulty.
IMHO I would thus do the removal of the stdlib status right now (tho the plan is missing some technical details), and I'd try to study / develop more the usability aspects of the stdlib split.
* I think that the CEP covers two orthogonal set of tasks, namely: * splitting the stdlib into several packages * removing the stdlib's special status (c.f. [[build] Turn the Standard Library into a regular library coq#16091](https://github.com/coq/coq/issues/16091) ) IMHO it would make sense to decouple these two tasks, as IMHO they do seem to have very different granularity.
I agree those are two quite diferent things. But they are not fully orthogonal either. For instance, doing the second thing implies separating the prelude (+ probably Setoid and the like) which is already a package split. So doing both things at the same time may actually save some effort.
* I think a critical aspect to this CEP is integration with tooling (build systems, package managers, doc, search tools, etc...) I think we have pretty good evidence that such a granular split of the stdlib has the potential to impact users pretty negatively unless tooling can compensate the added difficulty.
Could you please elaborate? We already have working package managers (Opam and Nix). My experience with mathcomp is that keeping both a make-all target and separate packages allows both comfort for developers (who can just type make to build everything withut worrying about the package split) and users (who can easily use only part of the, large, library). Tests in CI ensure that we don't break any of the two builds accidentally. I guess this setting is working well enough for mathcomp, as I can't remember any complaint about it. Do you see any fundamental difference between the stdlib and mathcomp that would turn this wrong? (at least my small prototype in the CEP convinces me that the mathcomp setting is replicable for the stdlib)
IMHO I would thus do the removal of the stdlib status right now (tho the plan is missing some technical details),
Please elaborate on those "missing technical details", that's the whole point of CEPs
and I'd try to study / develop more the usability aspects of the stdlib split.
What are precisely the points you think deserve further study / development?
A point that troubles me is that the files PArray, Sint63, Uint63, FloatAxioms are moved outside of Coq. In my opinion, files that describe the computational behavior of Coq's kernel should be tightly coupled to Coq's kernel. We cannot have an independent user library be the authoritative source of the reduction rules of Coq's builtin symbols.
I am not saying that these files should be kept in Coq in their entirety. But all the Primitive and Axiom declarations they contain should stay. The downside is that part of ZArith has to be kept in Coq too, so that the axioms can be expressed. But it would just be the Definition declarations of ZArith; no lemmas are needed. (This is not that different from what you did with FloatAxioms; only some definitions were moved from Flocq to Coq; all the theorems, especially those about real numbers, stayed in Flocq.)
@proux01 would you be willing to engage with me on this topic, in a medium of your choice? I see the value of some aspects of this CEP (e.g., cleaning up the dependencies within stdlib and spinning out obscure functionality) but leaving users overall at the mercy of an ecosystem of small independent packages evokes the horrors of npm & leftpad in my imagination. I figure that's not what you want either, but it's really hard for me to see what considerations would outweigh the costs of not having one standard definition of the integers and similarly basic concepts. :pray: Thanks!
A point that troubles me is that the files
PArray,Sint63,Uint63,FloatAxiomsare moved outside of Coq. In my opinion, files that describe the computational behavior of Coq's kernel should be tightly coupled to Coq's kernel. We cannot have an independent user library be the authoritative source of the reduction rules of Coq's builtin symbols.
Good point
I am not saying that these files should be kept in Coq in their entirety. But all the
PrimitiveandAxiomdeclarations they contain should stay. The downside is that part ofZArithhas to be kept in Coq too, so that the axioms can be expressed. But it would just be theDefinitiondeclarations ofZArith; no lemmas are needed.
Indeed, I updated the CEP / prototype accordingly. This adds 15 files / 2.1 kloc (almost half of them for the ZArith definitions).
would you be willing to engage with me on this topic, in a medium of your choice?
@andres-erbsen we can have a lengthier discussion on Zulip for instance
This CEP should be discussed during a forthcoming Coq Call: https://github.com/coq/coq/wiki/Coq-Call-2024-03-05
~~Could we have this coq-call discussion the week after, on the 12th? I'm unsure whether I'll be able to make it on the 5th, but I would very much like to participate (and ideally get in some one-on-one iteration with @proux01 first as well).~~
Had a productive discussion with @proux01; notes below.
Between the two of us, there seems to be agreement that increased clarity of dependency structure within stdlib would be valuable (this is Emilio's first point above, let's call it the "build split"). In particular, there is a common experience where contributing to stdlib is stifled because it is unclear what other files each particular file can import. @proux01 has already done the technical work required to make this happen, and while the dependency tree is gnarly, it is better than nothing, and capturing it in code would be an important improvement to stdlib maintenance. There also seems to be low-hanging fruit in terms of improving the developer experience further, for example by providing build targets that only build subsets of stdlib for intermediate feedback during prototyping. And I think it is independently valuable to identify "orphan" parts of stdlib that are not depended on internally, such as Sets and Reals, so they can be considered for spin-out.
As for removing stdlib from Coq (let's call it the "distribution split"), @proux01 is much more optimistic about the immediate user-facing impact than I am. This disagreement reflects different attitudes towards third-party packaging of coq and stdlib, and whether we consider the experience of users who rely on these packages to be in part a responsibility of coq developers. Specifically, I argue that if we are going to make a drastic change in packaging (going from 1 package to 20+), this should be coordinated closely with the maintainers of downstream packages; making this change without their approval is asking for trouble for all users further downstream. Similar issues to what I expect already happened with the build-system changes a few years ago; I am just trying to urge us to do better now. I personally rely exclusively on linux-distribution packages for Coq when I am not building from git, and I would guess almost all people I work with do the same; I do read on the community survey that opam is twice as popular but it is unambiguously not the only game in town. Thus I would like to see a clear, package-maintainer-approved plan for the distribution split, with a focus on minimizing disruption to users who want the entire stdlib. I personally consider the possible complications from the distribution split not to be worth the likely benefits, but if it is to happen, I am willing to help out to make sure it goes smoothly. As a contributor to Arch and Alpine Coq packages, I would prefer if the many-way split was preceded by a smaller-scale canary (perhaps just spinning out Reals).
One technical point that came up is the relationship between plugins and theory they support: on one hand, plugins are tightly coupled with Coq due to the use of the ML API, so it would make sense to keep them with Coq. @proux01 expects changes to plugin-gallina interfaces to be much less common, so putting e.g. lia and Z into separate repositories would work fine. I am less confident of this based on work I've followed, but perhaps @coq/micromega-maintainers can offer us an opinion from the close up?
As for non-technical aspects of specifically removing the special status of stdlib, I agree with this goal only for the less-frequently-used parts of the stdlib. I think it is in the interest of the community for very commonly used theory such as list, Z, bool, wf, ring, lia, and etc to continue to be distinguished and maintained centrally, by a subteam of coq developers. (The community survey agrees that these are the most popular parts).
Both of us also agree that there is long-term value in curating a cohesive, non-duplicative core of coq libraries and that this CEP isn't really about solving that. This is a much more ambitious and distant goal than figuring out how the current stdlib theories should be maintained. We agree that attracting more contributors would be valuable, and that we don't really have a promising plan for how to do that. Perhaps I should do a CEP on the more general topic of library-ecosystem stewardship; hopefully it can be relatively independent from this one though.
This disagreement reflects different attitudes towards third-party packages, and whether we consider the experience of users who rely on them to be in part a responsibility of coq developers.
By "3rd party packages" do you mean "coq packaged by someone" like https://packages.debian.org/stable/math/coq or "package using coq" like mathcomp etc?
@SnarkBoojum in case you haven't noticed it, you may be interested by the discussion above, as a Debian package maintainer
Two other points that came up:
-
We agree that the current situation when it comes to handle PRs to the stdlib is not great. I do hope that having a dedicated repo, not mixing stdlib PRs with Coq ones, could help. @andres-erbsen doesn't share my optimism.
-
we currently have
- coq-core
- coq-stdlib
that will become
- coq-core
- prelude, setoid, defs and axioms for primitive types spec
- remaining of current stdlib
this PR offers to keep coq-stdlib for 2. and use a new name (for instance "roots") for 3., but that's of course part of what should be settled by the CEP.
Both of us also agree that there is long-term value in curating a cohesive, non-duplicative core of coq libraries and that this CEP isn't really about solving that.
While I agree this CEP is not about solving that, I believe that the possibility of developing such a cohesive library is strongly conditioned by the right choices happening here.
@proux01 Thanks for pinging me, I indeed didn't follow this ticket.
On the Debian side, the coq source package already provides five different binary packages, so a split in different upstreams wouldn't be painful: bin:libcoq-stdlib would be provided by src:coq-stdlib instead of src:coq.
Since I packaged quite a few Coq-related packages, I have the impression that there are:
- some parts of the stdlib are experiments and not used outside -- they could be dropped or kept aside ;
- that other parts are incomplete but useful hence a few projects have supplements that could be merged ;
- that some things are just absent hence a few projects provide supplements that could be merged.
Notice the "could be merged" is easily said: the various downstreams almost certainly didn't complement in coherent ways with one another, so deciding what and how to merge will probably mean everyone will have some work to cope with the merge.
But still, after the initial period where everyone will be unhappy because things get broken everywhere, having a more fluid stdlib will mean people will actually contribute to it instead of adding their own ideas on their own, so that means less duplication on the whole.
That looks pretty positive.
Even with the recent changes, I find myself agreeing with the title of the CEP and struggling to relate to most of the content. I will respond to the points that I find salient and then sketch some thoughts beyond.
ensure that the stdlib does not enjoy special status
I would like to make sure that the stdlib is special in a specific sense: it should be is the comprehensive collection of theory that is expected to be useful to most Coq users and on whose design there is rough consensus. This means, for example, that concrete objects such as nat are in, and pervasive algebraic hierarchies are out because we have not managed to converge on a generally accepted solution, but so be it.
but without their historical origin
I would like to see the stdlib overcome its origin, but through evolution, not deprecation. For example, I think we should replace FMaps with stdpp maps, port the users that we can, if necessary have users that cannot be ported depend on an external FMaps artifact. The invariant here should be that stdlib contains the generally recommended solutions, and in cases we know we have failed to maintain this invariant, we should fix it.
that would be worth distributing as separate packages [...] Allow maintainers to extract stdlib components to maintain and evolve them outside the core Coq repository and to have their own release schedule and versioning scheme
I see the costs of this kind of fragmentation as very high, so perhaps Reals is the only part of stdlib that I would currently consider deserving of separate distribution.
allow other libraries to use newer features of Coq (like universe polymorphism, SProp and primitive projections).
I would love to use these features, but when we tried to use them in coqutil, they were not ready. Stdlib rigidity is not what is keeping us back here. On the contrary, whether we are able to use a feature in stdlib is a good litmus test for whether that feature is ready for general adoption.
Maybe most importantly: currently the stdlib cannot depend on anything else than Coq itself.
To me, the stdlib being self-contained, cohesive, and under one maintainership is the most valuable aspect of it (even given current realities on these axis). Instead of having stdlib depend on independently maintained projects, we should consider merging functionality such as Equations, itauto, and Zmod that were developed independently.
We should do an open call for maintainers
Yes, we should. Right now, to join us in plotting the future of stdlib, not after we have made a decision that might alienate some potential candidates.
The stdlib will no longer come bundled with Coq. It will however be just as easy to install via the usual package managers.
IMO this is a hard requirement for packaging split; and "the usual package managers" should include the up-to-date ones on repology and other popular options from the community survey.
The extreme opposite would be to lean toward a huge monorepo with everything from the platform
Just to be clear, I am not arguing for this extreme: the platform is highly duplicative and contains incompatible versions of many things, the stdlib should be curated for cohesion. And for maintaining a cohesive library, a monorepo for that library is the best path IMO.
[Monorepoa] also has one major drawback: it makes it harder to have the following dependencies:
coq-roots-A <- coq-extralib-B <- coq-roots-C.
As I said above, IMO this is a feature.
Specifically on whether to split the repo (coq+stdlib) or not, the only concrete argument in favor of splitting is that contributors could then subscribe to notifications on stdlib only. I propose instead implementing a bot that CCs them on stdlib PRs.
Instead, I would like to see the following:
- An immediate call for maintainers, with a well-lit path for getting started, gaining acceptance, and receiving the bits. This shall not rely on one being in France, coming to Coq calls, or any specific affiliation; instead we should take competent maintenance of a coq development outside stdlib as a strong positive indicator.
- A call for contributions of theory that ought to have been in stdlib in the first place, perhaps with an associated event during which we coach new contributors on this. stdpp and coqutil are examples of what to pull in first.
- Laxer compat policy for non-CI developments: we should require maintainer consensus that reasonable uses of stdlib can be ported in a sane backwards-compatible way, but needn't strive for zero-porting updates.
- A bot for subscribing to stdlib PRs and issues.
I think the continued evolution of library would be greatly helped by:
- An overlay "future" library (a la python) that makes stdlib of coq version n available on coq version n-1 whenever possible, with a streamlined process (or even a bot?) for simultaneously contributing to both.
- A megabuild like coq-universe for users for whom we can provide it today (probably not fiat-crypto any time soon though :/)
- More, faster CI runners (<40min per full ci is possible and would be immensely valuable)
- A CI policy restricting external dependencies of CI targets to help developers build it more easily locally
@andres-erbsen thanks for your message, I agree with your vision. I think tho we are short of the technology / tooling needed to implement the challenges of this model in a developer-efficient way.
By the way fiat-crypto builds in coq-universe just fine; as long as a coherent set of packages can be found.
We have in dune the %{coq:version} variable that can be used to implement fiat's-crypto build logic. Now thanks to (dynamic_include ...) there is little the cannot be done in the Dune side.
The thing that has blocked further progress on coq-universe is actually silly: the lack of a good way to manage the submodules.
As it stands today, it is just too much overhead to not to be able to perform git operations in the coq-universe repos in a way that submodules are handled well.
Lean has the lake stuff, that is something we could adopt in Coq. IMVHO that is the advantage that Lean has on not relying on a language like OCaml: they do deploy their own, single tooling; while we have to reuse OCaml tooling by force.
opam is not well adapted to the workflow lake-like tools (or cargo) enable, thus we are lacking here; deploying our own solution is pretty heavy resource-wise. Ummm.
The thing that has blocked further progress on
coq-universeis actually silly: the lack of a good way to manage the submodules.As it stands today, it is just too much overhead to not to be able to perform
gitoperations in thecoq-universerepos in a way that submodules are handled well.
Can you elaborate on what the issues are here?
Lean has the
lakestuff, that is something we could adopt in Coq. IMVHO that is the advantage that Lean has on not relying on a language like OCaml: they do deploy their own, single tooling; while we have to reuse OCaml tooling by force.
opamis not well adapted to the workflowlake-like tools (orcargo) enable, thus we are lacking here; deploying our own solution is pretty heavy resource-wise. Ummm.
Is there a description of this workflow somewhere? (Or could you describe it?)
The thing that has blocked further progress on
coq-universeis actually silly: the lack of a good way to manage the submodules. As it stands today, it is just too much overhead to not to be able to performgitoperations in thecoq-universerepos in a way that submodules are handled well.Can you elaborate on what the issues are here?
We have a bunch of submodules, some with commits on top of the master branch. Keeping these up to date is a lot of manual rebasing etc. We looked around for existing solutions to this issue but it seems the best solution is to just write some scripts to do this. The amount of work makes it quite difficult to keep the entire repo up to date.
https://github.com/coq-universe/coq-universe
Thank you all for the input on tooling! I agree it is important, and I am encouraged by the response. The perspective from which I am writing here is that we should first figure out the workflow we want, prototype it using manual chores instead of tools, and invest in tooling once we have decent confidence that we would be happy with what we're building up to. Perhaps the vision is already there, and I just need to learn about it. Regardless, the way I think of it, the broad question about future of stdlib is more about people and processes and less dependent on current state of tooling.
We have a bunch of submodules, some with commits on top of the master branch. Keeping these up to date is a lot of manual rebasing etc. We looked around for existing solutions to this issue but it seems the best solution is to just write some scripts to do this. The amount of work makes it quite difficult to keep the entire repo up to date.
The way I'd solve this is by having two submodules for each development, one that tracks upstream and one that has a branch to be merged into upstream (a folder of patches to apply might work just as well). Dependabot can update the upstream submodules, and CI should merge in the changes / apply the patches before building. Would this work?
We improved the motivation section of the CEP.
Let's proceed with the discussion during April 23rd call: https://github.com/coq/coq/wiki/Coq-Call-2024-04-23 Meanwhile, it would be great if the alternative offers could be elaborated in the "Alternatives" section of the CEP, in order to structure the discussion.
the comprehensive collection of theory that is expected to be useful to most Coq users and on whose design there is rough consensus
I guess we all agree that's what a standard library should be. Unfortunately, the current stdlib is full of things that don't make consensus, or even gather a strong consensus against them.
pervasive algebraic hierarchies are out because we have not managed to converge on a generally accepted solution
BTW note that if we are strict on this, it does actually exclude quite a lot. Even the way the theory on nat is built in the current stdlib is a kind of algebraic hierarchy construction after all.
not deprecation
The CEP offer to move the stdlib to its own repo, so that it can be kept / evolved in better conditions than it currently endures. Deprecation means intent to remove, that's a totally different thing.
The invariant here should be that stdlib contains the generally recommended solutions, and in cases we know we have failed to maintain this invariant, we should fix it.
Again, we all agree on that definition of an ideal stdlib and should aim in that direction. But the current stdlib is so far from that objective that the best way to reach it, without breaking everything, is far from obvious. Meanwhile, let's first try to improve the current situation by reaching a state were just moving into that direction seems more realistic.
I see the costs of this kind of fragmentation as very high, so perhaps Reals is the only part of stdlib that I would currently consider deserving of separate distribution.
This is a straw man, the CEP reads "Allow maintainers to extract stdlib components [...] in case they wish to do so.". It's about enabling it in case it would make sense, not splitting everything upfront (which I agree would certainly be very bad).
I would love to use these features, but when we tried to use them in coqutil, they were not ready. Stdlib rigidity is not what is keeping us back here. On the contrary, whether we are able to use a feature in stdlib is a good litmus test for whether that feature is ready for general adoption.
We should also understand that developers of new features don't necessarily have time / motivation to adapt an entire library. Having a more delimited prelude only to adapt could also help the development of such new Coq features, by enabling their adoptions first in basic libraries like the stdlib then in their reverse dependencies. If the development of the stdlib is stuck like currently, that could indeed be blocking the feature spread.
We should do an open call for maintainers
Yes, we should. Right now,
IMHO, that would be the worst thing to do. If I were such a new maintainer, I would certainly feel more frightened by the current discussion, than welcomed. Resolving that discussion and setting a more welcoming development environment seems to me like a strong prerequisite to a successful call for new stdlib maintainers.
Specifically on whether to split the repo (coq+stdlib) or not, the only concrete argument in favor of splitting is that contributors could then subscribe to notifications on stdlib only. I propose instead implementing a bot that CCs them on stdlib PRs.
Well it's much more than that: not having all the frightening OCaml code around, the review process that may be too heavy...
Instead, I would like to see the following:
Yes, please add a concrete proposal in the "Alternatives" section of the CEP so that all alternatives can be efficiently discussed.
This shall not rely on one being in France
[off topic] Sure, are we doing anything really bad wrt that point currently? Of course, for historical reasons, most Coq developers are french people and that reflects on the few physical meetings for practical reasons. But besides that, it seems to me that we make our best to make all public conversations happen in our best-possible English and be as welcoming as possible to non-french people. Is there anything you feel we could improve? [/off topic]
coming to Coq calls
Yeah, I guess stdlib maintainers could set their own set of calls if they wish so. And I agree that needing to attend a Coq call to just ask for a PR review, is a pretty terrific situation.
or any specific affiliation
Sure, are we doing anything really bad about this currently?
An overlay "future" library (a la python) that makes stdlib of coq version n available on coq version n-1 whenever possible, with a streamlined process (or even a bot?) for simultaneously contributing to both.
Just decoupling stdlib releases from Coq ones would make it much easier for each version of the stdlib to support multiple versions of Coq, just like most regular libraries do. That would be one of the advantages of the dualrepo approach.
A CI policy restricting external dependencies of CI targets to help developers build it more easily locally
This is quite orthogonal to the current CEP (maybe you should open a CEP about CI to discuss that kind of things). [off topic] But TBH, as a Coq developper, the current depth of the dependency tree in the CI doesn't feel particularly painful. The long compilation times of some of the developments and having to struggle with things like submodules feels much worse (hope the recent developments will improve things on that point, I haven't experienced them first-hand yet ;) ). The lack of clarity of the CI contract about some points also doesn't help and can make us feel more enslaved than helped by the CI. [/off topic]
Quick clarifying responses below; I am working on putting together something more structured and comprehensive.
nat is built in the current stdlib is a kind of algebraic hierarchy construction after all
But it's not pervasive -- most users don't even know it's there!
Deprecation means intent to remove, that's a totally different thing.
We should also understand that developers of new features don't necessarily have time / motivation to adapt an entire library
Which one of these do you mean? It really does feel like the goal of this CEP is to get the current stdlib out of the way and make way for its replacement, as opposed to reinvigorate it. (And see coq/coq#18870 and coq/coq#18871 for fresh samples of what new Coq features are stuck on -- basic tactics, not the theory you are proposing to (re)move here.)
Sure, are we doing anything really bad wrt [favoring France] currently?
I sure feel left out, and sometimes mystified by responses from the Coq team. I have been suggested that this is because I am not present in the in-person meetings.
We improved the motivation section of the CEP.
Who is "we"?
current depth of the dependency tree in the CI doesn't feel particularly painful
It's not the depth that is the issue, it is dependencies on random opam and other packages.
I don't think we should burden the stdlib with support for multiple Coq versions as we are already struggling to keep up with features present in one.
I guess we all agree that's what a standard library should be. Unfortunately, the current stdlib is full of things that don't make consensus, or even gather a strong consensus against them.
Could we try to list somewhere examples of what are consensual and non-consensual aspects of libraries (e.g. as an appendix of the CEP, or on a wiki page, complementing e.g., for the current stdlib, this wiki page)?
Also, how easy or complicate would it be to address what does not make consensus in the current libraries? (For instance, I've heard questions about heterogeneity, in naming, in order of arguments, in style; I've heard questions about using bool or Prop for decidable propositions; I've heard questions about having only le or also ge, about notations, about documentation, about complexity of use, about policies, about reusability, ... I don't feel all that unsurmountable.)
If the main objective is to join the best of all our efforts into something that is usable and satisfactory to all users, let's do it.
[off topic] (but I don't know where to put this)
I sure feel left out, and sometimes mystified by responses from the Coq team.
Can you elaborate? (although I understand that precising a feeling can be difficult)
I have been suggested that this is because I am not present in the in-person meetings.
That's pretty unclear to me. I'm myself not present to that many in-person events and don't feel excluded. We should also acknowledge that you are part of the dev team of fiat_crypto, which presents many differences with the remaining of the Coq ecosystem, and some long lasting tensions, in particular around backward compatibility and CI. I'd expect this to play a much more important role than location.
It's not the depth that is the issue, it is dependencies on random opam and other packages.
Interesting, I've never felt really impeded by that. You setup your system once and for all, whichever way you want (no obligation to use opam). It's not like you would need to recompile everything everytime or things would be constantly changing at a fast pace. [/off topic]
I don't think we should burden the stdlib with support for multiple Coq versions as we are already struggling to keep up with features present in one.
I'm not sure it would be that hard / much extra work. Anyway, I was just mentioning it because you suggested a solution that looked more labor intensive.
[off topic] (the discussion about how to evolve the stdlib is a very interesting one, and one that we should have, but it goes way beyond the objectives of the current CEP)
Also, how easy or complicate would it be to address what does not make consensus in the current libraries? (For instance, I've heard questions about [...] I don't feel all that unsurmountable.)
I agree none of that is insurmontable, it's rather the amount of such small things, accumulated over the stdlib history, that make it a huge endeavour. [/off topic]
My issue with this CEP is that it presumes a conclusion to the more general discussion about stdlib -- that we don't want it to be as central and distinguished as it is now. Changing the way stdlib is compiled to enforce internal dependencies is not controversial IMO.
Wdyt about moving the very-off-topic discussion to a zulip thread, maybe "future of stdlib maintainership"?