-
Notifications
You must be signed in to change notification settings - Fork 11
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Formalise Propositions 3.6 and 3.7 from RS17 paper #30
Conversation
I can reproduce the issue, I will trace it and report later. Thanks for letting us know! |
Initially, I thought there is a bug and an infinite loop somewhere. But it turns out, there's just a huge inefficiency (which can also be considered a bug, I guess). In particular, when checking I have fixed the issue locally, and now I see another issue in I will fix this second issue as well soon, make a release, and then this PR will be good to merge! Thanks for exposing weaknesses in the implementation :) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is working now, with rzk-0.5.7! If you don't plan on pushing more changes here, I am happy to merge :)
Great! Thanks for the quick response and fixes! Ready to merge for me :) |
Done. |
Closes #3.
Prop 3.6 works fine, but for prop 3.7 the check of Δ³-is-retract-Δ²×Δ¹-section does not terminate in my laptop. I'm not sure what's happening, but proof seems ok.