I want to use some theorems from the list module of stdpp. I don’t want to Import it because it is a large library and it clutters the global namespace with notation and names that I want to use for other things (like partition). So, I tried doing the following:
From stdpp Require base list.
Check list.elem_of_cons. (* The reference list.elem_of_cons was not found in the current environment. *)
In previous versions of Rocq/Coq this worked fine, but after upgrading from 8.20.0 to 9.0.0 this no longer works. It seems that the list module re-exports list_basics, list_monad etc., which each internally define their own list module that exports its symbols (see stdpp.list), but this does not work well when using Require only…
Selective import Import list_basics(elem_of_cons). does work, but does not play well with notations like Notation head := hd_error., and it would be rather tedious to do this for every symbol I want to refer to, and the documentation notes that I should not rely on the organization of these internal modules.
As a side note, it seems like the rocq-stdpp package that is listed on Iris / stdpp · GitLab does not exist in the repository that is listed there:
$ opam repo list
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
<><> Repository configuration for switch default ><><><><><><><><><><><><><><><>
1 rocq-released2 https://rocq-prover.github.io/opam/released/
2 rocq-released https://rocq-prover.org/opam/released
3 default https://opam.ocaml.org
$ opam install rocq-stdpp
[ERROR] No package named rocq-stdpp found.
I could not create an issue on the MPI-SWS gitlab because I cannot create an account there (“An error occurred while validating username“).
I guess they have chosen to rename the package but they have not yet released it under the new name. You can either use the latest released version, which is named coq-stdpp, or use their development version with a command akin to opam pin add rocq-stdpp https://gitlab.mpi-sws.org/iris/stdpp.git
Oh, so when a Rocq module Eports other modules, it does not make those modules available under its own namespace?
That is very odd. IIRC the same does happen when you use an explicit Module (we make use of that here), so somehow file modules and Module modules behave differently? Or is there something else going on?
As that readme explains, you need to add the Iris opam repo to get the latest development version.
This is odd. Have you tried a different username? If yes, could you send me a DM with the username and email address you tried? I can forward that to the admins so they can have a look. Unfortunately spammers make it very hard to run a public gitlab instance, so our admins need to do very aggressive spam filtering.
What do you mean? The commands Import and Export are purely about visibility. They never reroot any symbol under a new module, be it a file module or a Module module.
Module Foo.
Module M.
Definition bar := O.
End M.
End Foo.
Module Baz.
Export Foo.M.
End Baz.
Fail Check Baz.bar.
Fail Check Baz.M.bar.
Fail Check Baz.Foo.M.bar.
Succeed Check Foo.M.bar.
Okay I guess this answers my question why it is like this. It is just not what I would have expected coming from programming languages like C++/Rust where using/use do work like this.
Still I’d like to know if there is any way to do Require on all of these list sub-modules and be able to refer to all the symbols by list.symbol_name. (Or, in your example, do some variation of Require Baz and then use Baz.bar.) If I can’t do this it means I cannot really upgrade to the newer std++ version because I would need to change the style of my 22,000 line repo…
Ah, we must be doing something else different for the other module then.
It’s a shame that the Rocq module system seems to have no proper support for “facades”, where the internal module organization is hidden from the public API.
I would suggest you file an std++ issue but we have to first resolve the problem with the gitlab account for that – see my comment in the previous post. Meanwhile, I have created an issue for you.
All the symbols in list_basics etc are already wrapped in a list module, so it should be possible to refer to them as such. But clearly some further trickery is needed to make this actually work.
Oh I assumed that there was already a stable version of rocq-stdpp but this is not true.
Thank you, I ended up logging in through github. On Sign up · GitLab I have tried different usernames including ones that are just random characters but in the console I see a 401 response with error “You must be authenticated to access this path.” When I click “Sign up” anyway, it redirects me to the sign-in page, seemingly without actually having created the account.
Yes, that is the only way AFAIK. I don’t know how you even found the other form, the website does not link to it at all. You can’t use a random URL on a server that’s not linked anywhere and then expect that to work (and then not even mention that you used such a hidden URL when you talk about things not working!).
I didn’t know it was a hidden URL and that it wasn’t linked from anywhere… it seems like bad UI that a user should infer that the publicly accessible Sign in · GitLab page with the “username” and “password” fields also has no way to be used because you cannot create a username and password. But maybe that is just how gitlab works, I don’t know.
I mean, you clearly entered the URL in the URL bar without clicking a link. That’s not a “supported” way of interacting with any website I am aware of.
I agree the UI isn’t great, but it is just how gitlab works when local registration is disabled (and it sadly had to be disabled due to an enormous amount of spam bots, and no good tools in gitlab to deal with them).
That’s not a “supported” way of interacting with any website I am aware of.