Email Gateway (Aug 22 2022 at 10:12): Email Gateway (Aug 22 2022 at 10:12):From: Walther Neuper <wneuper@ist.tugraz.at>
this mail continues the thread broken at
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-June/msg00009.html
-------------------------------------------------------------------/
Lars,
... that demonstrates the genericity of libisabelle, great !
When integrating Protocol.thy into Isac [1] we run into problems now
[2]. We could eliminate some of the error messages (marked with @@@
instead of *** in [2] below) by replacing
imports Complex_Main
by imports "~~/src/HOL/Complex_Main"
in Isac's sources.
Should we replace imports by "~~/..." in the Isabelle sources, too?
Or: What are we doing wrong in [1]?
Walther
[1a] Isac's ROOT builds from Build_Isac
https://intra.ist.tugraz.at/hg/isa/file/43c1e5222f0e/src/Tools/isac/ROOT
[1b] while Build_Isac imports ".../Protocol"
https://intra.ist.tugraz.at/hg/isa/file/43c1e5222f0e/src/Tools/isac/Build_Isac.thy#l54
[1c] and Protocol imports "~~/src/Tools/isac/Frontend/Frontend", the
minimum required for operation_setup calctree etc:
https://github.com/wneuper/libisabelle/blob/master/libisabelle/src/main/isabelle/Protocol/Protocol.thy
[1d] libisabelle/../ROOT remains as is:
https://github.com/wneuper/libisabelle/blob/master/libisabelle/src/main/isabelle/Protocol/ROOT
[2] Error messages
wneuper@wneuper-w541:~/proto4/libisabelle$
/usr/local/isabisac/bin/isabelle build -D . -bv
Started at Mit Jun 10 09:00:41 CEST 2015 (polyml-5.5.2_x86-linux on
wneuper-w541)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/home/wneuper/.isabelle/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session Unsorted/Protocol
*** No such file: "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy"
*** The error(s) above occurred for theory "Complex_Main"
*** (required by "Protocol" via "Frontend" via "xmlsrc" via
"MutabelleExtra") (file
"/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
*** No such file: "/usr/local/isabisac/src/HOL/Library/Main.thy"
*** The error(s) above occurred for theory "Main"
*** (required by "Protocol" via "Frontend" via "xmlsrc" via
"MutabelleExtra" via "Refute") (file
"/usr/local/isabisac/src/HOL/Library/Refute.thy")
*** Incoherent imports for theory "Complex_Main":
@@@ "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy" (file
"/usr/local/isabisac/src/Tools/isac/KEStore.thy")
@@@ "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy" (file
"/usr/local/isabisac/src/Tools/isac/ProgLang/ListC.thy")
@@@ "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy" (file
"/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
@@@ "/usr/local/isabisac/src/Tools/isac/ProgLang/Complex_Main.thy"
(file "/usr/local/isabisac/src/Tools/isac/KEStore.thy")
@@@ "/usr/local/isabisac/src/Tools/isac/ProgLang/Complex_Main.thy"
(file "/usr/local/isabisac/src/Tools/isac/ProgLang/ListC.thy")
@@@ "/usr/local/isabisac/src/Tools/isac/ProgLang/Complex_Main.thy"
(file "/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
*** "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (file
"/usr/local/isabisac/src/Tools/isac/KEStore.thy")
*** "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (file
"/usr/local/isabisac/src/Tools/isac/ProgLang/ListC.thy")
*** "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (file
"/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
*** The error(s) above occurred in session "Protocol" (line 1 of
"libisabelle/src/main/isabelle/Protocol/ROOT")
Finished at Mit Jun 10 09:00:43 CEST 2015
0:00:02 elapsed time, 0:00:03 cpu time
Email Gateway (Aug 22 2022 at 10:12):From: Lars Hupel <hupel@in.tum.de>
build the "Protocol" session, but that one imports theories from Isac,
which in turn depends on HOL.
There are two ways to fix this: Modify the "ROOT" file of your
libisabelle copy so that it uses "HOL" instead of "Pure", or move the
theory files from libisabelle to the Isac repository and list it in its
"src/Tools/isac/ROOT" file.
By the way, is there a reason why the Isac repository is a clone of
Isabelle? Have you considered pulling the specific parts out and
registering it as an Isabelle component (according to §1.1.3 of the
system manual)?
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:13):From: Walther Neuper <wneuper@ist.tugraz.at>
From a brief glance at the build log, it appears that you first try to
build the "Protocol" session, but that one imports theories from Isac,
which in turn depends on HOL.
Right.
There are two ways to fix this: (1) Modify the "ROOT" file of your
libisabelle copy so that it uses "HOL" instead of "Pure", or (2) move the
theory files from libisabelle to the Isac repository and list it in its
"src/Tools/isac/ROOT" file.
We prefer (1), because we still want to keep apart libisabelle and Isac.
Your suggestion,
- session Protocol = Pure +
+ session Protocol = HOL +
however, again raises errors [1].
Another hint would be highly appreciated,
Walther
PS: Sorry for still not understanding completely how Isabelle manages
file dependencies in sessions.
[1]
wneuper@wneuper-w541:~/proto4/libisabelle$
/usr/local/isabisac/bin/isabelle build -D . -bv
Started at Mon Jun 15 18:36:24 CEST 2015 (polyml-5.5.2_x86-linux on
wneuper-w541)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/home/wneuper/.isabelle/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/Protocol
*** Incoherent imports for theory "Codec":
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Codec.thy"
(file
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy")
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Codec.thy"
(file "libisabelle/src/main/isabelle/Protocol/Codec_Test.thy")
*** "libisabelle/src/main/isabelle/Protocol/Codec.thy" (file
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy")
*** "libisabelle/src/main/isabelle/Protocol/Codec.thy" (file
"libisabelle/src/main/isabelle/Protocol/Codec_Test.thy")
*** The error(s) above occurred in session "Protocol" (line 1 of
"libisabelle/src/main/isabelle/Protocol/ROOT")
Finished at Mon Jun 15 18:36:26 CEST 2015
0:00:02 elapsed time, 0:00:06 cpu time
Email Gateway (Aug 22 2022 at 10:13):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
This works now, however, with ugly absolute paths:
/-------------------------------------------------------------------
theory Protocol
imports
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Codec"
"~~/src/Tools/isac/Frontend/Frontend"
:
--------------------------------------------------------------------/
Now I'm looking forward to completion of embedding on the ML-side with
great pleasure,
Walther
Email Gateway (Aug 22 2022 at 10:17):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
struggling with the error message
libisabelle$ java -cp full/target/scala-2.11/libisabelle-full.jar
Hello_PIDE
Exception in thread "main" java.lang.RuntimeException: Duplicate
session "RAW" (line 3 of "/usr/local/isabisac/src/Pure/ROOT") (line 3 of
"/usr/local/isabisac/src/Pure/ROOT")
when following your suggestionfor Hello_PIDE
JSystem sys = JSystem.instance(new File("/path/to/isac"), "Isac");
I see now, that I did not completely understand your fix:
There are two ways to fix this: (1) Modify the "ROOT" file of your
libisabelle copy so that it uses "HOL" instead of "Pure", or (2)
move the
theory files from libisabelle to the Isac repository and list it in its
"src/Tools/isac/ROOT" file.
We prefer (1), because we still want to keep apart libisabelle and Isac.
My question now: There is something wrong with the sessions [1] ---
--- isn't there some kind of mirror of libisabelle/../ROOT required in
isabisac (= Isabelle2014+Isac)?
Sorry not to be able to minimize the problem,
Walther
PS[1]: The error occurs in src/Pure/ROOT at "structure Distribution".
If I add to isabisac/ROOTS
+
/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol
the error remains the same, while isabisac accepts this +
without error.
Etc ...
PS[2]: Summary of the situation:
https://intra.ist.tugraz.at/hg/isa/file/eeb0940e0329/src/Tools/isac/Build_Isac.thy#l54
solved
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-June/msg00122.html
https://github.com/wneuper/libisabelle/commit/9e02c862175458867d492f3f0dd0aa7c79bd2d9f
* session Protocol = (Pure) HOL +
* Hello_PIDE:
JSystem sys = JSystem.instance(new File("."), "Protocol");
JSystem sys = JSystem.instance(new File("/usr/local/isabisac"), "Isac");
Email Gateway (Aug 22 2022 at 10:17):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
now I have a situation, which you can reproduce easily:
Hello_PIDE:
- JSystem sys = JSystem.instance(new
File("/usr/local/isabisac"), "Isac");
+ JSystem sys = JSystem.instance(new
File("/usr/local/Isabelle2014"), "HOL");
This gives:
libisabelle$ export ISABELLE_HOME=/usr/local/Isabelle2014
libisabelle$ /usr/local/Isabelle2014/bin/isabelle build -D . -bv
(* !!! session Protocol = (Pure) HOL + takes its time *)
libisabelle$ ./sbt full/assembly
(* ok *)
libisabelle$ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
Hello I'm Hello_PIDE!
Exception in thread "main" java.lang.RuntimeException: Duplicate
session "RAW" (line 3 of "/usr/local/Isabelle2014/src/Pure/ROOT")
(line 3 of "/usr/local/Isabelle2014/src/Pure/ROOT")
at isabelle.Library$ERROR$.apply(library.scala:20)
:
Do you have an idea, what is wrong here ?
Walther
Email Gateway (Aug 22 2022 at 10:17):From: Walther Neuper <wneuper@ist.tugraz.at>
now I have a situation, which can easily be reproduced:
even more easily reproduced:
$ git clone https://github.com/larsrh/libisabelle.git xxxxx
- JSystem sys = JSystem.instance(new File("."), "Protocol");
+ JSystem sys = JSystem.instance(new
File("/usr/local/Isabelle2014"), "HOL");
xxxxx$ export ISABELLE_HOME=/usr/local/Isabelle2014
xxxxx$ /usr/local/Isabelle2014/bin/isabelle build -D . -bv
xxxxx$ ./sbt full/assembly
xxxxx$ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
Exception in thread "main" java.lang.RuntimeException: Duplicate session
"RAW" (line 3 of "/usr/local/Isabelle2014/src/Pure/ROOT") (line 3 of
"/usr/local/Isabelle2014/src/Pure/ROOT")
at isabelle.Library$ERROR$.apply(library.scala:20)
:
How can one connect to some session ("HOL" and beyond) on the ML-side?
Hope to have sufficiently pinned down the situation herewith.
Thanks a lot in advance for your support,
Walther
Email Gateway (Aug 22 2022 at 10:19):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
since my last mail indicates, that there are principal questions about
Isabelle's session management (and not with settings of isabisac (=
Isabelle2014+Isac)), this question comes up:
Why not leave (PS(4))
JSystem.instance(new File("."), "Protocol");
as it was originally and import from isabisac this way (PS(2,3))
theory Protocol
imports Codec "~~/src/Tools/isac/Frontend/Frontend"
???
Wouldn't that agree better with your advice (On 2015-06-15 10:54)
Thank you very much for continuous support with the libisabelle
component, which is so important for Isac.
Walther
PS the full procedere:
(1) export ISABELLE_HOME=/usr/local/isabisac #= Isabelle2014+Isac
(2) theory Protocol
imports Codec "~~/src/Tools/isac/Frontend/Frontend"
(* "~~" refers to "/usr/local/isabisac" in (3), right? *)
(3) /usr/local/isabisac/bin/isabelle build -D . -bv
(4) edit Hello_PIDE:
JSystem sys = JSystem.instance(new File("."), "Protocol");
//JSystem sys = JSystem.instance(new File("/usr/local/isabisac"),
"Isac");
//"isabelle build -D . -bv" imports from isabisac via (2)
(5) edit libisabelle/../ROOT:
session Protocol = HOL +
(6) ./sbt full/assembly
(7) java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
java -cp full/target/scala-2.11/libisabelle-full.jar Mini_Test
ad (3) however, as discussed in previous mails, this causes the error:
wneuper@wneuper-w541:~/proto4/libisabelle$
/usr/local/isabisac/bin/isabelle build -D . -bv
Started at Mit Jun 24 08:30:46 CEST 2015 (polyml-5.5.2_x86-linux on
wneuper-w541)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/usr/local/isabisac/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"
*** Duplicate session "Protocol" (line 1 of
"libisabelle/src/main/isabelle/Protocol/ROOT") (line 1 of
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/ROOT")
Finished at Mit Jun 24 08:30:47 CEST 2015
0:00:01 elapsed time, 0:00:02 cpu time
Another question: How can one tell (3) about the relation to (5-6)?
Wouldn't that be necessary?
Notes:
(a) both paths in the error message are correct:
"libisabelle/src/main/isabelle/Protocol/ROOT"
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/ROOT"
(b) I see ISABELLE_BUILD_OPTIONS="" and continue investigations here.
Email Gateway (Aug 22 2022 at 10:20):From: Lars Hupel <hupel@in.tum.de>
I'm slightly confused about the current state of affairs here ... I'll
try my best to answer.
From a previous mail:
edit xxxxx/examples/src/main/java/Hello_PIDE.java
- JSystem sys = JSystem.instance(new File("."), "Protocol");
+ JSystem sys = JSystem.instance(new File("/usr/local/Isabelle2014"), "HOL");
The "File" object specifies the session root directory. Everything in
there will be added to the list of known sessions. Since Isabelle
already knows about its bundled sessions, adding $ISABELLE_HOME again
will naturally lead to duplicate sessions.
I take it that "/usr/local/isabisac" contains the full Isabelle
distribution with added Isac? I was expecting that you would specify
just the subdirectory of the Isac component.
Anyway, maybe using "." as path instead of $ISABELLE_HOME works.
Why not leave (PS(4))
JSystem.instance(new File("."), "Protocol");
as it was originally and import from isabisac this way (PS(2,3))
theory Protocol
imports Codec "~~/src/Tools/isac/Frontend/Frontend"???
It is a bit odd since you're including a "user-space" theory in a
"system-space" theory, but since all theories in an image are "equal"
regardless of their provenance, but conceptually, I don't see why this
shouldn't work.
Cheers
Lars
Last updated: Apr 30 2024 at 08:19 UTC