Bottlenecks in standard library

[mrhaandi]

Description of the problem

The standard library contains files such as Reals/Ranalysis.v, which mainly contain Require Export xyz.
This is great for users (no need to search the exact file names). However, when used in the standard library internally, this creates a bottleneck with respect to parallel compilation of the standard library.

For example, Reals/NewtonInt.v contains Require Import Ranalysis., which (among others) exports Rgeom.
However, Rgeom is not necessary for NewtonInt. Still in parallel compilation NewtonInt needs Rgeom to compile first.

Avoiding unnecessary bottlenecks by better import management in the standard library may improve parallel compilation speed.

Coq Version

8.17

[herbelin]

That's a good point. The original design of Reals had this chain of Export but more parallelism would indeed be nice. If you already made such finer analysis, that would be worth a PR (in my personal opinion).