search

snu-sf / paco

A Coq library for parametric coinduction
https://github.com/snu-sf/paco
Other
43 stars 10 forks source link

coq-itree broken #50

Closed Lysxia closed 1 month ago

Lysxia commented 1 month ago

Some proofs in itree were broken by the two latest commits on the master branch of paco. This was noticed after Coq CI started failing, cf coq/coq#19641.

It seems that pclearbot no longer clears upaco2 _ bot2 when it's under a forall. Is this intentional? Should this be fixed in paco or in itree?

Previously this worked:

(* initial assumption *)
REL : forall v : u0, id (upaco2 (eqit_ (flip RR) b2 b1 id) bot2) (k1 v) (k2 v)

(* pclearbot *)

(* updated assumption *)
REL : forall v : u0, paco2 (eqit_ (flip RR) b2 b1 id) bot2 (k1 v) (k2 v)
Lysxia commented 1 month ago

ping @gilhur

gilhur commented 1 month ago

@Lysxia, I am sorry about the trouble. I just fixed it and pushed the update. Thanks!

SkySkimmer commented 1 month ago

Still seems to fail although with a different error now https://gitlab.inria.fr/coq/coq/-/jobs/4810118

File "./extra/Dijkstra/ITreeDijkstra.v", line 263, characters 37-70:
Error: Tactic failure: Incorrect number of goals (expected 1 tactic).
gilhur commented 1 month ago

I will take a look and hopefully have it fixed today.

gilhur commented 1 month ago

@Lysxia and @SkySkimmer, I released Paco v4.2.1 and also made a pull request for ITree that removes workaround code due to a bug in pclearbot, which is no longer needed.

Lysxia commented 1 month ago

Thanks Gil. I've merged your PR so the Coq CI build should be fixed now. I also submitted a PR to opam for the new version of paco https://github.com/coq/opam/pull/3178

proux01 commented 1 month ago

@gilhur Note that paco should have a CI testing all reverse dependencies tested in Coq CI (which includes itree) and nothing should be pushed to paco until that CI passes. Otherwise, this kind of mistakes is bound to happen again in the future.

gilhur commented 1 month ago

@Lysxia Thanks! @proux01 Yes, you are right :) I will have a CI testing set up for our projects.

proux01 commented 1 month ago

Thanks