Re: [isabelle] Isabelle's environment and external executables



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
- require an Isabelle environment to work (e.g. $ISABELLE_HOME) *and*
- are supposed to be run directly by the user.

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




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