Email Gateway (Aug 23 2022 at 08:51): Email Gateway (Aug 23 2022 at 08:51):From: Georgy Dunaev <georgedunaev@gmail.com>
I want to be able to do "go to definition" action in ZFC_in_HOL. Now I can
do it only once: from my file example.thy to definition of set or V or
elts. But I cannot go deeper: the text in the HOL library is highlighted
with red color. What is wrong?
I've done this:
1)installed ZFC_in_HOL from AFP using the instruction.
2)changed "logic session name" in the top right corner of window to
"ZFC_in_HOL" and restarted Isabelle.
3)obtained info
"
Build started for Isabelle/ZFC_in_HOL ...
Building ZFC_in_HOL
ZFC_in_HOL: theory HOL-Cardinals.Fun_More
ZFC_in_HOL: theory HOL-Cardinals.Order_Relation_More
ZFC_in_HOL: theory HOL-Library.FuncSet
ZFC_in_HOL: theory HOL-Cardinals.Order_Union
ZFC_in_HOL: theory HOL-Library.Infinite_Set
ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Extension
ZFC_in_HOL: theory HOL-Library.Nat_Bijection
ZFC_in_HOL: theory HOL-Cardinals.Wellfounded_More
ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Relation
ZFC_in_HOL: theory HOL-Library.Old_Datatype
ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Embedding
ZFC_in_HOL: theory HOL-Library.Equipollence
ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Constructions
ZFC_in_HOL: theory HOL-Library.Countable
ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Order_Relation
ZFC_in_HOL: theory HOL-Cardinals.Ordinal_Arithmetic
ZFC_in_HOL: theory HOL-Library.Countable_Set
ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Arithmetic
ZFC_in_HOL: theory HOL-Cardinals.Cardinals
ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Library
ZFC_in_HOL: theory ZFC_in_HOL.ZFC_in_HOL
ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Cardinals
ZFC_in_HOL: theory ZFC_in_HOL.Kirby
ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Typeclasses
Finished ZFC_in_HOL (0:00:43 elapsed time, 0:02:15 cpu time, factor 3.09)
OK
"
But I can not use HOL go to definition.
example.thy:
theory newzfc imports ZFC_in_HOL.ZFC_in_HOL
begin
axiomatization qwe :: "bool set"
end
The file
$ISABELLE_HOME/src/HOL/Set.thy
is red and definitions are not clickable.
How to repair the IDE?
Sincerely Yours,
Georgy Dunaev
Email Gateway (Aug 23 2022 at 08:51):From: Peter Lammich <lammich@in.tum.de>
Hi,
that's a well known weakness of cross-referencing. It only works from
theories that are actually loaded in this session. If the theory is
already in the image your session is based on, it cannot be loaded
again (The error message for the red highlighting should read something
like "cannot reload already loaded theory"), and if it is not loaded,
cross-referencing does not work.
Last updated: Apr 24 2024 at 04:17 UTC