Email Gateway (Aug 18 2022 at 09:53): Email Gateway (Aug 18 2022 at 09:53):From: Roger Bishop Jones <rbj01@rbjones.com>
Thanks for the responses from Florian and Jeremy on extending the
library load path.
I am at present trying to decide how to reconcile my present web
site build system with the Isabelle build system.
I would like any work I do with Isabelle to conform to the way of
delivering contributions which is used in the isabelle archive
but I don't understand well enough how this works.
Though there are detailed instructions on how to make a
submission, I have found no instructions on how to install one.
The archive documentation encourages contributors to build on the
contributions in the archive, but its not clear how to do that.
I don't have a problem building the contribs which I have
downloaded, but I don't then see how to use them without
inserting a site specific load path adjustment into my own
theories. (and its not clear that that would work)
Can anyone explain this to me?
Roger Jones
Email Gateway (Aug 18 2022 at 09:54):From: Makarius <makarius@sketis.net>
Batch sessions usually include something like this in ROOT.ML (but not in
loaded theories or other ML files):
with_path "..." use_thy "Foobar";
(modify load path while loading this theory)
or
add_path "..."; (modify load path globally)
The latter can be compiled into a derived image, say MyHOL, in order to
have this available in interactive sessions, too.
There are many more ways to hack the load path, but personally I am never
that ambitious to stretch the system that far. Basically the whole
concept of having a load path is already wrong. At some point it will get
replaced by proper session specifications (uniformly for batch mode and
interactive development).
Makarius
Email Gateway (Aug 18 2022 at 09:54):From: Roger Bishop Jones <rbj01@rbjones.com>
On Tuesday 07 November 2006 10:43, Makarius wrote:
Batch sessions usually include something like this in ROOT.ML
(but not in loaded theories or other ML files):with_path "..." use_thy "Foobar";
(modify load path while loading this theory)or
add_path "..."; (modify load path globally)
Thanks, I think I'm going with:
add_path "../Theoryname";
as needed in ROOT.ML files, since that is site independent
assuming only that the archive theories are all unpacked in the
same directory (is that what "contrib" is for?)
There are many more ways to hack the load path, but personally
I am never that ambitious to stretch the system that far.
I'm only looking for something that works (unifomly with the
other archive theories)!
Basically the whole concept of having a load path is already
wrong. At some point it will get replaced by proper session
specifications (uniformly for batch mode and interactive
development).
That would be nice.
Thanks again,
Roger Jones
Email Gateway (Aug 18 2022 at 09:55):From: Makarius <makarius@sketis.net>
The contrib directory is just the default place to absorb any
site-specific additions that are not part of the actual Isabelle
distribution. You are free to use it in any way you like.
Makarius
Email Gateway (Aug 18 2022 at 09:55):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, I think I'm going with:
add_path "../Theoryname";
as needed in ROOT.ML files, since that is site independent
assuming only that the archive theories are all unpacked in the
same directory
Correct. Except that you mean "name-of-contribution", i.e. a directory
name, not "Theoryname".
I'm only looking for something that works (unifomly with the
other archive theories)!
It does. But beware that two contributions may (accidentally) contain
theories with the same name. If you add both paths, this may lead to the
wrong theory beeing loaded. Hence the whole concept is not perfect yet.
Tobias
Last updated: Nov 21 2024 at 12:39 UTC