Email Gateway (Aug 18 2022 at 15:55): Email Gateway (Aug 18 2022 at 15:55):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I just tried this and it worked, but only after I made sure I start i3p
within the directory of the .thy. It seems that ".." is relative to the
current working directory, not to the currently processed theory. Is
that intentional?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:07):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi!
is there a way of telling Isabelle where to search for THY files? From
the error message in PG-Emacs when trying to load a non-existing THY
file, I get that the standard search is "." and
"$ISABELLE_HOME/src/HOL/Library". I would like to extend this list.
The reason is that we have 3 entries in the AFP which our development is
based on (currently we have local copies of the corresponding THY
files). To me, it would seem as an overkill, if I had to incrementally
construct heap images for
1) HOL-First-Entry
2) HOL-First-and-Second-Entry
3) HOL-First-and-Second-and-Third-Entry
and then use 'HOL-First-and-Second-and-Third-Entry instead' of 'HOL'.
What do you think? How do other users that base their work on AFP
entries, handle such situations? Andreas? ;)
cheers
chris
Email Gateway (Aug 18 2022 at 16:07):From: Tobias Nipkow <nipkow@in.tum.de>
You can refer to theories in other AFP entries simply by writing
imports "../other-article-name/theory-name"
This is the standard way of doing it.
Tobias
Christian Sternagel schrieb:
Email Gateway (Aug 18 2022 at 16:07):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Sep 16, 2010 at 5:45 AM, Christian Sternagel
<christian.sternagel@uibk.ac.at> wrote:
Hi!
is there a way of telling Isabelle where to search for THY files? From the
error message in PG-Emacs when trying to load a non-existing THY file, I get
that the standard search is "." and "$ISABELLE_HOME/src/HOL/Library". I
would like to extend this list.
In src/HOL/Plain.thy, you'll find the following line:
ML {* path_add "~~/src/HOL/Library" *}
You can add similar lines to your own theory files if you want to add
other directories to the search path. This one uses "~~" and so is
relative to $ISABELLE, but I think absolute paths should also work.
The reason is that we have 3 entries in the AFP which our development is
based on (currently we have local copies of the corresponding THY files). To
me, it would seem as an overkill, if I had to incrementally construct heap
images for
1) HOL-First-Entry
2) HOL-First-and-Second-Entry
3) HOL-First-and-Second-and-Third-Entry
and then use 'HOL-First-and-Second-and-Third-Entry instead' of 'HOL'.
It is a real shame that building custom heap images is so difficult. I
agree that having to build N heap images in sequence just to use N
different libraries at once is overkill. A nicer solution would be to
have a tool where you could say "give me a heap image with libraries
X, Y, and Z" and it would compile one for you in one step.
Unfortunately, the current Isabelle tools are based on an assumption
of one-heap-image-per-directory; we really need to move away from
that.
What do you think? How do other users that base their work on AFP entries,
handle such situations? Andreas? ;)cheers
chris
Question from Isabelle newbie: "This AFP library looks interesting;
how do I install it?" My shameful response is that by far the easiest
way to use an AFP library is to copy all the files into a directory
with all your own theory files. I know that this doesn't scale well if
you want to use more than one AFP library at once. You could use
separate directories and relative paths as Tobias suggests, but as
long as we have a flat theory namespace this doesn't really scale
either. (Question for the AFP maintainers: With about 80 AFP entries
now, do they all use distinct theory names? Is this something that you
should be worried about?)
Being able to download and use other people's Isabelle libraries (AFP
entries in particular) is very important, in my opinion, and the
current situation is unacceptable. I think that having a proper way to
"install" third-party Isabelle libraries would bring significant
benefits to our research community, making it much easier for people
to collaborate and build upon each other's work.
I really hope that most of the developers will continue to think about
how we can do this better.
Thanks, Chris, for bringing this issue to everyone's attention.
Email Gateway (Aug 18 2022 at 16:07):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Chris,
JinjaThreads, which I am working on, also builds on three other AFP entries (Coinductive, FinFun and Jinja/DFA) and HOL-Word. The JinjaThreads theories in the AFP use the import system with relative paths explained by Tobias and use the HOL-Word heap.
Gerwin suggested to me that I do not build incremental heaps (HOL, HOL-Word, HOL-Word-Coinductive, HOL-Word-Coinductive-FinFun, ...), but rather pick one of them (HOL-Word) as the basis and load the other's theories on demand. This way, while building JinjaThreads, Isabelle loads also the other AFP entries again.
For my everyday development on JinjaThreads I have given up on building images of the other AFP entries and working with them because I update my Isabelle version to the latest repository snapshot every two or three days. So, I would have to rebuild these heap images each time then. Instead, I have organised my local directory structure to match the AFP's. To get to work quickly, I simply load these base theories with the "skip proof" option enabled, which is fairly fast.
Andreas
Email Gateway (Aug 18 2022 at 16:07):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi,
thnx for the many answers!
@Tobias: between the AFP entries themselves I do exactly what you
recommended.
However, the whole setup is more like Andreas described: n AFP entries
(currently 3, but I hope there are more to come) which we want to use in
our local development.
I do not particularly like the solution with adapting my local directory
structure. My current try is to have a local AFP.ML (see attachment)
adding the paths (to the local copy of the AFP hg-repo) and loading the
desired theories and then building a heap file
isabelle usedir -b -f AFP.ML HOL HOL-AFP
to work on. This almost works (and in our case the AFP entries are not
very big, hence creating the heap file is fast), only that there are
some THY files in AFP entries that have the same name as local THY
files... and this breaks everything. In the current situation it will be
easy to replace one file by a differently named one, but in general I
totally agree with Brian that the flat name space is... how to say...
not excessively nice.
cheers
chris
On 09/17/2010 08:28 AM, Andreas Lochbihler wrote:
Hi Chris,
The reason is that we have 3 entries in the AFP which our development is based on (currently we have local copies of the corresponding THY files). To me, it would seem as an overkill, if I had to incrementally construct heap images for
1) HOL-First-Entry
2) HOL-First-and-Second-Entry
3) HOL-First-and-Second-and-Third-Entry
and then use 'HOL-First-and-Second-and-Third-Entry instead' of 'HOL'.What do you think? How do other users that base their work on AFP entries, handle such situations? Andreas? ;)
JinjaThreads, which I am working on, also builds on three other AFP entries (Coinductive, FinFun and Jinja/DFA) and HOL-Word. The JinjaThreads theories in the AFP use the import system with relative paths explained by Tobias and use the HOL-Word heap.
Gerwin suggested to me that I do not build incremental heaps (HOL, HOL-Word, HOL-Word-Coinductive, HOL-Word-Coinductive-FinFun, ...), but rather pick one of them (HOL-Word) as the basis and load the other's theories on demand. This way, while building JinjaThreads, Isabelle loads also the other AFP entries again.For my everyday development on JinjaThreads I have given up on building images of the other AFP entries and working with them because I update my Isabelle version to the latest repository snapshot every two or three days. So, I would have to rebuild these heap images each time then. Instead, I have organised my local directory structure to match the AFP's. To get to work quickly, I simply load these base theories with the
"skip proof" option enabled, which is fairly fast.
well ^that sounds interesting... <whispering>how do I activate
it?</whispering>Andreas
AFP.ML
Email Gateway (Aug 18 2022 at 16:07):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Chris,
In the "Skip proof"-mode, Isabelle skips all proofs, but not the definitions, context switches, attribute declarations, etc, i.e. the latter take still their time to be processed.
Another option to get started quickly is to use writeable heaps, where you can start right where you had stopped before. I used to work with these, but my heaps got so large that shutting down Isabelle and writing the heap back to the disk exceeded all emacs timeouts. Makarius might be able to tell you more about writeable heaps.
Andreas
Email Gateway (Aug 18 2022 at 16:08):From: Makarius <makarius@sketis.net>
These persistent heap images used to be very commonplace until everybody
started using Proof General, because the basic usage of isabelle-process
was forgotten. The Isabelle system explains this in section 1.2 with a
small example near the end.
Proof General makes it traditionally a bit hard to work with the result,
also due to the default time out -- it can be changed on the Proof General
side using one of these huge option menus, or better by injecting some
elisp into $HOME/.emacs like this:
(custom-set-variables '(proof-shell-quit-timeout 45))
Makarius
Last updated: Apr 19 2024 at 04:17 UTC