I thought the toplevel was supposed to turn uncaught exceptions into anomalies rather than crashing? (https://github.com/coq/coq/issues/16462)
Sure. But what if it is the code that turns an uncaught exception into an anomaly that crashes?
Maybe that code can itself catch most exceptions that are raised and print less informative error messages? (I think I've seen this when an exception is raised in printing?)
Last updated: Jun 05 2023 at 10:01 UTC