Stream: Coq devs & plugin devs

Topic: anomaly guessing game

view this post on Zulip Jason Gross (Nov 19 2022 at 04:31):

I managed to get

File "/tmp/tmpmop1bru0/Crypto/Assembly/Symbolic.v", line 543, characters 0-9:
Error: Anomaly "in Lemmas.save_lemma_admitted: more than one statement."
Please report at http://coq.inria.fr/bugs/.

while minimizing https://github.com/coq/coq/issues/16834 here. Any guesses about the cause? (I can try to track it down on my own later, but it'll be a bit annoying, and if anyone can guess a way to trigger it, that'd save me some work.)

view this post on Zulip Jason Gross (Nov 19 2022 at 06:13):

Reported at https://github.com/coq/coq/issues/16856, not yet minimized

view this post on Zulip Jason Gross (Nov 19 2022 at 19:16):

Answer: Admitted doesn't work with Derive

Last updated: Dec 07 2023 at 06:38 UTC