Skip to content
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

--stop doesn't really work #212

Open
tsani opened this issue Apr 7, 2020 · 1 comment
Open

--stop doesn't really work #212

tsani opened this issue Apr 7, 2020 · 1 comment
Assignees
Labels
A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour B | refactor changing the implementation of existing features P | low low priority issue

Comments

@tsani
Copy link
Contributor

tsani commented Apr 7, 2020

The --stop option was added to Harpoon to assist in debugging command transcripts, to make Harpoon exit on the first command that produces an exception. The problem is that errors that are generated by Harpoon rather than by Beluga do not generate exceptions. They just print an error message.

This is tagged refactor because one should rethink the way exceptions are handled in Harpoon. Perhaps a simple approach is to make all errors proper OCaml exceptions. Since these exceptions have no need to be caught and analyzed, we can just wrap a function of type formatter -> unit -> unit that prints the error message.

@tsani tsani added B | bug unexpected or incorrect behaviour B | refactor changing the implementation of existing features A | harpoon affecting the Harpoon interactive prover labels Apr 7, 2020
@tsani tsani self-assigned this Apr 7, 2020
@tsani tsani added the P | low low priority issue label Apr 14, 2020
@tsani
Copy link
Contributor Author

tsani commented Apr 14, 2020

Given that --stop is largely a debugging tool, I've made this issue low-priority for now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour B | refactor changing the implementation of existing features P | low low priority issue
Projects
None yet
Development

No branches or pull requests

1 participant