Open jaccokrijnen opened 9 months ago
I've disabled QuickChick for now. Problem:
File "./src/PlutusIR/Analysis/UniqueBinders/DecOpt.v", line 26, characters 0-35:
Error:
Anomaly
"Uncaught exception Failure("No Checkers or Producers for relation: appears_bound_in_tm")."
Please report at http://coq.inria.fr/bugs/.
branch
wip/coq-8.18
, using opam switchcoq.8.18
.[x] Forward port Bart's QuickChick fix. Opened PR https://github.com/QuickChick/QuickChick/pull/345
[x] Forward port custom QuickChick patch for extraction. This is in branch https://github.com/Xiving/QuickChick/tree/8.18/fix-mutual/no-extraction
[ ]
QuickChick
andequations
are incompatible: both define aDerive
vernac command. This is a problem with Coq, there is a patch in the making on the Coq sideDerive
vernac (see https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Anomaly.3A.20bad.20vernac.20extend/near/403566924)[x] Do fixes in proofs (ltac seems to have a new way of automatic naming)
[ ] Update nix setup in plutus for extraction