Stream: Coq devs & plugin devs

Topic: Mtac2 broken in Coq's CI

Emilio Jesús Gallego Arias (Sep 07 2021 at 16:56):

@Janno mtac2 seems broken in Coq's CI, likely our fault? See https://github.com/coq/coq/pull/14851/checks?check_run_id=3534068725 for example

Gaëtan Gilbert (Sep 07 2021 at 17:08):

looks like it's from https://github.com/coq/coq/pull/14808
CI ran with missing overlay for a previous PR so we didn't see it
I guess we should revert then investigate

Janno (Sep 07 2021 at 17:24):

Let me see where the failure is. I might be able to say what is going on.

Janno (Sep 07 2021 at 17:33):

I think it is failing in the very first invocation of the Mtac2 interpreter. I'll have to turn on debugging options for more info but first I need to build coq/master.

Janno (Sep 07 2021 at 17:46):

It's taking longer than I anticipated and I need go AFK for a while. I'll continue later today.

Janno (Sep 07 2021 at 18:33):

Mtac2 is using

match .. with
| FFlex (ConstKey (hc, _) as k) ->
            let redflags = (CClosure.RedFlags.fCONST hc) in
            let env = info_env infos in
            let flags = RedFlags.red_transparent (CClosure.RedFlags.mkflags [redflags]) in
            let o = CClosure.unfold_reference env flags tab k in
            match o with ...

to unfold references. o seems to be None for (almost?) everything on coq/master.

Janno (Sep 07 2021 at 18:48):

Okay, the problem is that we were re-using tab from an earlier call to reduction.

Gaëtan Gilbert (Sep 07 2021 at 18:58):

I guess you should be reducing with only the primitives set opaque in the transparent state, then you don't have to restart reduction
or even with the "everything is transparent" transparent state since AFAIK the primitives are Qed

Janno (Sep 07 2021 at 19:03):

It's not quite that easy. We record constants that are being unfolded in order to generate backtraces for exceptions.

Janno (Sep 07 2021 at 19:03):

But the fix here is reasonably simple. Just create new tabs everywhere.

Gaëtan Gilbert (Sep 07 2021 at 19:06):

creating a tab for every unfold_reference is a waste of time, maybe we should expose the tabless version

Janno (Sep 07 2021 at 19:10):

That is true. I was actually hoping to make use of caching but Mtac2 can extend the local environment and I am not sure how that will interact with the cache.

Janno (Sep 07 2021 at 19:14):

I have the naive fix but github doesn't want to let me push my changes.

Janno (Sep 07 2021 at 19:53):

https://github.com/Mtac2/Mtac2/pull/341 is merged. This should fix Coq CI.

Last updated: Apr 20 2024 at 01:41 UTC