Stream: Coq devs & plugin devs

Topic: fiat-crypto-legacy


view this post on Zulip Jason Gross (Nov 01 2023 at 03:05):

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?

view this post on Zulip Jason Gross (Nov 01 2023 at 03:09):

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)

view this post on Zulip Hugo Herbelin (Nov 05 2023 at 14:22):

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