Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context



Hi Makarius,

There seem to be some parts missing to run the example, e.g. run_hello_world.  Do I need
this?
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.

The script makes many assumptions about the particular operating system environment.  I
did not manage to run it myself yet.
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.

I will keep on refining my attempt until some day it is maybe mature enough to be usable by others, too.

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

Andreas




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