Jakob Schulz (Apr 06 2023 at 15:15): Jakob Schulz (Apr 06 2023 at 15:15):Hi :)
I encountered an exception, of which I am not sure whether it is intentional or not. I have the following folder structure:
SomeFolder/
├─ Test.thy
Test.thy
The content of SomeFolder/Test.thy is just
theory Test
imports Main
begin end
while Test.thy imports this theory:
theory Test
imports "SomeFolder/Test.thy"
begin end
Now, everything works fine: I can define Lemmas in SomeFolder/Test.thy and use them in Test.thy. However, executing commands like find_theorems or sledgehammer inside Test.thy generates the following exception:
exception CONTEXT
("Cannot transfer: not a super theory", [], [],
["??.HOL.Trueprop
(??.HOL.eq
(??.Bit_Operations.semiring_bits_class.bit
(??.Power.power_class.power
(??.Num.numeral_class.numeral (??.Num.num.Bit0 ??.Num.num.One)) ?m)
?n)
(??.HOL.conj
(??.Bit_Operations.semiring_bits_class.possible_bit TYPE(?'a) ?n)
(??.HOL.eq ?m ?n)))"],
SOME
(
Theory
{Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups,
HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun,
HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,
HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields,
HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded,
HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,
HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn,
HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation,
HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,
HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base,
HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis,
HOL.Equiv_Relations, HOL.Transfer, HOL.Lifting, HOL.Num, HOL.Power,
HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function,
HOL.SAT, HOL.Quotient, HOL.Groups_Big, HOL.Fun_Def, HOL.Int,
HOL.Lattices_Big, HOL.Euclidean_Division, HOL.Parity,
HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis,
HOL.Set_Interval, HOL.Divides, HOL.Presburger, HOL.SMT, HOL.Sledgehammer,
HOL.Lifting_Set, HOL.List, HOL.Groups_List, HOL.Bit_Operations,
HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate,
HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random,
HOL.Code_Evaluation, HOL.Quickcheck_Random, HOL.Random_Pred,
HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile,
HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,
HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint,
HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main,
Draft.Test}
)) raised (line 612 of "thm.ML")
Is this intentional or a bug?
Manuel Eberl (Apr 06 2023 at 16:25):I'm not sure if it's intended behaviour that you are getting such an ugly error message, but the problem (and this is something that is known and unlikely to change any time soon) is that theory names have to be globally unique. If you have two theories with the exact same name, you cannot import both of them (even if they were to come from two different sessions).
This is probably an artefact of the fact that Isabelle was first developed some 30 years ago as a fun little experiment, and no one at the time thought it would ever be used on developments big enough for this to be a problem.
Wolfgang Jeltsch (Apr 06 2023 at 16:48):This issue is the reason why I prefix all my theory names with the session names: if I have a session called My_Session and a theory that should morally be called My_Theory, I name the theory My_Session-My_Theory (note the use of a hyphen instead of an underscore between the two name components; you need to surround the whole theory name with quotation marks for this to work).
Jakob Schulz (Apr 07 2023 at 08:04):I see, thank you both for your explanations and insights!
Last updated: Apr 28 2024 at 16:17 UTC