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



On Thu, 5 Dec 2013, Andreas Lochbihler wrote:

However, something else no longer works in Isabelle2013-2-RC3 although it worked in Isabelle2013-1. I have written a small script that compiles generated code and executes it to test whether my code generator setup works. So far, I used the following:

ML {*
fun using_master_directory thy p =
 p
 |> Path.explode
 |> Path.append (Thy_Load.master_directory thy)
 |> Path.append (File.pwd ())
 |> Path.implode

fun compile thy script_name params =
 let
   val script = using_master_directory thy script_name;
   val (output, exit) = Isabelle_System.bash_output (script ^ " " ^ params)
 in
   if exit = 0 then () else
     error ("Compile test failed for " ^ script_name ^ " and " ^ params ^
            ".\nreturn code: " ^ Int.toString exit ^ "\noutput:\n" ^ output)
 end

fun run thy program expected =
 let
   val prog = "cd " ^ using_master_directory thy "." ^ "; " ^ program
   val (output, exit) = Isabelle_System.bash_output prog
 in
   if exit = 0 andalso output = expected then () else
error ("Execution failed for " ^ program ^ "\nreturn code: " ^ Int.toString exit ^ "\nexpected output:\n" ^ expected ^ "\nactual output:\n" ^ output)
 end
*}

export_code run_hello_world same in SML file "SML/hello_world.ML"
ML {*
compile @{theory} "SML/build.sh" "SML/hello_world StdIO_Ex.run_hello_world";
 run @{theory} "SML/hello_world" "Hello world!\n";
*}

There seem to be some parts missing to run the example, e.g. run_hello_world. Do I need this?


where the script SML/build.sh looks as follows (it creates a test driver for the exported code, compiles it with polyml and cc to produce a stand-alone executable, such that the run function can then execute it.

#! /bin/bash
POLYHOME=~/.isabelle/contrib/polyml-5.5.0-3/x86_64-linux/
POLYLIB=${POLYHOME}

BUILD=$1_build.ML
cp $1.ML $BUILD
echo "PolyML.export (\"$1\", $2);" >> $BUILD
cat $BUILD | $POLYHOME/polyml
ret_code=$?
if [ ${ret_code} == 0 ]; then
LD_RUN_PATH=${POLYLIB}:${LD_RUN_PATH} cc -ggdb -o $1 -L${POLYLIB} -lpolymain -lpolyml $1.o
 ret_code=$?
fi
rm $BUILD $1.o
exit ${ret_code}

In Isabelle2013-1, this worked fine, but in Isabelle2013-2-RC3, I always get a return code of 1 (instead of 0) form build.sh even though it returns 0 when I execute it from my command line shell. Do you know what goes wrong here and what I have to adapt?

The script makes many assumptions about the particular operating system environment. I did not manage to run it myself yet.

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.

Depending on $ISABELLE_HOME_USER/etc/settings you may get different Poly/ML versions, also x86 vs. x86_64, that might cause a conflict with the one used above for batch compilation. Note that official releases have disjoint $ISABELLE_HOME_USER directories, so there could be some of your settings missing.


Looking also at the history diff of Isabelle2013-1 vs. Isabelle2013-2-RC3, the only change is related to shell command invocation is this: https://bitbucket.org/isabelle_project/isabelle-release/commits/d71e7908eec3 It should only affect the signalling, though, not any return codes.


	Makarius




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