Cobalt (Jul 06 2025 at 19:10): Cobalt (Jul 06 2025 at 19:10):Hi, I may have found a bug in the Isabelle server (for Isabelle 2025), when sending a use_theories command with pretty_margin: 0 the server tries to start the check but the task eventually fails with the message:
? {"kind":"error","message":"java.lang.ArithmeticException: / by zero","task":"643b0346-c974-448e-8f9c-c5505ed7c777"}
This seems like a violation of the server message spec. It also appears like there should probably be some kind of input validation before the zero is passed to the arithmetic operation.
Last updated: Jul 12 2025 at 12:41 UTC