[ci] VST broken on master.

[ejgallego]

It seems CI is broken in master, but it build OK in 8.11, so this seems on our side.

PR #12254 seems like a candidate for introducing this breakage, @ppedrot @herbelin any idea?

Link to error: https://gitlab.com/coq/coq/-/jobs/548092462#L8481

[ppedrot]

This is weird, CI was green on #12254. I'll try to look into that.

[ppedrot]

Maybe it's #12146 instead, or some lia improvement. There is a line containing a subst that succeeds in master, and fails on a trivial example before. Here is a minimal diff that makes it compile.

--- a/veric/mapsto_memory_block.v
+++ b/veric/mapsto_memory_block.v
@@ -1375,7 +1375,7 @@ Proof.
   induction N; intros; trivial. remember (size_chunk Mptr) as sz.
   replace (Z.of_nat (S N) * sz)%Z with (sz + Z.of_nat N * sz)%Z by lia.
   specialize (size_chunk_pos Mptr); intros. specialize (Z_of_nat_ge_O N); intros.
-  eapply derives_trans. apply mapsto_zeros_split; subst; try lia. apply Z.mul_nonneg_nonneg; lia.
+  eapply derives_trans. apply mapsto_zeros_split; subst; try lia.
   apply andp_right.
   { clear IHN. intros m [m1 [m2 [J [[M1 _] [[M2a M2b] _]]]]]; simpl in *.
     split; try lia. rewrite Ptrofs.add_unsigned in M2b, M2a.

I'll try to submit a backwards compatible patch.

[ppedrot]

See PrincetonUniversity/VST#417.

[ejgallego]

Thanks a lot for the research @ppedrot , indeed it seems that the problem is not due to some of our commits, but from the migration to lia upstream, which introduced a change not compatible with master. Confirmed by a bisect on my side.

So yeah, that's hard to check from our side, ideally we can uniformize contributions CI enough so they all test master too.