Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected behavior when recursively importing...

Email Gateway (Oct 24 2024 at 13:33):

From: Fabian Huch <huch@in.tum.de>
In Isabelle/7d61f448f693, we just encountered some very puzzling
behavior: When importing Pure before Main, everything is fine, e.g.:

(* B.thy *)
theory B imports Pure Main begin
datatype t = X | Y
end

But when Pure is imported recursively before Main, things break:

(* A.thy *)
theory A imports Pure begin end

(* B.thy *)
theory B imports A Main begin
datatype t = X | Y
end

Here we get the following error from datatype (other HOL commands also
break with different errors -- it looks like Pure was re-defined):

exception SIMPLIFIER ("Congruence not a meta-equality",
["HOL.Trueprop (HOL.eq ?t ?t') ⟹ HOL.Trueprop (HOL.eq (B.t.case_t ?f1.0
?f2.0 ?t) (B.t.case_t ?f1.0 ?f2.0 ?t'))"]) raised (line 721 of
"raw_simplifier.ML")

This happens in both the interactive mode and headless build (full
example attached).

Fabian

unexpected.tar.gz

Email Gateway (Oct 24 2024 at 15:04):

From: Makarius <makarius@sketis.net>
On 24/10/2024 15:27, Fabian Huch wrote:

In Isabelle/7d61f448f693

That is an arbitrary repository version after Isabelle2024, and thus not
relevant on this mailing list.

I see the same in Isabelle2023 and Isabelle2024, though.

we just encountered some very puzzling behavior:
When importing Pure before Main, everything is fine, e.g.:

(* B.thy *)
theory B imports Pure Main begin
datatype t = X | Y
end

But when Pure is imported recursively before Main, things break:

(* A.thy *)
theory A imports Pure begin end

(* B.thy *)
theory B imports A Main begin
datatype t = X | Y
end

There are many ways to break things when going below Main: that is officially
not supported, and only works under certain side-conditions. Problems are not
unexpected.

So the usual question: What is the application? What are you trying to do?

Makarius

Email Gateway (Oct 24 2024 at 15:12):

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

On 10/24/24 17:03, Makarius wrote:

There are many ways to break things when going below Main: that is
officially not supported, and only works under certain
side-conditions. Problems are not unexpected.

So the usual question: What is the application? What are you trying to
do?

I was just puzzled about this -- I didn't think I would need a specific
application to import Pure and then Main.

Fabian

Email Gateway (Oct 24 2024 at 15:34):

From: Makarius <makarius@sketis.net>
On 24/10/2024 17:12, Fabian Huch wrote:

On 10/24/24 17:03, Makarius wrote:

There are many ways to break things when going below Main: that is
officially not supported, and only works under certain side-conditions.
Problems are not unexpected.

So the usual question: What is the application? What are you trying to do?

I was just puzzled about this -- I didn't think I would need a specific
application to import Pure and then Main.

Theory merges and theory graph construction is not fully symmetric.

As a rule of thumb you always start with Main (or an extension of it) and
merge whatever else you need from the right.

In Isabelle/ML this is exemplified by Library.merge, but sometimes it is a
variant of Basics.merge_options where content may get lost.

Makarius

Last updated: Jan 04 2025 at 20:18 UTC