Stream: Coq devs & plugin devs

Topic: Backtraces in CoqIDE


view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 16:11):

I am getting the perennial anomaly "Anomaly: Occurrence of Find string not in table", which is not something new. But now it also prints an OCaml backtrace.

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 16:11):

since when do we do this?

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 16:12):

this might be very bad for performance

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 16:39):

we don't
at least Check Prop Prop. prints no backtrace in my coqide

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 16:42):

I am talking about CoqIDE errors

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 16:43):

It was introduced by f3f165b, look for Printexc.record_backtrace in coqide.ml


Last updated: Feb 05 2023 at 21:03 UTC