Email Gateway (Jan 16 2026 at 16:11): Email Gateway (Jan 16 2026 at 16:11):From: Simon Wimmer <wimmersimon@gmail.com>
Dear list,
It seems that Isabelle-2025-1 always accepts sorry during isabelle
build,
regardless of whether quick_and_dirty is set. I attach a minimal example
at the end.
This behavior appears on Apple Silicon and Linux (Intel).
It was already present in RC1.
Simon
Example:
ROOT:
session Test = Main +
theories
Test
Test.thy:
theory Test
imports Main
begin
lemma False
sorry
end
Command:
isabelle build -d . -c -o quick_and_dirty=false Test
Email Gateway (Jan 16 2026 at 16:38):From: Makarius <makarius@sketis.net>
On 16/01/2026 17:11, Simon Wimmer wrote:
It seems that Isabelle-2025-1 always accepts
sorryduringisabelle build,
regardless of whetherquick_and_dirtyis set. I attach a minimal example at
the end.
Command:
isabelle build -d . -c -o quick_and_dirty=false Test
This is bad.
Note that it works properly as follows:
isabelle build -d . -c -o quick_and_dirty=false -o show_results=false Test
We have accumulated a bit too many options, variants, modes. I need to
investigate this further, to understand its intended meaning and purpose.
Makarius
Email Gateway (Jan 16 2026 at 21:19):From: Makarius <makarius@sketis.net>
On 16/01/2026 17:38, Makarius wrote:
This is bad.
For the historical record, here is the relevant changeset from 28-Aug-2025:
changeset: 83065:0a1a054d9b23
user: wenzelm
date: Thu Aug 28 15:55:07 2025 +0200
summary: clarified show_results to serve as guard for interactive mode --
avoid printing internal consts, e.g. in 'record' or 'datatype', where
Specification.definition is used as convenience for class instantiation (see
also 889d5cdc034b, 951abf9db857, ecf80e37ed1a);
This treats all Isar commands in "isabelle build" as interactive and thus
always allows 'sorry'.
I need to think about Isabelle2025-2 (January 2026) where this is partially
reverted.
Makarius
Email Gateway (Jan 17 2026 at 19:59):From: Makarius <makarius@sketis.net>
On 16/01/2026 22:19, Makarius wrote:
On 16/01/2026 17:38, Makarius wrote:
This is bad.
I need to think about Isabelle2025-2 (January 2026) where this is partially
reverted.
My current plan is to apply carefully chosen changes on top of Isabelle2025-1,
and publish that as Isabelle2025-2 at the start of next week. There won't be
any incompatibilities. AFP may remain at afp-2025-1 and does not need to be
relaunched.
We've had such a slightly awkward situation before, with Isabelle2023-1
(November 2013) vs. Isabelle2023-1 (December 2013). See also
https://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/NEWS ---
but with fewer changes this time.
Makarius
Last updated: Jan 31 2026 at 12:53 UTC