DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
204 stars 51 forks source link

Error installing coq-itree 5.1.1 with coq 8.18.0 #259

Closed RalfJung closed 1 year ago

RalfJung commented 1 year ago

In updating all my opam switches to Coq 8.18.0, I encountered what I think to be an incompatibility of coq-itree with the latest coq version. The opam file of coq-itree does not declare a conflict with Coq 8.18, but the build fails:

- File "./theories/Events/FailFacts.v", line 106, characters 6-16:
- Error:
- setoid rewrite failed: Unable to satisfy the following constraints:
- UNDEFINED EVARS:
-  ?X283==[E A B x y H x0 y0 H0 a0 |-
-           Relation_Definitions.relation (failT (itree E) B)]
-           (internal placeholder) {?r}
-  ?X284==[E A B x y H x0 y0 H0 a0 |-
-           subrelation (pointwise_relation A eq1) (pointwise_relation A ?r)]
-           (internal placeholder) {?s}
-  ?X286==[E A B x y H x0 y0 H0 a0 |-
-           Relation_Definitions.relation (itree E (option B))]
-           (internal placeholder) {?r0}
-  ?X287==[E A B x y H x0 y0 H0 a0 (do_subrelation:=do_subrelation) |-
-           Proper (?r ==> ?r0 ==> flip impl) (eutt (option_rel eq))]
-           (internal placeholder) {?p}
-  ?X288==[E A B x y H x0 y0 H0 a0 |- ProperProxy ?r0 (y0 a0)]
-           (internal placeholder) {?p0}
- TYPECLASSES:?X283 ?X284 ?X286 ?X287 ?X288
- SHELF:||
- FUTURE GOALS STACK:?X288 ?X287 ?X286 ?X284 ?X283||

Would be nice to get an opam release of this package that is compatible with the latest Coq. :)

RalfJung commented 1 year ago

I found this commit which I presume fixes the problem: https://github.com/DeepSpec/InteractionTrees/commit/eede8c539985e358e7149ab77b5c058def37571d So looks like all that's missing is a new opam package that includes the fix?

Lysxia commented 1 year ago

I've just released 5.1.2 with that fix.

RalfJung commented 1 year ago

Thanks. :)