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

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
 HIPSPEC_HOME="$COMPONENTâ

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â
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?

/Moa

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



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