Email Gateway (Oct 10 2024 at 12:41): Email Gateway (Oct 10 2024 at 12:41):From: Makarius <makarius@sketis.net>
* General *
Command "unbundle b" and its variants like "context includes b" allow
an optional name prefix with the reserved word "no": "unbundle no b"
etc. This inverts the polarity of bundled declarations like 'notation'
vs. 'no_notation', and thus avoids redundant bundle definitions like
"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may
be used instead. Consequently, the syntax for multiple bundle names has
been changed slightly, demanding an explicit 'and' keyword. Minor
INCOMPATIBILITY.
Command "open_bundle b" is like "bundle b" followed by "unbundle b",
so its declarations are applied immediately, but also named for later
re-use: "unbundle no b" etc.
Blocks for pretty-printing (of types, terms, props etc.) now support
properties "open_block" (bool) and "notation" (string as cartouche).
When "open_block" is enabled, the block has no impact on formatting, but
it may carry markup information via "notation". The latter uses formal
kinds (e.g. "mixfix", "infix", "binder") together with informal words to
describe the notation. This markup affects both input and output of
inner syntax --- it can be explored via mouse hovering in the Prover IDE
as usual (or programmatically by Isabelle/Scala tools). Markup for
"infix" and "binder" declarations are automatic, but general mixfix
forms require manual annotations in the theory library. Plenty of
existing examples may be found in the Isabelle sources by searching for
"notation=" (without quotes and no extra space). Occasional
INCOMPATIBILITY for 'no_syntax' or 'no_notation' declarations in user
applications: the mixfix template needs to be adapted accordingly, but
it is often better to use "unbundle no foobar_syntax", as explained for
HOL libraries below.
Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
in ML). Most Isabelle theories have been adapted accordingly, such that
hyperlinks work properly e.g. for "['a, 'b] ⇒ 'c" or "⟦A; B⟧ ⟹ C" in
Pure, and "∀x∈A. B x" or "∃x∈A. B x" in HOL.
* HOL *
Various declaration bundles support adhoc modification of notation,
notably like this:
unbundle no list_syntax
unbundle no list_enumeration_syntax
unbundle no list_comprehension_syntax
unbundle no relcomp_syntax
unbundle no converse_syntax
unbundle no rtrancl_syntax
unbundle no trancl_syntax
unbundle no reflcl_syntax
unbundle no abs_syntax
unbundle no floor_ceiling_syntax
unbundle no uminus_syntax
unbundle no funcset_syntax
This is more robust than individual 'no_syntax' / 'no_notation'
commands, which need to copy mixfix declarations from elsewhere and thus
break after changes in the library.
Theory "HOL-Library.Datatype_Records" provides bundle
"datatype_record_syntax" to exchange its alternative notation versus
regular "record_syntax". This also allows to swap record syntax later
on, notably like this:
unbundle no datatype_record_syntax
This refers to Isabelle/87f173836d56 and AFP/68a8276e79a0.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 12:46):From: Lawrence Paulson <lp15@cam.ac.uk>
And welcome for that reason. Thanks!
Larry
On 10 Oct 2024, at 13:25, Makarius <makarius@sketis.net> wrote:
This is more robust than individual 'no_syntax' / 'no_notation'
commands, which need to copy mixfix declarations from elsewhere and thus
break after changes in the library.
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 13:22):From: Makarius <makarius@sketis.net>
On 10/10/2024 14:25, Makarius wrote:
- Blocks for pretty-printing (of types, terms, props etc.) now support
properties "open_block" (bool) and "notation" (string as cartouche).
When "open_block" is enabled, the block has no impact on formatting, but
it may carry markup information via "notation". The latter uses formal
kinds (e.g. "mixfix", "infix", "binder") together with informal words to
describe the notation. This markup affects both input and output of
inner syntax --- it can be explored via mouse hovering in the Prover IDE
as usual (or programmatically by Isabelle/Scala tools). Markup for
"infix" and "binder" declarations are automatic, but general mixfix
forms require manual annotations in the theory library. Plenty of
existing examples may be found in the Isabelle sources by searching for
"notation=" (without quotes and no extra space). Occasional
INCOMPATIBILITY for 'no_syntax' or 'no_notation' declarations in user
applications: the mixfix template needs to be adapted accordingly, but
it is often better to use "unbundle no foobar_syntax", as explained for
HOL libraries below.
Some more remarks on this. Markup for pretty-blocks (or quasi blocks via
"open_block") replaces the old TODO-item of "markup of sub-expressions of
types/terms/blocks". The latter turned out as too complex to be ever
implemented, especially due to very ambitious syntax translations that have
emerged over the decades in applications.
Doing it on the surface of the inner-syntax instead, merely required some
"minor" cleanup and manual annotations of free-form mixfix syntax (not infix
nor binder). I have mostly done it for the main Isabelle library theories
already: HOL, HOL-Library, HOL-Algebra, HOL-Number_Theory, HOL-Analysis etc.
More isolated applications are missing, as well as most of AFP.
Some important inner-syntax idioms --- e.g. monad syntax and Hoare-logic
syntax --- still require further refinement. Ultimately, there should be just
one well-understood and uniform approach to it, not 3 different approaches to
7 different versions monads or Hoare logic.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 13:37):From: Makarius <makarius@sketis.net>
On 10/10/2024 14:25, Makarius wrote:
This markup affects both input and output of
inner syntax --- it can be explored via mouse hovering in the Prover IDE
as usual (or programmatically by Isabelle/Scala tools).
Further side-remarks:
* "output" means that I have reworked to Pretty-printing engine quite a
bit, to be more robust and scalable for tons of markup (lets say many MB up to
few GB).
* "input" means that I have applied approx. 60 small changes to
src/Pure/Syntax/parser.ML in order to have markup treated properly within the
regular Earley algorithm. I have discovered and removed various oddities in
the implementation, but did not understand all of its secrets. As usual, the
empiric test material was AFP (including performance).
The markup for input was specifically requested by people from Linz, as a
prerequisite to make an "accessible" Prover IDE eventually. It means that
users without eyesight can explore types/terms/props by a tactile interface.
(A few years ago VSCode had made quite some noise about "accessibility", but
that has degraded a lot recently, so it is not an immediate answer to the
problem.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 14:32):From: Makarius <makarius@sketis.net>
On 10/10/2024 15:36, Makarius wrote:
The markup for input was specifically requested by people from Linz, as a
prerequisite to make an "accessible" Prover IDE eventually. It means that
users without eyesight can explore types/terms/props by a tactile interface.
(A few years ago VSCode had made quite some noise about "accessibility", but
that has degraded a lot recently, so it is not an immediate answer to the
problem.)
Side-remark on this side-remark.
From what I've learned in Linz 1 year ago, the main Open-Source product in
this area is NVDA https://www.nvaccess.org (for Windows only).
The editor, whatever it is, needs to connect to that. There is even an
official accessibility API Java, but I don't know if and how that works.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC