Bad interaction of async proofs and HB

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes

MIT License

95 stars 20 forks source link

Bad interaction of async proofs and HB #434

Closed eponier closed 1 month ago

eponier commented 2 months ago

I don't know if it is an error coming from HB or Coq, but the easy way to reproduce it is with HB. Feel free to transfer the bug report to coq if this is more appropriate.

The bug is really easy to reproduce with CoqIDE. Just open the following file and go to the end. The error Anomaly "Uncaught exception Not_found" is produced. I tried coq 8.19 and 8.18, with HB 1.17.

From HB Require Import structures.

Goal True.
Proof. reflexivity.
Qed.

eponier commented 2 months ago

Compiling with coqc -async-proofs on also triggers the anomaly.

eponier commented 1 month ago

Never mind, this is an occurrence of https://github.com/LPCIC/coq-elpi/issues/543, closing.