Stream: Coq devs & plugin devs

Topic: Standalone deps in CI


view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:38):

Is there a reason why we still have some standalone devs without a proper job in the CI? It's annoying for overlays, because they're hardcoded in the downstream script.

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:39):

I am thinking for instance of verdi_raft, which embeds struct_tact, inf_seq_ext, cheerios and verdi.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2022 at 09:42):

Lack of manpower @Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:42):

ok, so no real reason

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:42):

not sure what the point of splitting the verdi script would be tbh

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2022 at 09:42):

there is a lot of improvements we could do w.r.t. overlays, i have a long list

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:43):

when I have a bit of time I will write a patch then

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2022 at 09:43):

just didn't found an intern or engineer to help with them

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:43):

@Gaëtan Gilbert the dev tool scripts do not support internal deps

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2022 at 09:43):

Indeed I think that overlays should work for devs as in the fast CI mode we discussed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2022 at 09:43):

and have much better dev scripts

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:43):

what scripts?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2022 at 09:43):

./create-overlays

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:44):

^ this

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:44):

right I guess you still need to comment out the make line

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:44):

also it's annoying from the github UI in case of failure because it's misleading

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:44):

my understanding is that we did that when dep management was a hell in gitlab ci:

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:45):

with all the pipeline depth and whatnot

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:45):

now that gitlab provides a straightforward graph dep model it should be free

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:45):

each job has about 5min of startup + end time so we don't want to split too much

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:45):

yet another argument to reduce the size of vo files (and hence docker images)

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:46):

I can live with this but I think it's quite a wart

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:46):

I think first we should split the docker image into one image for base and one for edge

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:46):

vo files aren't in the docker image btw

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:47):

can't we split the scripts but run several of them in the gitlab ci yml file in a single target?

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:48):

this would solve most of my problems

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:51):

sure
with the current way it's written when there are missing deps they just get run too so it's easy

view this post on Zulip Karl Palmskog (Jun 28 2022 at 10:38):

as de factor maintainer of verdi_raft and friends, please let me know if we can do anything on repo side to help devs out.


Last updated: Feb 05 2023 at 21:03 UTC