Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context
No, I just sent you the (partial) source code to see whether you have a quick idea what
might be going wrong. A fully working example would have been a rather large attachment.
There seem to be some parts missing to run the example, e.g. run_hello_world. Do I need
I know that it is just a crude hack, but I have not yet had the time to develop an
interoperable, proper solution. It would be great if Isabelle had some support to actually
compile and execute generated code. "export_code ... checking SML Haskell Scala OCaml" is
already great, but it checks only syntactic correctness of the generated code.
The script makes many assumptions about the particular operating system environment. I
did not manage to run it myself yet.
I will keep on refining my attempt until some day it is maybe mature enough to be usable
by others, too.
Thanks for the hint with "set -x". That made me realise that the build script expects to
be run in the directory of the theory, but the function compile did not ensure this.
Apparently, I had started the Isabelle sessions from different directories and that caused
the difference between Isabelle2013-1 and Isabelle2013-2-RC3.
Maybe there is just some confusion about LD_RUN_PATH vs. LD_LIBRARY_PATH, which is changed
when the Isabelle process is run. With "set -x" in the script you should see in the output
what actually fails.
This archive was generated by a fusion of
Pipermail (Mailman edition) and