Email Gateway (Aug 18 2022 at 09:53): Email Gateway (Aug 18 2022 at 09:53):From: Roger Bishop Jones <rbj01@rbjones.com>
I have failed to discover any way of adding directories to the
isabelle library load path.
Can anyone help me with this?
Roger Jones
Email Gateway (Aug 18 2022 at 09:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Roger,
you could try (in an Isar .thy file)
ML {* add_path "<my_path>" *}
Cheers
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 09:53):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Roger Bishop Jones wrote:
I have failed to discover any way of adding directories to the
isabelle library load path.Can anyone help me with this?
Roger Jones
Roger,
add_path ".." (as an ML command) used to do this.
At some time the behaviour of this became unpredictable (at some point,
changes you'd made to the path would get forgotten).
At the time I recall being told (in effect) that this wasn't a bug, it
was an (undocumented) feature.
If this is the problem you're having, try
(1) add_path in an ML file which is use'd, not loaded by use_thy
(this is what I do)
(2) ThyLoad.add_path (I suspect this might also work, though I can't
recall where I came across this idea and I never tried it out).
Hope this helps.
Jeremy
Last updated: May 03 2024 at 04:19 UTC