search

snu-sf / paco

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

gcofix failing in 4.1 #41

Closed YaZko closed 3 years ago

YaZko commented 3 years ago

Hello,

The latest release of gpaco broke a script in Vellvm. It appears to be a side effect to the "fix" in gcofix from issue #37, but I haven't looked close enough to figure out what is happening exactly.

The proof failing is the following (it is in the Vellvm repo, but is a purely itree-based thing, it only depends on Utils/NoEvents.v ): https://github.com/vellvm/vellvm/blob/master/src/coq/Utils/Commutation.v#L36

We get Error: Proof is not complete. when calling ecofix CIH where it used to work on the previous version. Unfolding the definition of ecofix, it happens when calling paco_post2 CIH with gL..

Am I missing a reason for which it indeed should fail, or did the fix from #37 introduce another bug by side effect?

Best, Yannick

minkiminki commented 3 years ago

I made a hotfix (5a38bcf). Could you test that this patch works? @YaZko

YaZko commented 3 years ago

Hello @minkiminki ,

I just tried the patch, it indeed solves the problem perfectly! Thanks a lot.

minkiminki commented 3 years ago

Good! I released 4.1.1 and wait for it to be merged in opam-coq-archive.