Re: [isabelle-dev] Extracting dependencies from theory headers
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 of the sources for this long standing issue. ;-) 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 directory or load path can be discontinued eventually, but user theories have to be adapted a bit. Sounds entirely reasonable to me. AFP/00b2b6716ed8 still has approximately 200 files that are located via the secondary search path, as can be seen by grepping for that text the log files. Is anyone in particular working on that? Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
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 directory or load path can be discontinued eventually, but user theories have to be adapted a bit. What do you intend as the replacement of the load path? For things like HOL/Library or the AFP, named roots (i.e. paths like AFP:Abstract-Rewriting/Abstract_Rewriting) could do the trick, but I don't see what is wrong about a properly implemented load path (i.e. paths not stored in images; without the relative path naming anomalies I outlined above; maybe distinguishing between references relative to the master_dir or to the load path, like '#include ...' and '#include ...' in C). Absolute paths like you introduced in 64cd30d6b0b8 only work for core Isabelle, not for the AFP. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
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 master_dir change to the enclosing directory of the theory being imported? Thanks, -john On Dec 30, 2010, at 5: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 of the sources for this long standing issue. 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 directory or load path can be discontinued eventually, but user theories have to be adapted a bit. In Isabelle/00b2b6716ed8 the legacy status of the load path feature is made explicit. I have also cleared out the Isabelle distribution already. AFP/00b2b6716ed8 still has approximately 200 files that are located via the secondary search path, as can be seen by grepping for that text the log files. Makarius smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
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 to the enclosing directory of the theory being imported? Yes, the master directory changes accordingly. This is what I meant with the sentence below: On Dec 30, 2010, at 5:17 AM, Makarius wrote: the master directory, which is the location of the enclosing theory file when traversing the import graph. Here is also the ML version of it: http://isabelle.in.tum.de/repos/isabelle/file/00b2b6716ed8/src/Pure/Thy/thy_info.ML#l276 The idea is that resources are references relatively to each theory node, without any further complications getting in between. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
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 relative path in an imports or uses declaration? [...] In principle the relatively recent master path concept should solve all that, but its needs to be done right once and for all in the Scala layer. The add_path stuff should disappear at some point, with the usual delay in deleting old features. I did some tests to see how this master path concept works (by loading theories with convoluted imports in isabelle tty). My current understanding is as follows: For a path P, let name(P) be the last component of the past and base(P) the remaining components. - For each theory file, its master directory is the directory, the theory file is located in. - When theory A imports theory B, then Isabelle searches (1) master_dir(A)/B (2) current_dir/name(B) (3) $LOAD_PATH/name(B) (for some load paths, includes e.g. Library for HOL) (If I read the code correctly, (2) belongs to (3), as current_dir is part of the load path). Is this understanding correct? While I agree with (1), I'm a bit sceptical about (2) and (3). For one, it seems strange to drop base(B) in this cases -- is this intentional? One should either use B here (or perhaps drop (2) and (3) completely, if B is not just a theory name). 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. Greetings, Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
[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 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 relative path in an imports or uses declaration? [...] In principle the relatively recent master path concept should solve all that, but its needs to be done right once and for all in the Scala layer. The add_path stuff should disappear at some point, with the usual delay in deleting old features. I did some tests to see how this master path concept works (by loading theories with convoluted imports in isabelle tty). My current understanding is as follows: For a path P, let name(P) be the last component of the past and base(P) the remaining components. - For each theory file, its master directory is the directory, the theory file is located in. - When theory A imports theory B, then Isabelle searches (1) master_dir(A)/B (2) current_dir/name(B) (3) $LOAD_PATH/name(B) (for some load paths, includes e.g. Library for HOL) (If I read the code correctly, (2) belongs to (3), as current_dir is part of the load path). Is this understanding correct? While I agree with (1), I'm a bit sceptical about (2) and (3). For one, it seems strange to drop base(B) in this cases -- is this intentional? One should either use B here (or perhaps drop (2) and (3) completely, if B is not just a theory name). 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
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 a bit of confusion every time new users come in. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
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 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 relative path in an imports or uses declaration? - Related to the above: Dynamic load path modifications via add_path (as e.g. in HOL/Plain.thy) are a show-stopper, since they make it impossible to see what an Import refers to just by looking at headers. These would have to be replaced by something static, possibly a property of the session. Question: What are typical uses of add_path, other than the two instances in the current distribution (which set the library path, once for HOL and once for HOLCF)? After our very brief excursion into distributed make and queue management last year, the main new aspect from this year was http://hudson-ci.org/ Did anybody take a look at that? At least the website looks nice and simple. It is all JVM-based and seems to support Mercurial projects, too. I looked at it, but I found the design fairly inflexible. Its Mercurial support is limited to testing the tipmost revision when it comes in. Aggregation is nice (weather icons etc.), but all data seems to be time-indexed and not revision-indexed. It could be a replacement for the current isatest if somebody manages to set it up properly. But it will not do any of the following: - developer-initiated tests of unpublished changes - automatic bisects - multi-repository compatibility tracking (Isabelle vs. AFP) Florian recently spent some time with our own testing tool, which is now in a better state. I still hope that this becomes reality in the not-too-distant future. But this is another story. Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Extracting dependencies from theory headers
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 format. I also remember that Makarius already had the important ingredients for such a tool. How far is it to get this working from the present state? I am asking because Lars, Florian and I had this discussion again today. If we had such a tool, we would actually be willing to spend some time trying to replace the user-written (rather: copied) IsaMakefiles in the AFP with a single generated one. (Lars seems to be a make expert, and he had some realistic ideas on simplifying the whole setup). In particular, this would allow parallel builds of the AFP using make -j. Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Extracting dependencies from theory headers
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 format. I also remember that Makarius already had the important ingredients for such a tool. That was the state last winter: relatively robust parsing of headers (which is surprisingly difficult to get right due to strange 16bit chars on the JVM) and some rudiments of session management. Here are some examples for the isabelle scala toplevel: import isabelle._ val system = new Isabelle_System val header = new isabelle.Thy_Header(system.symbols) header.read(system.platform_file(~~/src/HOL/HOL.thy)) val manager = new Session_Manager(system) manager.component_sessions() The enumeration of component sessions depends on session.root files sprinkled in the relevant directories. Right now touch session.root will do the trick, because the content is not processed at all. I am asking because Lars, Florian and I had this discussion again today. If we had such a tool, we would actually be willing to spend some time trying to replace the user-written (rather: copied) IsaMakefiles in the AFP with a single generated one. (Lars seems to be a make expert, and he had some realistic ideas on simplifying the whole setup). In particular, this would allow parallel builds of the AFP using make -j. Last winter my plan was to generate make files and let some of the many variants of make do the job, not just GNU make -j also some of these distributed make systems around. In the meantime, I have mentally moved away from make more and more: it comes with a huge legacy (compatibility issues, inherent limitations like lack of support for spaces or unicode in file names, absence of make on most end-user systems etc.) These problems are not relevant for administrative tasks for AFP, of course. Presently my main concern is to get the interactive session management for Isabelle/Scala right, by a fully internalized process management. I have already reworked the basic process wrapper several times, and merely need to add existing parallel processing facilities on top (using threads or actors as usual). I wanted to have that in fall, but it is probably going to be around Christmas again. The lack of interactive session management is one of the main showstoppers for realistic applications of Isabelle/jEdit right now. Ultimately, the division of batch mode vs. interaction should disappear altogether, but this could take quite some time. So reworking batch mode independently could make some sense. After our very brief excursion into distributed make and queue management last year, the main new aspect from this year was http://hudson-ci.org/ Did anybody take a look at that? At least the website looks nice and simple. It is all JVM-based and seems to support Mercurial projects, too. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
