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

From: Lars Hupel <hupel at<mailto:hupel at>>
Subject: Re: [isabelle] Isabelle's environment and external executables
Date: 9 May 2016 at 14:22:50 GMT+2
To: Moa Johansson <moa.johansson at<mailto:moa.johansson at>>, "isabelle-users at<mailto:isabelle-users at>" <isabelle-users at<mailto:isabelle-users at>>

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

Yes, indeed.

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

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
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.

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.

It would make the installation of my tool easier.
Or is there a good reason not to do this?


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

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