search

coq / bot

A (Coq Development Team) bot written in OCaml
MIT License
23 stars 17 forks source link

Better error messages on uncaught exceptions #264

Open JasonGross opened 1 year ago

JasonGross commented 1 year ago

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?

Zimmi48 commented 1 year ago

This message is generated here: https://github.com/coq/bot/blob/3deea7d3c044371cf5df92ae70a51ec4339071f8/src/bot.ml#L506-L511 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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

@Zimmi48 Not for coqbot.