Stream: Coq devs & plugin devs

Topic: ✔ gitlab.inria.fr account?

Jason Gross (Oct 26 2021 at 23:16):

Would it be possible for me to get an external gitlab.inria.fr account? I'm trying to make an issue request on Flocq that it install .glob files

Emilio Jesús Gallego Arias (Oct 27 2021 at 00:50):

Yes you can, tho it is mostly useless [but may work for issues]

Emilio Jesús Gallego Arias (Oct 27 2021 at 00:51):

Instead let's doubly ping @Guillaume Melquiond , for a) take note of your request, and b) hopefully convince him to move flocq to an open hosting platform

Karl Palmskog (Oct 27 2021 at 05:56):

if the issue due to Flocq installation, then other projects that use the same build systems (remake) such as Coquelicot are probably also affected

Guillaume Melquiond (Oct 27 2021 at 06:02):

To be clear, this has nothing to do with the build system. Even when I was using make, I had already decided against shipping files that end users cannot make use of.

Emilio Jesús Gallego Arias (Oct 27 2021 at 08:07):

Glob files are required if users want to build docs properly aren't they?

Emilio Jesús Gallego Arias (Oct 27 2021 at 08:07):

But indeed Coq packages should be consistent, if coq_makefile / dune do install glob files, flocq should too

Guillaume Melquiond (Oct 27 2021 at 08:10):

No, unless I am missing something, you cannot build the documentation after the fact (i.e., from already installed files rather than source files), so installed glob files serve no purpose with respect to documentation.

Théo Zimmermann (Oct 27 2021 at 08:25):

Yes, @Jason Gross, getting an Inria external account nowadays requires getting a sponsor and the sponsor renewing the sponsorship every year. I can do that for you if you want (I already did this for Michael and Yishuai IIRC).

Enrico Tassi (Oct 27 2021 at 09:15):

I'm afraid glob files are also used to do other things. @Jason Gross could you explain what?
(I do have one use case, and I think I'll try to move that piece of info in the .vo proper... but in the meanwhile...)

Jason Gross (Oct 27 2021 at 17:08):

@Théo Zimmermann if it doesn't cost anything (or more specifically costs less than it costs the devs to respond to any issues I open about, e.g., Flocq, on the coq issue tracker itself), then I'd greatly appreciate that, thanks!

Jason Gross (Oct 27 2021 at 17:32):

@Guillaume Melquiond I need .glob files to turn all relative Require statements in installed .v files into absolute ones. Here's the expanded explanation:

• When minimizing CI developments that depend on Flocq, I want to be able to create a stand-alone .v file that can be built (and further minimized and added to the test-suite) without needing to build/install any additional libraries.
• Hence I need to be able to inline .v files from Flocq into the minimal example I'm building, and the resulting file needs to build.
• Hence either I need to absolutize all Require statements, or else I need to somehow infer the command line arguments used to build this particular .v file, and then either infer the source .v file that was installed to this place or else mangle the command line arguments (in particular -R and -Q flags) so that they refer to the installed Flocq rather than the source tree. (Also, I expect down the road I'm going to run into problems with developments that use things like -set, -noinit, etc, and I might open an issue request on Coq that the command line arguments that impact the .vo file output be recorded in the .glob file somehow.)
• Since the build systems of CI developments are varied and I don't want to add special cases for all of them, I want to just route through the CI build targets that Coq uses. Furthermore, I want to reuse the artifacts from Coq's CI, rather than rebuilding the library myself. Hence I want to work assuming that all I have in hand is a pre-built, pre-installed Flocq, without needing to parse the build system, and without needing to rebuild the entire library from scratch.
• I know of no way to reconstruct the command-line arguments from the installed state, so rebuilding the .v file seems impossible under these constraints.
• Hence I need all of the .v, .vo, and .glob files to be installed, so I can absolutize all Require statements when inlining a .v file

Maxime Dénès (Oct 27 2021 at 19:00):

Théo Zimmermann said:

Yes, Jason Gross, getting an Inria external account nowadays requires getting a sponsor and the sponsor renewing the sponsorship every year. I can do that for you if you want (I already did this for Michael and Yishuai IIRC).

@Théo Zimmermann the default sponsorship period was recently changed to 3 years

Théo Zimmermann (Oct 28 2021 at 07:59):

That's good to hear.

Théo Zimmermann (Oct 30 2021 at 16:16):

@Jason Gross You've now got an external Inria account.

Théo Zimmermann (Oct 30 2021 at 16:17):

I've also renewed the end date of the sponsorship for Michael and Yishuai. In the three cases, it is 2022-12-31 since this is currently the end date of my contract with Inria. @Maxime Dénès should I transfer the sponsorship to you since you are on a permanent contract?

Enrico Tassi (Oct 31 2021 at 13:46):

If Maxime is busy I'm fine doing the sponsoring, but I need a pointer since I could not figure out where the look for this setting.

Théo Zimmermann (Oct 31 2021 at 17:03):

Documentation for this is indeed hard to find. The page to manage them is https://external-account.inria.fr and I think you need the VPN to get access.

Théo Zimmermann (Oct 31 2021 at 17:30):

Should I transfer the three accounts to you?

Jason Gross (Oct 31 2021 at 20:57):

@Théo Zimmermann Thanks!

Notification Bot (Nov 01 2021 at 15:46):

Jason Gross has marked this topic as resolved.

Maxime Dénès (Nov 03 2021 at 23:39):

@Théo Zimmermann Sure, no pb. Although I'm not completely sure how to perform such a transfer, technically. Did you see an option to do it?

Maxime Dénès (Nov 03 2021 at 23:39):

Or was the transfer already done to Enrico?

Théo Zimmermann (Nov 04 2021 at 09:33):

@Maxime Dénès Yes, there is an option to change the sponsor. I transferred them to you now.

Last updated: Jun 05 2023 at 09:01 UTC