Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] [ISSUE] PIDE reports wrong error line and mess...

Email Gateway (Apr 02 2026 at 17:50):

From: Bartosz Glowacki <cl-isabelle-users@lists.cam.ac.uk>

Dear Isabelle developers,

I found a difference between isabelle build and the PIDE server (use_theories) outputs when by sorry appears as the final tactic before qed in a calc-terminated proof block:

• isabelle build (correct): "Bad context for command 'qed'" at the qed line
• PIDE server: "Outer syntax error: keyword '(' expected, but end-of-input was found" one line earlier, at the by sorry line

Minimal reproducer:

theory BugDemo
imports "HOL-Combinatorics.Multiset_Permutations"
begin

text \\<open>
map_index_self: mapping the index function over a distinct list gives [0..<length xs].
\\<close>

lemma map_index_self:
assumes "distinct xs"
shows "map (index xs) xs = [0..<length xs]"
proof -
have "xs = map (\\<lambda>i. xs ! i) [0..<length xs]"
by (simp add: map_nth)
also have "map (index xs) \\<dots> = map id [0..<length xs]"
by (intro map_cong) simp_all
finally show ?thesis
by sorry     (* PIDE reports error here - wrong *)
Qed         (* isabelle build reports error here - correct *)

end

The real error is semantic — qed finds no open goal context — and isabelle build diagnoses it correctly. PIDE reports a spurious syntax error at the wrong line instead. While this is not a serious bug, it may be misleading for the end-user to receive the syntax error instead of the real issue they should focus on.

This was found using a differential fuzzing framework that compares error output between isabelle build and the PIDE server on mutated AFP theories. The mutation by simp -> by sorry triggered this mismatch in 10/10 independent runs. I am happy to share the framework and logs.

This was found as part of my dissertation work on differential testing of the Isabelle platform.

Kindest regards,
Bartosz Glowacki
King's College London

Email Gateway (Apr 07 2026 at 12:16):

From: Fabian Huch <huch@in.tum.de>

'by sorry' is syntactically ill-formed, and there is no surprise that an
interactive session reports errors differently from a non-interactive
build because

a) a headless build does not need to keep track of as much markup
information and

b) an interactive session tries to recover from problems (to some
degree), such that one can continue editing in the presence of errors.

Fabian

On 4/2/26 19:05, Bartosz Glowacki (via cl-isabelle-users Mailing List)
wrote:

Dear Isabelle developers,

I found a difference between isabelle build and the PIDE server
(use_theories) outputs when by sorry appears as the final tactic
before qed in a calc-terminated proof block:

• isabelle build (correct): "Bad context for command 'qed'" at the qed
  line
• PIDE server: "Outer syntax error: keyword '(' expected, but
  end-of-input was found" one line earlier, at the by sorry line

Minimal reproducer:

theory BugDemo
  imports "HOL-Combinatorics.Multiset_Permutations"
begin

text \\<open>
  map_index_self: mapping the index function over a distinct list
gives [0..<length xs].
\\<close>

lemma map_index_self:
  assumes "distinct xs"
  shows   "map (index xs) xs = [0..<length xs]"
proof -
  have "xs = map (\\<lambda>i. xs ! i) [0..<length xs]"
    by (simp add: map_nth)
  also have "map (index xs) \\<dots> = map id [0..<length xs]"
    by (intro map_cong) simp_all
  finally show ?thesis
    by sorry     (* PIDE reports error here - wrong *)
Qed         (* isabelle build reports error here - correct *)

end

The real error is semantic — qed finds no open goal context — and
isabelle build diagnoses it correctly. PIDE reports a spurious syntax
error at the wrong line instead. While this is not a serious bug, it
may be misleading for the end-user to receive the syntax error instead
of the real issue they should focus on.

This was found using a differential fuzzing framework that compares
error output between isabelle build and the PIDE server on mutated AFP
theories. The mutation by simp -> by sorry triggered this mismatch
in 10/10 independent runs. I am happy to share the framework and logs.

This was found as part of my dissertation work on differential testing
of the Isabelle platform.

Kindest regards,
Bartosz Glowacki
King's College London

Last updated: Apr 12 2026 at 02:50 UTC