Re: [isabelle] Isabelle's environment and external executables
From: Lars Hupel <hupel at in.tum.de<mailto:hupel at in.tum.de>>
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 chalmers.se<mailto:moa.johansson at chalmers.se>>, "isabelle-users at cl.cam.ac.uk<mailto:isabelle-users at cl.cam.ac.uk>" <isabelle-users at cl.cam.ac.uk<mailto:isabelle-users at cl.cam.ac.uk>>
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
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
$ 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
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
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