The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

Here is a first analysis of the failures (up to math-classes). All seems legitimate and have a solution. For two of them (engine bench and iris), the solution is at the Coq level.

Bedrock2:

Notation "x {{ u }}" ... (at level 8).
Check x{{u}}.(field). (* now fails because "t.(...)" expects t at level 1 *)

Reasonable solution: move "x {{ u }}" at level 1?

Category theory:

Notation "⟨πD,πC⟩" := comma_proj (at level 100).
Check ⟨πD,πC⟩ ≈ ⟨πD,πC⟩ ◯ φ. (* ◯ at level 40 *)

Reasonable solution: move ⟨πD,πC⟩ at level 0

CoLoR:

Notation "x !" := (clos_trans x) (at level 35).
Check R! x y.

Reasonable solution: move "x !" at level < 10 (e.g. 1, since its argument seems to be a variable in practice).

Cross-crypto:

Notation "'ret' v" := (MRet _ v) (at level 75).
Check x = ret v.

Tentative solution: move "'ret' v" at level 69 (as it is sometimes applied to an application, or to "a::l")

Engine bench:

Ltac f := do 1000 let v := open_constr:(_ : True) in idtac. (* "let" at level 5 but "do" expects level 3)

Do like for binder_constr, i.e. move binder_tactic at level 1 (where application lives), and this would even simplify repeated rules like for tac + tac.

HoTT:

Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3).
Check f^-1%equiv. (* % expects its argument at level 1 *)

Reasonable solution: move "f ^-1" at level 1.

Iris:

split; [|done] => _. (* knowing that "=>" expects its argument at level 1, but ";" is at level 4 *)

Solution: decide if "=>" really wants to be at level 1.

itree:

Check pure (m := m) (a := a + (b + c))%type. (* %type does not apply to a (a:=b) as might be expected *)

Solution: move %type inside the parenthesis

Math classes:

Notation "∥ L ∥" := (norm L) (at level 50).
Check (abs a) * ∥v∥. (* "*" expects level 40 but ∥v∥ is at level 50 *)

Solution: move "∥ L ∥" at level 0.

At the Coq call (2023-10-24), the question of adding a warning so as to allow users to do the changes themselves was raised, and this is certainly that can be tried (i.e., in case of parsing error, we try the recovery mode even though it is deactivated, and if it succeeds, we warn that it has been used).

The investigations above also suggest the following:

• For closed notations (such as ∥ L ∥ or ⟨πD,πC⟩), put them automatically at level 0 and warns (or warn that it could be better put at level 0).
• For postfix notations (such as x {{ u }}, R ! or f ^-1), warn that it is in general clearer to put them at level 1.

What is the status of Fiat Crypto Legacy?

What is the status of Fiat Crypto Legacy?

The first error look similar to engine bench (ltac level issue, with repeat).

@coqbot merge now

I had to temporarily disactivate kami and sf that are infriging the CI contract:

@samuelgruetter, @andres-erbsen, @bcpierce00, @liyishuai I'll happily merge any PR reverting the corresponding commit once things are fixed downstream.

I had to temporarily disactivate kami and sf that are infriging the CI contract:

rocq/dev/ci/README-users.md

Lines 21 to 22 in ed67c98

	- You react in a timely manner to adapt to the few requested changes
	required by Rocq developers or to integrate their patches (in a 7 days timeframe,

@samuelgruetter, @andres-erbsen, @bcpierce00, @liyishuai I'll happily merge any PR reverting the corresponding commit once things are fixed downstream.

You say disable Kami, but AFAIU the Kami overlay was merged, it was just incorrectly propagated to its reverse deps. There seems to have been some action to propagate it after your request (mit-plv/fiat-crypto#2112), so what was the final status of the issue when this PR got merged? There isn't much trace to get this info here or elsewhere.

Indeed the update was propagated before this PR as described by Andres in

That's a stale PR. fiat-crypto is not auto-updating because the build is broken.

Manual update at mit-plv/fiat-crypto#2112

So please revert the disabling of Fiat Crypto and its dependencies.

Indeed the update was propagated before this PR as described by Andres in

This is obviously wrong, kami was still red in CI at the time of merging. I wouldn't have had to disactivate it otherwise.
According to this PR, the last overlay still wasn't propagated through all the git submodules at the time of merging, 12 days after it's opening (in fact, Stdlib CI indicates that this propagation finally happened only ten more days later).
So apparently I was right to be tired of waiting, and having to rebase this PR several times, just because of that git submodule propagation taking weeks.
We have a CI policy, please adhere to it and don't waste developer's time!

I think what happened here is that there were two overlays to kami with identical commit summaries, and the second one missed the manual bump in fiat-crypto. I don't think it's worth our time debating what the letter of the CI policy says about this case, and specifically for this PR I am quite happy it is finally merged one way or another. At the same time, if you had contacted us instead of waiting, we would have happily made and merged a fiat-crypto overlay to the desired effect; at least i was unaware that another one was needed.

More generally, in situations like this where multiple things are failing for multiple reasons, I think communicating more earlier about what each of us sees is going on can help a lot. I do believe everyone is trying to do a good thing here, and trying to clear up ambiguity about how things are is more likely to be successful than reiterating how things should be.

In that spirit, I would like to reiterate that the automatic submodule bumper in fiat-crypto is a conservative best-effort measure. If it doesn't work in 24h, please contact us and ask for an overlay. If it doesn't work, and there isn't an underlying cause like fiat-crypto being broken by an earlier rocq change, we will treat this as a bug in the autobumper. But having triggered the autobumper isn't necessarily enough to get an overlay created and merged to fiat-crypto.

Details: The rocq-pr rebase right before disabling kami ran ci and at least according to gitlab logs it did include a kami overlay and the merge commit i linked to earlier. It also still failed, i think because it was missing the second overlay. And then after early-july holiday season and rocq fixing haskell extraction, we got the autobumper unstuck again, i presume catching up to the second overlay without anyone noticing.