Stream: Coq devs & plugin devs

Topic: ✔ Is -Q recursive?

Enrico Tassi (Feb 02 2022 at 16:52):

I'm toying with -Q d p and it seems it is recursive: it does add d and all its subdirectories. Has it always been like that? (I did read the doc, and not really understood it)

Emilio Jesús Gallego Arias (Feb 02 2022 at 16:53):

Yes it is Enrico

Emilio Jesús Gallego Arias (Feb 02 2022 at 16:54):

Difference is only that with -R doesn't require From foo

Emilio Jesús Gallego Arias (Feb 02 2022 at 16:54):

Once you use From there is also a wildcard

Guillaume Melquiond (Feb 02 2022 at 17:48):

Enrico Tassi said:

I'm toying with -Q d p and it seems it is recursive: it does add d and all its subdirectories. Has it always been like that? (I did read the doc, and not really understood it)

The documentation says (and it is mostly unchanged since its inception in 8.5):

A logical prefix Lib can be associated with a physical path using either the command line option -Q path Lib or the command line option -R path Lib. All subfolders of path are recursively associated with the logical path Lib extended with the corresponding suffix coming from the physical path. For instance, the folder path/Foo/Bar maps to Lib.Foo.Bar. [...] For example, the name associated with the file path/Foo/Bar/File.vo is Lib.Foo.Bar.File.

Are there some suggestions to improve it?

Enrico Tassi (Feb 02 2022 at 20:53):

I was talking about this: https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Add-LoadPath
The text you quote is fine. Where is it?

Guillaume Melquiond (Feb 02 2022 at 21:29):

https://coq.inria.fr/distrib/current/refman/language/core/modules.html#libraries-and-filesystem
As for Add LoadPath, its meaning might indeed have changed in 8.5. It was non-recursive and became recursive. From a backward compatibility point of view, the change was almost transparent. And that way, I did not have to add Add RecButNonRec LoadPath but I could just reuse Add LoadPath.

Notification Bot (Feb 03 2022 at 09:39):

Enrico Tassi has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC