Email Gateway (Jul 07 2026 at 11:18): Email Gateway (Jul 07 2026 at 11:18):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Dear Isabelle developers,
I am working on the type annotation algorithm in
~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML that is used
by some interactive tools, e.g., Sledgehammer and Sketch and Explore.
The algorithm places type annotations in terms such that printing and
then parsing them again yields a term with the same type as the original
term. This is crucial when trying to output well-formed Isar proofs.
While testing the algorithm, I ran into some unfortunate behavior that
results from the interaction of Syntax_Trans.atomic_abs_tr' and the
syntax translation case_prod_tr'/case_prod_guess_names_tr' in
Product_Type.thy. You can observe this behavior in
Isabelle/333ffbe82f5f, where
term "λ_. 1 :: nat"
yields "λ_. 1" :: "'a ⇒ nat" while
term "λ(x, _). 1 :: nat"
gives "λ(x, uu_). 1" :: "'a × 'b ⇒ nat", which contains an internal
variable uu_. The latter term cannot be parsed after printing it due to
the internal variable. Note that the same behavior surfaces for other
users of Syntax_Trans.atomic_abs_tr' such as the translations for SOME
and set comprehensions.
The reason for the first term being printed without internal variables
is the changeset Isabelle/41986849fee0 that adds support for the syntax
constant _idtdummy (printed as _) to Syntax_Trans.abs_tr'/mk_binder_tr';
however, case_prod_tr'/case_prod_guess_names_tr' internally uses
Syntax_Trans.atomic_abs_tr', which has no support for _idtdummy. This
could be changed by a 4-line modification of Syntax_Trans.atomic_abs_tr'
(see attached diff), which produces the right result on the surface,
although I am not sure if there is any collateral.
Anecdotally, I know that users of Sketch and Explore have stumbled over
this behavior.
Cheers,
Lukas
Email Gateway (Jul 10 2026 at 15:19):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
After consulting with Tobias and Larry, I have now inspected all users
of Syntax_Trans.atomic_abs_tr' in the distribution and the AFP and
propose the attached changes. Except for a change in
HOL-Probability.Probability_Measure all changes are concerned with the
print_translation of Collect in HOL.Set and its clones. The change to
the print translation of Collect is necessary, since
Syntax_Trans.atomic_abs_tr' now might return _idtdummy instead of always
a variable. This changes the behavior of
term "{_. True}"
from outputting "{uu_. True}" to "{_. True}", which is arguably nicer.
The change to HOL-Probability.Probability_Measure is perhaps overly
defensive because the translation only works on bounded set
comprehensions: e.g., for a bounded set comprehension {x. x ∈ A ∧ True}
the bound variable x is always used, so it can never be replaced by a
dummy. Allowing dummies in bounded set comprehensions would therefore
require significant refinements. I have checked all other users of
Syntax_Trans.atomic_abs_tr' and convinced myself that no changes are
necessary. The AFP builds successfully with these changes:
https://build.proof.cit.tum.de/build?id=38dc54fc-0a32-4755-a0b3-496107c8d016.
Tobias has pointed out that he is the original author of the file, but
judging from the more recent history Makarius is the current owner of
the file. Makarius, can you comment on how to proceed?
Cheers,
Lukas
On 07.07.26 13:09, Lukas Stevens wrote:
Dear Isabelle developers,
I am working on the type annotation algorithm in
~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML that is
used by some interactive tools, e.g., Sledgehammer and Sketch and
Explore. The algorithm places type annotations in terms such that
printing and then parsing them again yields a term with the same type
as the original term. This is crucial when trying to output
well-formed Isar proofs.While testing the algorithm, I ran into some unfortunate behavior that
results from the interaction of Syntax_Trans.atomic_abs_tr' and the
syntax translation case_prod_tr'/case_prod_guess_names_tr' in
Product_Type.thy. You can observe this behavior in
Isabelle/333ffbe82f5f, whereterm "λ_. 1 :: nat"
yields "λ_. 1" :: "'a ⇒ nat" while
term "λ(x, _). 1 :: nat"
gives "λ(x, uu_). 1" :: "'a × 'b ⇒ nat", which contains an internal
variable uu_. The latter term cannot be parsed after printing it due
to the internal variable. Note that the same behavior surfaces for
other users of Syntax_Trans.atomic_abs_tr' such as the translations
for SOME and set comprehensions.The reason for the first term being printed without internal variables
is the changeset Isabelle/41986849fee0 that adds support for the
syntax constant _idtdummy (printed as _) to
Syntax_Trans.abs_tr'/mk_binder_tr'; however,
case_prod_tr'/case_prod_guess_names_tr' internally uses
Syntax_Trans.atomic_abs_tr', which has no support for _idtdummy. This
could be changed by a 4-line modification of
Syntax_Trans.atomic_abs_tr' (see attached diff), which produces the
right result on the surface, although I am not sure if there is any
collateral.Anecdotally, I know that users of Sketch and Explore have stumbled
over this behavior.Cheers,
Lukas
atomic_abs_tr.diff
atomic_abs_tr_AFP.diff
Email Gateway (Jul 10 2026 at 18:15):From: Makarius <makarius@sketis.net>
On 10/07/2026 17:11, Lukas Stevens wrote:
Tobias has pointed out that he is the original author of the file, but judging
from the more recent history Makarius is the current owner of the file.
Makarius, can you comment on how to proceed?
Tobias started the inner syntax engine > 30 years ago. I have reworked it so
many times since then that I don't remember how often it has changed.
In Isabelle development, we don't have "owners" of anything, but individuals
who are personally responsible for certain parts of the system.
I am personally responsible for everything around inner syntax.
I am presently busy elsewhere, and my mail folder is lagging behind several
months.
Re-openening a thread just after a few days of inactivity is a waste of time
--- it slows down the development process for no particular reason.
Makarius
Email Gateway (Aug 01 2026 at 13:32):From: Makarius <makarius@sketis.net>
On 07/07/2026 13:09, Lukas Stevens wrote:
I am working on the type annotation algorithm in ~~/src/HOL/Tools/
Sledgehammer/sledgehammer_isar_annotate.ML that is used by some interactive
tools, e.g., Sledgehammer and Sketch and Explore.While testing the algorithm, I ran into some unfortunate behavior that results
from the interaction of Syntax_Trans.atomic_abs_tr' and the syntax translation
case_prod_tr'/case_prod_guess_names_tr' in Product_Type.thy.
This is still open. I will take a brief look before we head to the
Isabelle2026 release, to see if it is to be addressed before or after the release.
After the release I would like to absorb all previous attempts to print terms
for re-parsing into Isabelle/Pure, such that becomes part of the regular
functionality.
Makarius
Email Gateway (Sep 21 2026 at 21:13):From: Makarius <makarius@sketis.net>
On 01/08/2026 15:32, Makarius wrote:
On 07/07/2026 13:09, Lukas Stevens wrote:
I am working on the type annotation algorithm in ~~/src/HOL/Tools/
Sledgehammer/sledgehammer_isar_annotate.ML that is used by some interactive
tools, e.g., Sledgehammer and Sketch and Explore.While testing the algorithm, I ran into some unfortunate behavior that
results from the interaction of Syntax_Trans.atomic_abs_tr' and the syntax
translation case_prod_tr'/case_prod_guess_names_tr' in Product_Type.thy.
This is still open. I will take a brief look before we head to the
Isabelle2026 release, to see if it is to be addressed before or after the
release.
I was delayed with many other things before Isabelle2026-RC1, so this was the
first thing to inspect. It turned out that there are many more corner cases of
printing abstractions: we have never taken it really serious in the past 3-4
decades. I was tempted to improve on it, but that is very bad timing for the
current release process. So I ended up mainly with this change:
changeset: 85671:fa5be76d009f
user: wenzelm
date: Mon Sep 21 19:38:30 2026 +0200
files: NEWS src/Pure/Syntax/syntax_trans.ML
src/Pure/type_infer_context.ML src/Pure/variable.ML
description:
more robust printing of terms with bound variables marked as "internal", e.g.
from vacuous abstraction;
Thus all places where bound variables are printed --- via mark_bound_abs or
mark_bound_body, to produce the "green" markup --- should give something that
can be parsed again. The following examples produce a regular "uu" instead of
internal "uu_":
term "∀_∈A. b"
term "λ(_, _). b"
In contrast, these guys produce an underscore, as before (because the print
translation is different, but not 100% correct either):
term "λ_. b"
term "∀_. b"
After the release I would like to absorb all previous attempts to print terms
for re-parsing into Isabelle/Pure, such that becomes part of the regular
functionality.
This has high priority, together with various improvements of many other
binder-like print operations.
We shall also need explicit checks that printed output can be
parsed/type-checked again: probably enabled by default, and disabled on request.
Makarius
Last updated: Oct 05 2026 at 16:54 UTC