On 31/12/2010, at 12:17 AM, Makarius wrote:
On Wed, 22 Dec 2010, Gerwin Klein wrote:
I would think that only one search path is necessary, but I don't understand
what is meant by master_dir, I missed that part of the discussion.
This thread is getting almost as entangled as the history
On 30.12.2010 14:17, Makarius wrote:
Last summer I've made another round in clearing out the confusion,
working towards a stateless model based solely on the master directory,
which is the location of the enclosing theory file when traversing the
import graph. Thus the implicit use of current
Thanks Makarius, I believe that addresses my use-case.
Another question: If the user asks Isabelle to process theory A, and
theory A has statement
imports dir1/B
and theory B has statement
imports dir2/C
then will Isabelle look for theory C in dir1 or dir1/dir2 ?
In other words, does
On Thu, 30 Dec 2010, John Matthews wrote:
Another question: If the user asks Isabelle to process theory A, and
theory A has statement
imports dir1/B
and theory B has statement
imports dir2/C
then will Isabelle look for theory C in dir1 or dir1/dir2 ?
In other words, does master_dir change
On 19.11.2010 11:49, Makarius wrote:
On Fri, 19 Nov 2010, Alexander Krauss wrote:
- Relative paths are not resolved by the current simple parser. I
remember that there used to be some oddities in PG related to relative
paths. I am not sure what the situation is now. What is the meaning of
a
[I managed to lose the CC:header for the list, so here a copy of this
message with correct headers. Sorry for the noise :/]
On 19.11.2010 11:49, Makarius wrote:
On Fri, 19 Nov 2010, Alexander Krauss wrote:
- Relative paths are not resolved by the current simple parser. I
remember that there
On 22/12/2010, at 2:52 AM, Lars Noschinski wrote:
Furthermore, I would argue that current_dir should not be part of the
load_path while recursively loading dependencies. The only time current_dir
should be considered is when loading a theory file from the toplevel
Seconded. This causes quite
Makarius wrote:
Here are some examples for the isabelle scala toplevel:
[...]
Thanks, these are good pointers.
Unfortunately, this is (once again) harder than I thought. Here are the
issues/questions:
- Relative paths are not resolved by the current simple parser. I
remember that there used
Dear list, (and Makarius in particular :-) )
I remember some offline discussions last year about having an Isabelle
tool that extracts file dependencies from theory sources (probably
starting from some special session file, which specifies the root
theories) and outputs it in a simple textual
On Mon, 15 Nov 2010, Alexander Krauss wrote:
I remember some offline discussions last year about having an Isabelle
tool that extracts file dependencies from theory sources (probably
starting from some special session file, which specifies the root
theories) and outputs it in a simple textual
10 matches
Mail list logo
