Skip to content
This repository has been archived by the owner on Aug 20, 2021. It is now read-only.

libexec/klab-prove-all: unaccept BADGAS specs #411

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

asymmetric
Copy link
Contributor

Remove them from the accept directory, so that the whole process is restarted.

This is not ideal (since the proof had already been accepted), but the
alternative risks giving false positives if one doesn't inspect the
build log.

Remove them from the accept directory, so that the whole process is restarted.

This is not ideal (since the proof had already been accepted), but the
alternative risks giving false positives if one doesn't inspect the
build log.
@asymmetric asymmetric requested a review from a team April 22, 2020 12:04
@d-xo
Copy link
Contributor

d-xo commented Apr 22, 2020

Do we know why get-gas was unable to extract a gas expression from these BADGAS proofs? i.e was the problem in the proof or in get-gas itself?

@asymmetric
Copy link
Contributor Author

asymmetric commented Apr 22, 2020

Nope, I don't know, but I would say that's out of scope for this PR, isn't it?

If you look at get-gas and get-x, there are several reasons why they could exit with an error, some of them unrecoverable (e.g. files missing, maybe someone has removed them manually?), and this PR tries to recover from that state without manual intervention.

@asymmetric
Copy link
Contributor Author

But I do think this is not the best solution, since the proofs itself has been accepted, so I'm open to better suggestions.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants