I am in the process of fixing fiat-crypto-legacy for Coq's CI, and it seems that in the interim while it was broken (in the past four days since https://github.com/coq/coq/pull/18014 was merged without making an overlay for f-c-l), it seems that there's been a new regression introduced in master?
File "./src/Experiments/SimplyTypedArithmetic.v", line 7059, characters 4-350:
Error: Anomaly "Not an unfoldable reference."
Please report at http://coq.inria.fr/bugs/.
Should f-c-l be taken off allowed-failure?
And what is up with those line numbers? This is https://github.com/mit-plv/fiat-crypto/blob/77a2f7db22cfe88d92c6331e20fce22cd3b9bc1d/src/Experiments/SimplyTypedArithmetic.v#L7059
cbv [BoundsPipeline Let_In] in *;
repeat match goal with
| [ H : match ?x with _ => _ end = Success _ |- _ ]
=> destruct x eqn:?; cbv beta iota in H; [ | destruct_head'_prod; congruence ];
let H' := fresh in
inversion H as [H']; clear H; rename H' into H
end.
(Target is some-early util
)
line 7059, characters 4-350:
The location span is excessively large specifically because it is an anomaly? We would need to check.
Last updated: Oct 13 2024 at 01:02 UTC