Email Gateway (Aug 18 2022 at 14:12): Email Gateway (Aug 18 2022 at 14:12):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I have an export_code ... file "foo.ML" statement.
However, the file "foo.ML" is created in the directory of the theory
where the Isabelle-process was first started on, that is not necessarily
the directory of the theory containing the export_code statement.
This currently results in getting ML-files of different ages splattered
around my thy-directories, depending on what theory I load first.
Is there a way to place the generated code file in the directory of the
theory that contains the export_code statement?
There seem to be some shortcuts like "~~" for the isabelle-home
directory (?). Are those shortcuts documented somewhere? Is there
perhaps even a shortcut for the directory of the current theory file?
Regards and many thanks in advance for any hints,
Peter
Email Gateway (Aug 18 2022 at 14:13):From: Makarius <makarius@sketis.net>
On Thu, 1 Oct 2009, Peter Lammich wrote:
I have an export_code ... file "foo.ML" statement. However, the file
"foo.ML" is created in the directory of the theory where the
Isabelle-process was first started on, that is not necessarily the
directory of the theory containing the export_code statement.
You are right, when Proof General starts the process, it uses the cwd of
the associated buffer that happens to be in front at that time. So the
result is indeed erratic.
There seem to be some shortcuts like "~~" for the isabelle-home
directory (?). Are those shortcuts documented somewhere?
It might be buried in one of our many manuals from different periods, or
maybe not.
Isabelle path specifications are as follows:
- Basic posix notation with ".", "..", "/" and root "/"
- environment variables $HOME, $ISABELLE_HOME, $WHATEVER, ...
- abbreviated variables: ~ for $HOME, and ~~ for $ISABELLE_HOME
The basic idea of the Isabelle environment is explained in the "system"
manual, and is in fact quite central to the Isabelle system since 1998.
Is there perhaps even a shortcut for the directory of the current theory
file?
I've occasionally thought about things like that. Of course the
environment cannot be changed during the load process, because this would
be a global side-effect.
Maybe the notion of "project directory" would work better, i.e. an
environment "constant" that points to the root directory of a session
(where ROOT.ML is at the moment).
Makarius
Last updated: Apr 25 2024 at 12:23 UTC