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

Better error messages on uncaught exceptions #264

Open
JasonGross opened this issue Jan 23, 2023 · 4 comments
Open

Better error messages on uncaught exceptions #264

JasonGross opened this issue Jan 23, 2023 · 4 comments
Labels
enhancement New feature or request

Comments

@JasonGross
Copy link
Member

I see things like

Error: Unhandled exception: (Invalid_argument Str.matched_group)

and similar messages for stack overflow (on logentries), and it would be nice to get a backtrace instead, so I can Can this be done?

@ticket-tagger ticket-tagger bot added the enhancement New feature or request label Jan 23, 2023
@Zimmi48
Copy link
Member

Zimmi48 commented Feb 8, 2023

This message is generated here:

bot/src/bot.ml

Lines 506 to 511 in 3deea7d

let () =
Lwt.async_exception_hook :=
fun exn ->
(fun () ->
Lwt_io.printlf "Error: Unhandled exception: %s" (Exn.to_string exn) )
|> Lwt.async

Since we are not in a catch clause, I'm not sure that a backtrace would still be available. We could experiment with inserting Printexc.print_backtrace (and turning exception backtrace recording on, with Printexc.record_backtrace).

@Alizter
Copy link
Contributor

Alizter commented Feb 8, 2023

We should record backtraces since we are not performance critical anyway. Debugging coq bot is hard enough on its own, we should help any way we can.

@Zimmi48
Copy link
Member

Zimmi48 commented Apr 16, 2023

Since we do not use exception-based workflows in the bot codebase (except maybe catching a few Not_found here and there coming from external libraries), would this have any actual performance impact anyway?

@Alizter
Copy link
Contributor

Alizter commented Apr 17, 2023

@Zimmi48 Not for coqbot.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

3 participants