[misc] Remove special code paths used in the Stdlib transition.

[ejgallego]

#19530 turned the standard library into a regular library installed in user-contrib, however, we still have some special code paths in Coq due to compatibility. These code paths are fairly low-level and should be eventually removed.

In particular, these code paths allow users to skip the From Stdlib when doing a Require Import foo where foo is a stdlib module, and some Coq / Stdlib renaming mappings in several places.

Moreover, we still load the prelude, unless -noinit is passed. We could consider requiring users to do From Stdlib Require Import Prelude so the dependency on the prelude is now explicit.

See also the original bug #5257 for the deprecation.

[SkySkimmer]

This has many advantages

Can you be more specific?

[Alizter]

One advantage is that we don't have to do all this special case handling with boot and noinit that we currently have to do. This will simplify some of our infrastructure and allow us to eventually make the stdlib more modular.

[Alizter]

It will also stop users from getting confused. If I have a List.v file in my project and I write:

Require Import List.

Am I talking about Stdlib or my project?

[Alizter]

Here is an idea from @rgrinberg. We could add an option to coqc "-open" which would by default open a module prefix allowing the From to be forgone. For instance, if we start requiring (or warning about) From Coq everywhere, we should allow people to pass -open Coq to their build if they don't want to transition.

[SkySkimmer]

So we could replace -R path foo with -Q path foo -open foo?

[ejgallego]

As I noted in Zulip, -open is more akin to Require Import IMHO, so not sure that should be the right name to signal the current theory. Actually, Coq can automatically deduce what is the current theory and remove the need for From automatically.

[Alizter]

@ejgallego For the current theory, Coq can correctly deduce the From part. That is fine. I am talking about people using -R for other theories in their projects. The main one being the coq standard lib. The -open flag it supposed to replace these uses of -R. Nobody should be writing -R.

[ejgallego]

Yes, nobody should be writing -R, nor -open if we want.

[Alizter]

@ejgallego Getting everybody to decorate their Require Imports of the stdlib with From Coq is quite a large task. I would start with deprecating and removing -R first, adding -open as a transnational replacement, and then eventually remove that.

[ejgallego]

What's the point? How are -R and -open different other than in name?

[ejgallego]

Also, -open is a bad name for the reasons I've explained.

[ejgallego]

If you want this kind of flag, the best name according to Coq's terminology is -implicit-path

[Alizter]

-R will recursively -Q all subdirectories with logical names matching/

-open will instead give Coq an alternative From _ to try on a naked Require Import.

[ejgallego]

Then -implicit_from may be better. Open means "Import" which IMHO has a different semantics.