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

Dear Makarius,

I quickly testes Isabelle2013-2-RC3 with XEmacs and ProofGeneral and in terms of UI, everything seems to work as good as it did before (I am already used to the problem that interruptions sometimes get PG out of sync with Isabelle and I have to retract the theory or restart Isabelle, but this does not seem to happen more often than with Isabelle2013).

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 =
  |> Path.explode
  |> Path.append (Thy_Load.master_directory thy)
  |> Path.append (File.pwd ())
  |> Path.implode

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

fun run thy program expected =
    val prog = "cd " ^ using_master_directory thy "." ^ "; " ^ program
    val (output, exit) = Isabelle_System.bash_output prog
    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)

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

where the script SML/ 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

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


On 04/12/13 18:02, Makarius wrote:
On Wed, 4 Dec 2013, Andreas Lochbihler wrote:

Isabelle2013-1 did not work out so well, due to too few people putting hard measures of
testing on it.
Well, I did test Isabelle2013-1-RC* over several weeks, but mostly ProofGeneral.

There were various changes for Isabelle2013-2 that affect interaction and process
management in general: TTY, Proof General, PIDE document editing. So it is important to
see if it still works for you.


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