Stream: Coq devs & plugin devs

Topic: ✔ gitlab.inria.fr account?


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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 27 2021 at 00:50):

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Oct 28 2021 at 07:59):

That's good to hear.

view this post on Zulip Théo Zimmermann (Oct 30 2021 at 16:16):

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

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

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

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

view this post on Zulip Théo Zimmermann (Oct 31 2021 at 17:30):

Should I transfer the three accounts to you?

view this post on Zulip Jason Gross (Oct 31 2021 at 20:57):

@Théo Zimmermann Thanks!

view this post on Zulip Notification Bot (Nov 01 2021 at 15:46):

Jason Gross has marked this topic as resolved.

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

view this post on Zulip Maxime Dénès (Nov 03 2021 at 23:39):

Or was the transfer already done to Enrico?

view this post on Zulip 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: Dec 05 2023 at 04:01 UTC