Stream: Coq devs & plugin devs

Topic: Menhir


view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:24):

According to https://github.com/coq/coq/blob/master/dev/ci/ci-basic-overlay.sh Menhir's target branch for overlays is 20220210 but it looks quite behind a "master" branch. Is the target branch still 20220210?

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:25):

basic-overlay is the source of truth

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:28):

But here I get: "The target branch 20220210 does not exist."

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:29):

There is a "release-branch-20220210" on which I can merge-request.

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:29):

it's a tag not a branch

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:31):

So which is the branch I should target?

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:31):

master I guess

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:32):

but then what is 20220210 in https://github.com/coq/coq/blob/master/dev/ci/ci-basic-overlay.sh?

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:33):

the tag we use currently
you can change it

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:33):

(Trying to grasp an important piece of truth from the source)

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:34):

So the source of truth needs to be updated?

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:34):

if you want to

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:35):

a file can be the source of truth, but you have the power

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:36):

ok, and for metacoq?

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:36):

we're on a branch for metacoq so just submit the overlays

view this post on Zulip Pierre Rousselin (Oct 20 2023 at 13:37):

I'm asking because metacoq's "main" looks broken.

view this post on Zulip Gaëtan Gilbert (Oct 20 2023 at 13:40):

should be fixed since https://github.com/MetaCoq/metacoq/pull/995
or is it another error?

view this post on Zulip Gaëtan Gilbert (Dec 12 2023 at 20:32):

funny error https://gitlab.inria.fr/coq/coq/-/jobs/3691631
the http job ran the day after the menhir job so go a different date

view this post on Zulip Pierre Rousselin (Dec 12 2023 at 20:51):

That's so funny :lol:. Morale: you can't move the Menhir.
I'll try to think about it tomorrow, but my brain is probably hopelessly broken.

view this post on Zulip Gaëtan Gilbert (Dec 14 2023 at 11:40):

https://github.com/coq/coq/pull/18408


Last updated: Oct 13 2024 at 01:02 UTC