Re: [isabelle] libisabelle: embedding on ML-side



this mail continues the thread broken at
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-June/msg00009.html
-------------------------------------------------------------------/

Lars,

   JSystem sys = JSystem.instance(new File("/path/to/isac"), "Isac");

... 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 at 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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.