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
Yes you can, tho it is mostly useless [but may work for issues]
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
if the issue due to Flocq installation, then other projects that use the same build systems (remake) such as Coquelicot are probably also affected
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.
Glob files are required if users want to build docs properly aren't they?
But indeed Coq packages should be consistent, if coq_makefile / dune do install glob files, flocq should too
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.
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).
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...)
@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!
@Guillaume Melquiond I need .glob files to turn all relative Require
statements in installed .v files into absolute ones. Here's the expanded explanation:
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.)Require
statements when inlining a .v
fileThé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
That's good to hear.
@Jason Gross You've now got an external Inria account.
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?
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.
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.
Should I transfer the three accounts to you?
@Théo Zimmermann Thanks!
Jason Gross has marked this topic as resolved.
@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?
Or was the transfer already done to Enrico?
@Maxime Dénès Yes, there is an option to change the sponsor. I transferred them to you now.
Last updated: Dec 05 2023 at 04:01 UTC