Re: [isabelle] file name of export_code



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





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