Email Gateway (Aug 23 2022 at 08:50): Email Gateway (Aug 23 2022 at 08:50):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Dear all,
I'm having the following error when trying to run jEdit via the command
Isabelle2020:
/Failed to execute application script "./lib/scripts/Isabelle_app"/
I have unpacked Isabelle into a directory called bin in my home. There
may be some problem on how Isabelle2020 looks for this file, because if
I run
~/bin/Isabelle2020/Isabelle2020
it works smoothly. My PATH includes
//home/pedro/bin/Isabelle2020/bin:/home/pedro/bin/Isabelle2020/:/home/pedro/bin/Isabelle2020/lib/scripts//
/
(the last one was added to try to solve the problem). This also failed
in the release candidates, but I didn't try it before because I needed
to throw some command line options through isabelle jedit.
Did anyone experience this issue?
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Email Gateway (Aug 23 2022 at 08:50):From: Makarius <makarius@sketis.net>
This merely means you should not try to play with the PATH, especially not for
the toplevel executable "Isabelle2020" --- it wants to have its full
executable path as argument 0.
A more standard way is to use "isabelle install ~/bin" and then "isabelle
jedit ...", assuming that ~/bin is already in your PATH.
You can also look at the generated shell scripts in ~/bin to see how to make
an alias to Isabelle executables, without breaking the integrity of the
application, i.e. like this:
#!/usr/bin/env bash
exec "/home/makarius/lib/Isabelle2020/Isabelle2020" "$@"
Makarius
Last updated: Apr 20 2024 at 12:26 UTC