Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] using files

Email Gateway (Aug 18 2022 at 09:43):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
I find that sometimes (unpredictably) "use"ing a file uses the "wrong"
file, for example in the src/HOL directory,

ThyLoad.show_path();

val it = ["."] : string list

Library.pwd () ;

val it = "/home/users/jeremy/Isabelle2005/src/HOL" : string

ThyInfo.use "ROOT.ML"; (* uses Pure/ROOT.ML *)

What exactly does ThyInfo.use do to decide what file to use?

thanks,

Jeremy

Email Gateway (Aug 18 2022 at 09:44):

From: Stefan Berghofer <berghofe@in.tum.de>
Jeremy Dawson wrote:
The file name supplied as an argument to the use command is interpreted
relative to the location of the theory last loaded. For example, if the
theory Thy1 imports a theory Thy2 located in subdirectory Subdir via

theory Thy1
imports "Subdir/Thy2"

then all use commands in *.ML files loaded by theory Thy2 refer to the
files in directory Subdir, and not in the directory containing Thy1.
If use seems to act strangely, then this is probably caused by the
the current context (which you can inspect via "the_context()") being
set to the "wrong" theory.

Greetings,
Stefan

Last updated: May 03 2024 at 04:19 UTC