Email Gateway (Aug 22 2022 at 13:19): Email Gateway (Aug 22 2022 at 13:19):From: Moa Johansson <moa.johansson@chalmers.se>
Hi all,
I’m calling some external (Haskell) executables from inside Isabelle. If I start isabelle from the shell (using the command “isabelle jedit”) it works fine, and my executables are picked up from my bash environment as they’re in the PATH. However, if I start Isabelle by double-clicking, the environment is different, and Isabelle no longer finds what is in my normal path.
I’ve consulted the Isabelle Systems Manual, and tried to follow the instructions to add the paths to the ISABELLE_TOOLS environment variable in my $ISABELLE_HOME_USER/etc/settings, but that does not work. I’ve also tried adding the path to $ISABELLE_HOME_USER/etc/components but that made no difference either.
Obviously doing something silly but wrong, as it should be easy to add something to Isabelle’s environment.
Here are the gory details, my Isabelle extension is looking for two executables called “HipSpecifyer” and “hipster-hipspec”, but fails to find them:
/var/folders/sl/hb1d9hld2tsfgn33xgsxt1lc0000gp/T/isabelle-moajohansson3147/bash_script1000488: line 1: HipSpecifyer: command not found
/var/folders/sl/hb1d9hld2tsfgn33xgsxt1lc0000gp/T/isabelle-moajohansson3147/bash_script1000491: line 1: hipster-hipspec: command not found
Best,
Moa
Email Gateway (Aug 22 2022 at 13:19):From: Lars Hupel <hupel@in.tum.de>
Hi Moa,
I’m calling some external (Haskell) executables from inside Isabelle. If I start isabelle from the shell (using the command “isabelle jedit”) it works fine, and my executables are picked up from my bash environment as they’re in the PATH. However, if I start Isabelle by double-clicking, the environment is different, and Isabelle no longer finds what is in my normal path.
I would personally avoid calling tools via PATH, because things tend to
not work reliably (as you observed too).
I’ve consulted the Isabelle Systems Manual, and tried to follow the instructions to add the paths to the ISABELLE_TOOLS environment variable in my $ISABELLE_HOME_USER/etc/settings, but that does not work. I’ve also tried adding the path to $ISABELLE_HOME_USER/etc/components but that made no difference either.
An "Isabelle tool" is an executable which can be invoked using the "tool
wrapper", e.g. like this:
$ isabelle build
Here, "build" is a "tool". You should register executables as tools if they
On the other hand, an "Isabelle component" acts more as an extension for
Isabelle. It looks like this would be the correct approach for your use
case.
However, Isabelle components require a little bit of setup. In essence,
a component is just a path somewhere on your file system which has been
added to "etc/components" (you did that already). Let's say this is
"/path/to/hipspec". Additionally, you need an "etc/settings" file in
this path.
$ cat /path/to/hipspec/etc/settings
HIPSPEC_HOME="$COMPONENT"
The special $COMPONENT variable is provided during initialization of the
component. The end result is that $HIPSPEC_HOME will refer to that path
in a stable and reproducible manner.
The very same mechanism is used to provide the $AFP variable from the
AFP repository.
Note that the above approaches are not mutually exclusive. You can also
register more Isabelle tools in the "etc/settings" file. Isabelle tools
can be executed from within Isabelle/ML using
"Isabelle_System.isabelle_tool".
Hope that helps,
Lars
Email Gateway (Aug 22 2022 at 13:19):From: Lars Hupel <hupel@in.tum.de>
So, to check that I’ve understood correctly:
- Both my executables are in "$HOME/Library/Haskell/bin/“
- $ISABELLE_USER/etc/components I add one line with the path to where the executables are.
- I then have to create a file etc/settings also in "$HOME/Library/Haskell/bin/“
- In this file I include the line
$HOME/Library/Haskell/bin/="$COMPONENT”
Almost. The line literally has to say:
HIPSPEC_HOME="$COMPONENT"
It’s a little bit complicated, yes. I’d like to avoid too much set up burden for the user of my tool if possible.
How do you plan to distribute your tool? Maybe you could publish a
tarball with the binaries or build instructions; then all you'd have to
do would be to tell your users to
1) unpack it somewhere
2) add "/path/to/unpacked/tarball" to $ISABELLE_HOME_USER/etc/components
You can bundle the "etc/settings" into the tarball, as there's nothing
installation-specific in there.
But to be fair if you want to put your tools alongside other
non-Isabelle-specific Haskell executables somewhere under "~/bin", it's
not the best idea to register that path as a component. (Locally it's
fine if you know what you're doing, but I wouldn't impose that on users.)
I wonder if the best option for me is to just create one new environment variable in $ISABELLE_USER/etc/settings
(e.g. HIPSPEC_HOME=$HOME/Library/Haskell/bin/)
and then let my code refer to this path, instead of just the names of the executables, e.g. ./$HIPSPEC_HOME/hipster-hipspec.
You could also do that. That's basically the way it works for some other
executables, e.g. ISABELLE_GHC or ISABELLE_OCAML.
It would make the installation of my tool easier.
I'd say it's about the same complexity for installation.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:19):From: Makarius <makarius@sketis.net>
If you have users of your tool apart from yourself, the canonical
approach is to make a proper (self-contained) Isabelle component in just
one directory, and tell users to add a suitable "init_component" line to
their $ISABELLE_HOME_USERS/etc/settings or add the directory to
$ISABELLE_HOME_USERS/etc/components.
There are plenty of existing examples: more than half of the Isabelle
distribution consists of such components. They just happen to be shipped
by default.
Makarius
Last updated: Apr 27 2024 at 01:05 UTC