Stream: Coq devs & plugin devs

Topic: ✔ Is -Q recursive?


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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 16:53):

Yes it is Enrico

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 16:54):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 16:54):

Once you use From there is also a wildcard

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

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

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

view this post on Zulip Notification Bot (Feb 03 2022 at 09:39):

Enrico Tassi has marked this topic as resolved.


Last updated: Feb 01 2023 at 16:03 UTC