There's long been an issue with "use" when trying to compile and run files which themselves contain "use". For example if ROOT.ML contains: use "first.ML"; use "second.ML";
The inner calls to "use" are taken relative to whatever the original working directory was set to, which means that ROOT.ML always has to be called with the right directory. It's not possible to call use "/home/david/mydirectory/ROOT.ML"; from an arbitrary directory.
I've committed a change to the NestedUse branch which is one possible solution to this. The version of "use" in there records the full path to the parent directory of the file name when a file is "used". If that file then contains a nested call to "use" the file is first checked as previously using the original working directory but if that fails it looks for the name by appending the parent directory to the name given. So in the example above, it would first look for "./first.ML" and only if that does not exist would it look for "/home/david/mydirectory/first.ML".
This seems as though it should achieve the desired effect with the minimum change to existing programs but there are other alternatives. For example, should it look first relative to the parent directory?
David
On Thu, 15 Oct 2015, David Matthews wrote:
There's long been an issue with "use" when trying to compile and run files which themselves contain "use".
This seems as though it should achieve the desired effect with the minimum change to existing programs but there are other alternatives. For example, should it look first relative to the parent directory?
Isabelle used to use the built-in scheme for "use" of the underlying ML system in distant past. There were many special cases and sources of confusion. Over the years we have reworked that many times.
Today we have rather simple and rigid scheme:
* Each source file has a "master directory" (what you have called "parent directory" on this thread).
* Loaded resources always/unconditionally prepend the master directory of the enclosing file, without checking presence in the file system.
This means there are no "disjunctions" in how resources of a project are resolved.
Moreover there is no dependence on the file-system state. The latter aspect is particularly important in the IDE: it allows to manage resources abstractly without the physical file-system. The IDE could also create required but missing resources on the spot.
Makarius
David,
On Thu, 2015-10-15 at 15:18 +0100, David Matthews wrote:
I've committed a change to the NestedUse branch which is one possible solution to this. The version of "use" in there records the full path to the parent directory of the file name when a file is "used". If that file then contains a nested call to "use" the file is first checked as previously using the original working directory but if that fails it looks for the name by appending the parent directory to the name given. So in the example above, it would first look for "./first.ML" and only if that does not exist would it look for "/home/david/mydirectory/first.ML".
With this change, use "/home/david/mydirectory/ROOT.ML"; will work as intended *unless* there happens to be a file 'first.ML' in the current directory. In my view, this is a rather obscure error condition with great potential for accidental surprises.
The current implementation at least has a simple specification. Also, it is not at all uncommon to interpret paths relative to the current working directory; e.g., bash does the same.
What may be missing in SML is a way to determine the name and path of the file that is being 'used.'
Best, Tjark
On Tue, 20 Oct 2015, Tjark Weber wrote:
What may be missing in SML is a way to determine the name and path of the file that is being 'used.'
In Isabelle/ML (which is not SML) this can be done like this:
Position.file_of @{here}
where @{here} identifies its own position in the ML source via the abstract type Position.T; the fileprojected from it is (string option) since ML source does not necessarily reside in a file.
There is another subtle semantic problem, because the file-name is usually physical, and thus subject to the accidental situation at compile-time. Moving the compiled application later will render this invalid.
In Isabelle the latter happens when "the world" (e.g. the HOL image) is compiled and later moved around. There is a special trick to fold the compile-time ISABELLE_HOME directory prefix into the symbolic variable $ISABELLE_HOME, so it can be derefenced dynamically at run-time.
Makarius
On 20/10/2015 13:03, Tjark Weber wrote:
On Thu, 2015-10-15 at 15:18 +0100, David Matthews wrote:
I've committed a change to the NestedUse branch which is one possible solution to this. The version of "use" in there records the full path to the parent directory of the file name when a file is "used". If that file then contains a nested call to "use" the file is first checked as previously using the original working directory but if that fails it looks for the name by appending the parent directory to the name given. So in the example above, it would first look for "./first.ML" and only if that does not exist would it look for "/home/david/mydirectory/first.ML".
With this change, use "/home/david/mydirectory/ROOT.ML"; will work as intended *unless* there happens to be a file 'first.ML' in the current directory. In my view, this is a rather obscure error condition with great potential for accidental surprises.
The current implementation at least has a simple specification. Also, it is not at all uncommon to interpret paths relative to the current working directory; e.g., bash does the same.
What may be missing in SML is a way to determine the name and path of the file that is being 'used.'
That's a very good idea. I wasn't happy about the solution I'd proposed and having a way of getting the file name is a much better way of doing it. I've modified the NestedUse branch to revert the previous change and added PolyML.getUseFileName: unit -> string option This returns the name of the file currently being "used", if there is one.
David
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
tjark.weber＠it.uu.se