Email Gateway (Aug 17 2022 at 14:49): Email Gateway (Aug 17 2022 at 14:49):From: Michael Norrish <Michael.Norrish@nicta.com.au>
I am implementing an Isar toplevel directive that takes a filename as
an argument. I'd like to interpret this as relative to the directory
containing the enclosing theory file, instead of the base directory of
the Isabelle session. (These two things can be different.)
Thanks,
Michael.
Email Gateway (Aug 17 2022 at 14:49):From: Makarius <makarius@sketis.net>
First of all note that actual theory values have no notion of the source
text or file-system location. You may still get something like this by
asking the theory loader, e.g. using Context.theory_name and
ThyInfo.loaded_files. The latter merely records file dependencies, but
the main thy source will show up as head element eventually. (The file
list may well be empty, e.g. in interactive composition of theory sources
without loading any files.)
Maybe this kind of peeking into theory loader internals can even be
avoided. The theory system does not really maintain qualified theory
names anyway. By use_thy "/foo/bar/MyTheory" or ``theory ... imports
"/foo/bar/MyTheory"" ...'' the system merely augments the load path
temporarily and then looks for "MyTheory.thy" as usual. This means when
processing a thy file one may assume its path is already included in the
lookup -- if it has been found then it must have been via the load path.
Any subsequent load operation (with base file names) will go through the
same procedure.
To make a long story short, just do something like ``use "myfile.ML"'' to
refer to auxiliary files within the same directory as the current thy
source.
Makarius
Email Gateway (Aug 17 2022 at 14:49):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Makarius writes:
Yes. In this case, I'm loading C files with a custom piece of code,
so I need to make my code as smart as "use".
Michael.
Email Gateway (Aug 17 2022 at 14:49):From: Makarius <makarius@sketis.net>
So maybe ThyLoad.check_file is what you want, e.g.:
ThyLoad.check_file NONE (Path.basic "Primes.thy");
(This example finds a file through the "$ISABELLE_HOME/src/HOL/Library"
load_path entry.)
Makarius
Last updated: May 03 2024 at 08:18 UTC