Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Ctrl-Click on abbreviation from locale in imag...

view this post on Zulip Email Gateway (Aug 19 2022 at 13:12):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,

I noticed that when I open a locale that has been defined in the image of the session and
Ctrl-Click on an identifer which refers to an abbreviation in that locale, then
Isabelle/jEdit jumps to the begin of the context block. I would have expected that it
jumps to the declaration of the abbreviation as it does for definitions. Here's a MWE for
Isabelle2013-1:

theory Scratch imports Main begin
(1)context partial_function_definitions begin
term "fixp_fun"
end
end

Ctrl-Click on fixp_fun jumps to (1), but I would prefer line 130 of Partial_Function.thy.

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 13:12):

From: Makarius <makarius@sketis.net>
This is a general shortcoming due to the way how formal entities and their
positions are managed internally. I have been aware of it when I
introduced the concept some years ago, even before a usable Prover IDE
front-end was available. Similar inconveniences happen when declarations
and attributed fact expressions are processed in various situations of
local context.

Further refinement of this area needs to be postponed until more serious
problems are solved.

You are mentioning Isabelle2013-1 above. Can you also give quick try to
http://isabelle.in.tum.de/website-Isabelle2013-2-RC3/ ? There are at
least 24h more time, before I consider making the final snapshot for
Isabelle2013-2.

Isabelle2013-1 did not work out so well, due to too few people putting
hard measures of testing on it. You are the expert on getting to the
limits of what is possible and what not ...

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 13:13):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,

You are mentioning Isabelle2013-1 above. Can you also give quick try to
http://isabelle.in.tum.de/website-Isabelle2013-2-RC3/ ? There are at least 24h more time,
before I consider making the final snapshot for Isabelle2013-2.
At the moment, I am hooked on the repository version, I have simply checked that the same
behaviour also occurs with Isabelle2013-1. But I'll see whether I find some time tomorrow
to give it a try.

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.

You are the expert on getting to the limits of what is possible and what not ...
Well, but I only hit the limits during my normal work; a quick check usually does not take
me there.

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 13:13):

From: Makarius <makarius@sketis.net>
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.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 13:14):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,

I quickly testes Isabelle2013-2-RC3 with XEmacs and ProofGeneral 3.7.1.1 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 =
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";
*}

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?

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 13:14):

From: Makarius <makarius@sketis.net>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 13:14):

From: Makarius <makarius@sketis.net>
After some more tinkering with the script, it somehow works for me with
polyml-5.5.0-3, using the following in $ISABELLE_HOME_USER/etc/settings:

ML_PLATFORM=x86_64-linux
ML_HOME="$HOME/.isabelle/contrib/polyml-5.5.0-3/$ML_PLATFORM"
ML_SYSTEM=polyml-5.5.0
ML_OPTIONS="-H 1000 --gcthreads 4"
ML_SOURCES="$ML_HOME/../src"

I've run the build.sh either via "isabelle env ..." in the shell or via
ML {* Isabelle_System.bash ...*}, which should provide the same process
environment in both situations.

Note that David Matthews changed the ways of Poly/ML batch compilation in
Poly/ML 5.5.1, which is bundled with Isabelle2013-1 and Isabelle2013-2
(uniformly for all release candidates). The new polyc script might
actually help to make this more robust.

For now, I merely need a confirmation that the issues is just one of local
settings, not due to any change in the long chain of release candidates.

Makarius
build.sh

view this post on Zulip Email Gateway (Aug 19 2022 at 13:14):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 30 2024 at 04:19 UTC