Email Gateway (Aug 18 2022 at 17:58): Email Gateway (Aug 18 2022 at 17:58):From: Brian Huffman <brianh@cs.pdx.edu>
Hello all,
I have recently noticed some weird/undesirable behavior with regards
to lattice syntax. Exploring this issue brings up some fundamental
questions about what it really means for Isabelle to merge two
theories.
As many of you may know, HOL/Lattices.thy defines infix syntax for
various lattice operations, including binary "inf" and "sup"; but then
it uses "no_notation" to erase this syntax at the end of the file, to
avoid using up so many precious symbols. Users who want to use the
syntax can import it from HOL/Library/Lattice_Syntax, like this:
theory Scratch imports "~~/src/HOL/Library/Lattice_Syntax" begin
term "x \<sqinter> y" (* parses as "inf x y" *)
When I wrote my Free Boolean Algebra AFP entry (which makes heavy use
of the lattice syntax) I followed what seemed to be the best practice,
and used "no_notation" to delete the syntax again.
I expected that users of my Free_Boolean_Algebra library would be able
to use the lattice syntax (if they chose to do so) by importing
Library/Lattice_Syntax again. Unfortunately this does not work!
theory Scratch
imports
"~~/src/HOL/Library/Lattice_Syntax"
"~/hg/afp/thys/Free-Boolean-Algebra/Free_Boolean_Algebra"
begin
term "x \<sqinter> y"
*** Inner lexical error at: \<sqinter> y (line 7 of
"/home/brianh/Documents/Isabelle/Scratch.thy")
*** Failed to parse term
*** At command "term" (line 7 of "/home/brianh/Documents/Isabelle/Scratch.thy")
I thought that when you say "theory C imports A B begin", Isabelle
should actually merge theories A and B. In particular, any input
syntax that exists in either theory A or theory B should be available
in theory C. But that is not the case here! The syntax in
Lattice_Syntax is completely ignored.
Evidently, Isabelle assumes that merging Lattice_Syntax +
Free_Boolean_Algebra will be equal to the Free_Boolean_Algebra theory
by itself (because Lattice_Syntax is an ancestor theory of
Free_Boolean_Algebra) and optimizes away the actual theory merge. But
this is an invalid assumption.
Email Gateway (Aug 18 2022 at 17:58):From: Lukas Bulwahn <bulwahn@in.tum.de>
On 07/28/2011 05:28 PM, Brian Huffman wrote:
Hello all,
I have recently noticed some weird/undesirable behavior with regards
to lattice syntax. Exploring this issue brings up some fundamental
questions about what it really means for Isabelle to merge two
theories.As many of you may know, HOL/Lattices.thy defines infix syntax for
various lattice operations, including binary "inf" and "sup"; but then
it uses "no_notation" to erase this syntax at the end of the file, to
avoid using up so many precious symbols. Users who want to use the
syntax can import it from HOL/Library/Lattice_Syntax, like this:theory Scratch imports "~~/src/HOL/Library/Lattice_Syntax" begin
term "x \<sqinter> y" (* parses as "inf x y" *)When I wrote my Free Boolean Algebra AFP entry (which makes heavy use
of the lattice syntax) I followed what seemed to be the best practice,
and used "no_notation" to delete the syntax again.I expected that users of my Free_Boolean_Algebra library would be able
to use the lattice syntax (if they chose to do so) by importing
Library/Lattice_Syntax again. Unfortunately this does not work!theory Scratch
imports
"~~/src/HOL/Library/Lattice_Syntax"
"~/hg/afp/thys/Free-Boolean-Algebra/Free_Boolean_Algebra"
beginterm "x \<sqinter> y"
*** Inner lexical error at: \<sqinter> y (line 7 of
"/home/brianh/Documents/Isabelle/Scratch.thy")
*** Failed to parse term
*** At command "term" (line 7 of "/home/brianh/Documents/Isabelle/Scratch.thy")I thought that when you say "theory C imports A B begin", Isabelle
should actually merge theories A and B. In particular, any input
syntax that exists in either theory A or theory B should be available
in theory C. But that is not the case here! The syntax in
Lattice_Syntax is completely ignored.Evidently, Isabelle assumes that merging Lattice_Syntax +
Free_Boolean_Algebra will be equal to the Free_Boolean_Algebra theory
by itself (because Lattice_Syntax is an ancestor theory of
Free_Boolean_Algebra) and optimizes away the actual theory merge. But
this is an invalid assumption.Obviously, you cannot load a theory twice in Isabelle.
So, it is not only an optimization but an necessity not to load and
merge the theory twice in your situation.
I guess the pragmatic solution is to ask your users to use a clone of
Lattice_Syntax with a different name. The correct technical solution in
Isabelle is a local context-aware infrastructure for syntax, which is
just a little bit out of reach right now, but other people can probably
describe the situation more in-depth than I can right now.
Lukas
- Brian
Email Gateway (Aug 18 2022 at 17:58):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Jul 28, 2011 at 9:26 AM, Lukas Bulwahn <bulwahn@in.tum.de> wrote:
Obviously, you cannot load a theory twice in Isabelle.
So, it is not only an optimization but an necessity not to load and merge
the theory twice in your situation.
Loading and merging are separate things. I am not asking Isabelle to
load the same theory twice. I am merely asking Isabelle to merge a
theory with one of its ancestors.
I guess the pragmatic solution is to ask your users to use a clone of
Lattice_Syntax with a different name.
I am well aware of a workaround. All I have to do is create a dummy
empty theory file called "Lattice_Syntax_Copy" that imports
Lattice_Syntax.
theory Lattice_Syntax_Copy imports Lattice_Syntax begin
end
Now, since Lattice_Syntax_Copy is not actually an ancestor of
Free_Boolean_Algebra, then Isabelle can be persuaded to do actually
merge them together.
theory Scratch imports Lattice_Syntax_Copy Free_Boolean_Algebra begin
term "x \<sqinter> y" (* this works *)
The correct technical solution in
Isabelle is a local context-aware infrastructure for syntax, which is just a
little bit out of reach right now, but other people can probably describe
the situation more in-depth than I can right now.
Yes, a much nicer long-term solution would be something that would
make the whole no_notation/Lattice_Syntax.thy hack unnecessary.
But in the short term, it would be nice for theory imports to behave
in the way I expect (i.e. actually merge every theory in the import
list, without throwing any away). I tracked the problem to the
function Context.begin_thy in Pure/context.ML. The function
maximal_thys implents the ignore-ancestors-in-imports bug/feature:
fun maximal_thys thys =
thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy,
thy')) thys);
fun begin_thy pp name imports =
if name = "" orelse name = draftN then error ("Bad theory name: " ^
quote name)
else
let
val parents = maximal_thys (distinct eq_thy imports);
...
Email Gateway (Aug 18 2022 at 17:58):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
At the current state of the art, I see two approaches to deal with that
issues:
In the long run the vision is to have syntax managed by locales and this
acitvate it on demand.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:59):From: Alexander Krauss <krauss@in.tum.de>
One cannot change the semantics of theory merges "in the short term",
just because "no_notation" happens to be conceptually broken. We must
get rid of it, instead of going further in the same direction.
Alex
Email Gateway (Aug 18 2022 at 17:59):From: Brian Huffman <brianh@cs.pdx.edu>
I am not suggesting that we change the merge behavior "just because
no_notation is broken". Rather, I am suggesting that we change the
merge behavior because the merge behavior itself is broken. The
no_notation command just happens to be the thing that caused me to see
the problem; the basic problem with theory merging is really much more
general.
The current ignore-everything-but-maximal-theories merge behavior was
introduced in 2005:
http://isabelle.in.tum.de/repos/isabelle/rev/f1152f75f6fc
This implementation assumes that when a user imports theories A and B,
where A is an ancestor to B, then merging A and B will always yield a
theory that is identical to B. So, as an optimization, it doesn't
bother to merge A at all.
The implicit assumption here, upon which the correctness of this
optimization rests, is that descendant theories only extend the theory
context in a monotonic fashion. The problem is that this simply is not
true.
The "no_notation" command is one example of something that modifies
the theory context in a non-monotonic way, deleting something from the
context, instead of adding to it. You say that we may eventually get
rid of the "no_notation" command, but what about all the other
commands that delete things from the theory context? Will "declare foo
[simp del]" be phased out as well?
I propose that we go back to the pre-2005 theory merge semantics, by
reverting the relevant portion of changeset f1152f75f6fc. If at some
point in the future we manage to completely eradicate all
non-monotonic theory-updating commands, at that time it might be safe
to reinstate the maximal-theories-only optimization.
Last updated: Apr 23 2024 at 16:19 UTC