@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
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
Let me see where the failure is. I might be able to say what is going on.
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.
It's taking longer than I anticipated and I need go AFK for a while. I'll continue later today.
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.
Okay, the problem is that we were re-using tab
from an earlier call to reduction.
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
It's not quite that easy. We record constants that are being unfolded in order to generate backtraces for exceptions.
But the fix here is reasonably simple. Just create new tab
s everywhere.
creating a tab for every unfold_reference is a waste of time, maybe we should expose the tabless version
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.
I have the naive fix but github doesn't want to let me push my changes.
https://github.com/Mtac2/Mtac2/pull/341 is merged. This should fix Coq CI.
Last updated: Oct 13 2024 at 01:02 UTC