Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Sat, 18 Aug 2012, Florian Haftmann wrote: For the record: I did not know that Tjark had conversed with Florian privately before. This removes the main accusation on his http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was looking like he was seizing control of the draft started by Florian. The email reads (in German): ich würde vorschlagen, dass ich Admin/download_components so modifiziere, dass das Script Admin/components parsed (ähnlich wie in init_components), um die herunterzuladenden Komponenten zu bestimmen. Spricht aus deiner Sicht etwas dagegen? das Skript muss auch in der Lage sein, Komponenten der Vergangenheit runterzuladen. D.h. es würde über einen schalter -c/--current gehen, der dann einfach die aktuelle Liste runterlädt (oder vielleicht vorher noch die bereits vorhandenen Komponenten in ISABELLE_COMPONENTS noch davon wegnimmt?). Ansonsten würden nach wie vor die explizit angegebenen Komponenten runtergeladen. Ansonsten bleiben die Punkte, die bereits auf der Mailingliste genannt wurden: * curl statt wget * verschieben nach Admin/lib/Tools/download_components, um ein Tool der Admin-Komponente draus zu machen, und das Skript entsprechend anzupassen. In this case, I did not follow the rule I normally impose on myself to redirect any generic Isabelle issue to one of the mailing lists, this was my fault. Yes, I accept part as a proof, and offer my apologies both to Tjark and Florian in this respect. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
For the record: > I did not know that Tjark had conversed with Florian privately before. > This removes the main accusation on his > http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was > looking like he was seizing control of the draft started by Florian. The email reads (in German): >> ich würde vorschlagen, dass ich Admin/download_components so >> modifiziere, dass das Script Admin/components parsed (ähnlich wie in >> init_components), um die herunterzuladenden Komponenten zu bestimmen. >> Spricht aus deiner Sicht etwas dagegen? > > das Skript muss auch in der Lage sein, Komponenten der Vergangenheit > runterzuladen. D.h. es würde über einen schalter -c/--current gehen, > der dann einfach die aktuelle Liste runterlädt (oder vielleicht vorher > noch die bereits vorhandenen Komponenten in ISABELLE_COMPONENTS noch > davon wegnimmt?). Ansonsten würden nach wie vor die explizit > angegebenen Komponenten runtergeladen. > > Ansonsten bleiben die Punkte, die bereits auf der Mailingliste genannt > wurden: > * curl statt wget > * verschieben nach Admin/lib/Tools/download_components, um ein Tool der > Admin-Komponente draus zu machen, und das Skript entsprechend anzupassen. In this case, I did not follow the rule I normally impose on myself to redirect any generic Isabelle issue to one of the mailing lists, this was my fault. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Fri, 17 Aug 2012, Tobias Nipkow wrote: Am 17/08/2012 21:51, schrieb Christian Urban: On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: > Tjark, you have no business here. I assume something got here lost in translation. Otherwise, we should all make reasonable effort to welcome everybody on both, the isabelle-users and isabelle-dev lists. After all, we like to have plenty of users and plenty of developers for Isabelle; not like the GDR, which had a country, but in the end had no people. ;o) Thank you, Christian, spot on. The number of users and number of developers is off-topic here. I am not commenting further on this complex issue on this thread (you can open another if you want). Back to the main issue: I had some interesting conversations at the Isabelle workshop in Princeton. The tone of the isabelle mailing list is perceived as amusingly agressive by outsiders. I don't find it amusing, I find it aggarvating. Taking a dig at someone via a ceterum censeo in a signature is not helpful, but "You have no business here" is downright rude. This was indeed a hot outbreak on after a rather cool thread here: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-August/003011.html https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-August/003013.html https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-August/003021.html My unusually cool conclusion after Tjark still not quite understanding (even until now): > So I have to follow one more change to get the work done eventually. > This is not very productive. Can everybody please watch their language? I may be old fashioned, but saying "Please do not ... because ..." instead of "You have no business here" makes all the difference. As my grandmother, god bless her, used to say: "Der Ton macht die Musik". The tone was indeed a bit harsh at the end and on the wrong thread. I was referring to Tjarks's http://isabelle.in.tum.de/repos/isabelle/rev/ec82c33c75f8 after I've made several times clear that he should not engage in the ongoing work by Krauss/Haftmann/Wenzel on the component business. It is part of old Isabelle development wisdom that more than 2-3 people cannot work productively on a particular topic. I did not know that Tjark had conversed with Florian privately before. This removes the main accusation on his http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was looking like he was seizing control of the draft started by Florian. It is part of ancient Isabelle development tradition that places of activity by one person are not directly interfered by another one, until the dust has settled; and then it is often better to start some email thread than pushing further changes on top. Otherwise there would be a constant fear of people who are starting some intiatives that they cannot finish quickly enough before others meddle with it. This was also what my rather cool remark "The Isabelle repository is not a Wiki" was referring to (although German Wikipedia would not even allow such uncoordinated edits). Anyway, some concluding remarks on a hot thread on a hot day: * The isabelle-dev mailing list was started on my initiative, and I've tried to motivate people over several years to redirect the discussion of Isabelle internals from my personal mail address to the public mailing list. In the last year or so this has actually started to work, so that sometimes there are some actual technical discussions, not just opinions. And people who are not directly engaged in some topic can see what is happening, without secret decisions happening in the back room. * I hope that we will all make an effort to continue making isabelle-dev the place where stuff really happens. * Mail signature lines suck, but I will use one just this time. Makarius -- Do not meddle in the affairs of wizards, for they are subtle and quick to anger. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
Am 17/08/2012 21:51, schrieb Christian Urban: > > > On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: > > Tjark, you have no business here. > > I assume something got here lost in translation. > Otherwise, we should all make reasonable effort > to welcome everybody on both, the isabelle-users > and isabelle-dev lists. After all, we like to have > plenty of users and plenty of developers for Isabelle; > not like the GDR, which had a country, but in the end > had no people. ;o) Thank you, Christian, spot on. I had some interesting conversations at the Isabelle workshop in Princeton. The tone of the isabelle mailing list is perceived as amusingly agressive by outsiders. I don't find it amusing, I find it aggarvating. Taking a dig at someone via a ceterum censeo in a signature is not helpful, but "You have no business here" is downright rude. Can everybody please watch their language? I may be old fashioned, but saying "Please do not ... because ..." instead of "You have no business here" makes all the difference. As my grandmother, god bless her, used to say: "Der Ton macht die Musik". Tobias > > If you want to propose changes to the Isabelle repository, you can send > > them the via email as hg changeset. > > > > > >Makarius > > ___ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Fri, 2012-08-17 at 21:57 +0200, Makarius wrote: > Tjark has violated a bit too many rules of conduct in too short time, > basically abusing his historic administrator privileges on the > Isabelle repository. In the past week, I made minor modifications to a two-week-old maintenance script of Florian (having asked him for permission off-list beforehand), implementing features that you had suggested yourself. I appreciate that your latest, much more comprehensive revision of the components business has already made this script obsolete. And I fixed a completely irrelevant typo elsewhere. I apologize if these commits troubled you in any way. But to be perfectly honest, I don't really see the abuse. I tried hard not to break anything, and can assure you that any violation of unwritten rules of conduct was entirely unintentional. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Fri, 17 Aug 2012, Christian Urban wrote: On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: > Tjark, you have no business here. I assume something got here lost in translation. Otherwise, we should all make reasonable effort to welcome everybody on both, the isabelle-users and isabelle-dev lists. After all, we like to have plenty of users and plenty of developers for Isabelle; not like the GDR, which had a country, but in the end had no people. ;o) Tjark has violated a bit too many rules of conduct in too short time, basically abusing his historic administrator privileges on the Isabelle repository. Submission by sending changesets or pull request is always open to everyone, and to the discretion of the responsible maintainer what to do with it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: > Tjark, you have no business here. I assume something got here lost in translation. Otherwise, we should all make reasonable effort to welcome everybody on both, the isabelle-users and isabelle-dev lists. After all, we like to have plenty of users and plenty of developers for Isabelle; not like the GDR, which had a country, but in the end had no people. ;o) Christian > > If you want to propose changes to the Isabelle repository, you can send > them the via email as hg changeset. > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
Tjark, you have no business here. If you want to propose changes to the Isabelle repository, you can send them the via email as hg changeset. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Fri, 2012-08-17 at 15:15 +0200, Makarius wrote: > If you need shortcuts, use existing shell alias or scripting facilities. > You can even make your private Isabelle tools by augmenting ISABELLE_TOOLS > and *not* pushing anything like that on the official repository. Sure, but wouldn't the same argument apply to ISABELLE_BUILD_OPTIONS? After all, one could use "isabelle build -o ..." instead. I guess I don't quite see why on the one hand you consider it useful to provide a convenient way to set default options for isabelle.Build, while on the other hand you don't think it would be an improvement if the same mechanism also worked for options to "isabelle build". Are end-users even aware of the distinction (and should they have to be)? Anyway, your call. > > Ceterum censeo: Isabelle needs an issue tracker. > > I count this as trolling on this mailing list. It is not my intention to emotionally upset you (or anyone else). A signature seemed sufficiently non-obtrusive to me. Many email clients automatically discard it at some point. In fact, I'd be happy to discuss the topic (although I doubt that you need me to argue the benefits of issue tracking for collaborative software development), to investigate trackers, or even to take on long-term maintenance. But any tracker only makes sense with a certain degree of developer acceptance. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Fri, 17 Aug 2012, Tobias Nipkow wrote: Am 17/08/2012 15:15, schrieb Makarius: I count this as trolling on this mailing list. We all have our pet peeves. Tjark can express that somewhere privately, not here on this mailing list. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
Am 17/08/2012 15:15, schrieb Makarius: > I count this as trolling on this mailing list. We all have our pet peeves. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
On Fri, 17 Aug 2012, Tjark Weber wrote: I had expected that ISABELLE_BUILD_OPTIONS would allow me to specify default options for the "isabelle build" tool, for instance "-v" for verbose output. None of the regular tools ever had such a feature, for usedir it was merely a historical accident. If you need shortcuts, use existing shell alias or scripting facilities. You can even make your private Isabelle tools by augmenting ISABELLE_TOOLS and *not* pushing anything like that on the official repository. In reality, ISABELLE_BUILD_OPTIONS are merely passed on to isabelle.Build, which has its own idea of valid options. There is in fact a much more versatile notion of "system options" behind that. It is not fully active yet, and the documentation not there yet. This is not a bug, but merely a consequence of what development of the repository version means: it is the construction area, where parts are fit together until something of decent quality can be shipped as official release again. Ceterum censeo: Isabelle needs an issue tracker. I count this as trolling on this mailing list. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options
Hi, I had expected that ISABELLE_BUILD_OPTIONS would allow me to specify default options for the "isabelle build" tool, for instance "-v" for verbose output. In reality, ISABELLE_BUILD_OPTIONS are merely passed on to isabelle.Build, which has its own idea of valid options. I would suggest that "isabelle build" treats ISABELLE_BUILD_OPTIONS similar to options passed on the command line, so that one could use all the options supported by "isabelle build" -- and not merely those supported by isabelle.Build -- in ISABELLE_BUILD_OPTIONS. Best regards, Tjark -- Ceterum censeo: Isabelle needs an issue tracker. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
> (BTW, in > Scala ambiguity after additional imports is treated as an error, and > causes the conflicting name entries to be canceled out.) I definitely like this! Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
> When I've seen the "complete_boolean_algebra" incident on the other > thread my first impulse was to check how far the wiring of the class > package wrt. the Isabelle document markup was. In principle the prover > can provide useful clues in non-intrusive ways here, if done right. > E.g. in Isabelle/jEdit one can hover over the text with COMMAND/CONTROL > to ask "What is this?" and often get useful feedback already. > > Unfortunately, the class package is still in a confusing state here, so > I did not even put it on the list of things to be done, because it is > just another instance of similar ongoing reforms, and there are so many > really pressing things in the pipeline. (Quite a bit has happened here > already, like purging the name space module from historic cruft one more > time, and assembling all syntax layers clearly in one place.) I dimly remember that one day I had planned to return to the class package (awaiting a trigger which in fact has not fired until now). I guess the problem is somehow about dealing with bindings the right way to preserve markup which has to be added, but I am far from understanding what actually has to be amended. Maybe at a certain time you can give me further hints. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
I'm not sure that a warning is necessary. There were multiple factors in my confusion. One, clearly, was that type classes (like everything else) had always been global, and I never expected them to be localised. Two, I expected a type class such as complete_boolean_algebra to be canonical: the one defined in Main should be the right one, so any modification should be out of the question. I haven't actually studied the two definitions to see which one is really correct; getting these proofs working again is difficult enough. But either the one in Main needs to be corrected, or the local one needs to be given a more appropriate name. Larry On 22 Aug 2011, at 21:54, Makarius wrote: > When I've seen the "complete_boolean_algebra" incident on the other thread my > first impulse was to check how far the wiring of the class package wrt. the > Isabelle document markup was. In principle the prover can provide useful > clues in non-intrusive ways here, if done right. E.g. in Isabelle/jEdit one > can hover over the text with COMMAND/CONTROL to ask "What is this?" and often > get useful feedback already. > > Unfortunately, the class package is still in a confusing state here, so I did > not even put it on the list of things to be done, because it is just another > instance of similar ongoing reforms, and there are so many really pressing > things in the pipeline. (Quite a bit has happened here already, like purging > the name space module from historic cruft one more time, and assembling all > syntax layers clearly in one place.) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
On Mon, 22 Aug 2011, Brian Huffman wrote: Isabelle prints out warning messages whenever anyone declares a duplicate simp rule, intro rule, etc. It would be nice if Isabelle would print a similar warning whenever a definition reuses a name that is already in scope in the current context. For example, if a theory defines a class like this... class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra ...and a class called "complete_boolean_algebra" is already in scope, then a warning message ought to be printed. Such a warning message would be useful for constant names, lemma names, etc. as well. When I've seen the "complete_boolean_algebra" incident on the other thread my first impulse was to check how far the wiring of the class package wrt. the Isabelle document markup was. In principle the prover can provide useful clues in non-intrusive ways here, if done right. E.g. in Isabelle/jEdit one can hover over the text with COMMAND/CONTROL to ask "What is this?" and often get useful feedback already. Unfortunately, the class package is still in a confusing state here, so I did not even put it on the list of things to be done, because it is just another instance of similar ongoing reforms, and there are so many really pressing things in the pipeline. (Quite a bit has happened here already, like purging the name space module from historic cruft one more time, and assembling all syntax layers clearly in one place.) Anyway, your above idea of "warning whenever a definition reuses a name that is already in scope in the current context" does not really remind me of how this works internally. What means "name" here? E.g. a package defining some "induct" rule is perfectly right to do so in the presence of another "induct", as long as additional name qualification makes things clear to the system and the user. We have reasonably well-established concepts of "binding", "naming", and "morphisms" on bindings. Any new feature somehow needs to fit smoothly into the picture. Also note that a special twist is the name space merge that happens at theory import time: independent specifications can silently cause a conflicting situation in the application context. What could work, and is on my list for a long time already, is to give some feedback in situations where *ambiguity* occurs in name space resolution. This would also follow the intention behind the names_unique (formerly unique_names) option, only that the prover would show such spots spontaneously and non-intrustively whenever they appear in input or output, both in defining and referencing positions. (BTW, in Scala ambiguity after additional imports is treated as an error, and causes the conflicting name entries to be canceled out.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
Hello everyone, Isabelle prints out warning messages whenever anyone declares a duplicate simp rule, intro rule, etc. It would be nice if Isabelle would print a similar warning whenever a definition reuses a name that is already in scope in the current context. For example, if a theory defines a class like this... class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra ...and a class called "complete_boolean_algebra" is already in scope, then a warning message ought to be printed. Such a warning message would be useful for constant names, lemma names, etc. as well. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature request
On Tue, 7 Dec 2010, Thomas Sewell wrote: I was recently reminded of one of the things on my wish-list for Isabelle: a "make -k" mode in which the system continues for as long as possible and reports as many errors as possible, rather than halting after the first one. I think this would be generally useful to Isabelle users, but it would be especially useful when fiddling with tactics that are already in use. The usual approach is to try several variations aiming to minimise incompatibility, but there's no easy way to get an idea of the level of incompatibility without repairing the first few errors. To clarify, I'd like to be able to type something like "isabelle testmake (arguments)", and the system would run through the same sources as on an "isabelle make", only errors in proof scripts would be suppressed. Once everything is loaded and any image to be saved is saved, the system would print all the errors encountered at the end of the log. It occurred to me how to implement this feature using the existing parallel apparatus. What's needed is a way to defer an exception raised in computing a future object forever, leaving the exception in the future and allowing all other independent work to conclude. Since parallel proofs are executed in future calculations that never need to be joined (unless someone is inspecting proof terms), this could provide a solution. I had a go at doing this myself but got nowhere. Does anyone familiar with the concurrency code think this is possible? The strictly sequential treatment of errors is indeed an artifact of the obsolete TTY model. I am still working hard on its replacement in Isabelle/Scala and Isabelle/jEdit. Just some weeks ago, for the first Isabelle course with the new interface, I also made some small improvements concerning recovery after errors, although not as seriously as is required here. The whole theory loading process is approching a substantial reform. During the summer I managed to remove lots of historical baggage. The next step is to unify its parallel scheduler with the new interactive document model. While I'm putting things on the concurrency wish-list, I have one more: a limit on the length of the work queue. The reason I request this is that some of our large sessions (1-2 hrs) seem to perform poorly with parallelism, and I suspect part of the problem is that the problem parsing thread is getting so far ahead of the problem-solving threads that the majority of the contexts and problems from the session are living in memory waiting to be solved. I think the way you would implement this is by switching mode once the work queue is large enough and dropping any threads attempting further forks to the bottom of the priority list. Does anybody else think this might be a good idea? I guess I should try to conjure up an example session which demonstrates the performance problems. Did you check my publications on that? There are some fine-grained charts of the future scheduler state, with some explanations how they were produced. Even that limited information can help in isolating bottle necks. There is always more than one surprise awaiting ... Of course, publicly available proofs are easier to profile, but that is a different story. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Feature request
Hello Isabelle developers. I was recently reminded of one of the things on my wish-list for Isabelle: a "make -k" mode in which the system continues for as long as possible and reports as many errors as possible, rather than halting after the first one. I think this would be generally useful to Isabelle users, but it would be especially useful when fiddling with tactics that are already in use. The usual approach is to try several variations aiming to minimise incompatibility, but there's no easy way to get an idea of the level of incompatibility without repairing the first few errors. To clarify, I'd like to be able to type something like "isabelle testmake (arguments)", and the system would run through the same sources as on an "isabelle make", only errors in proof scripts would be suppressed. Once everything is loaded and any image to be saved is saved, the system would print all the errors encountered at the end of the log. It occurred to me how to implement this feature using the existing parallel apparatus. What's needed is a way to defer an exception raised in computing a future object forever, leaving the exception in the future and allowing all other independent work to conclude. Since parallel proofs are executed in future calculations that never need to be joined (unless someone is inspecting proof terms), this could provide a solution. I had a go at doing this myself but got nowhere. Does anyone familiar with the concurrency code think this is possible? While I'm putting things on the concurrency wish-list, I have one more: a limit on the length of the work queue. The reason I request this is that some of our large sessions (1-2 hrs) seem to perform poorly with parallelism, and I suspect part of the problem is that the problem parsing thread is getting so far ahead of the problem-solving threads that the majority of the contexts and problems from the session are living in memory waiting to be solved. I think the way you would implement this is by switching mode once the work queue is large enough and dropping any threads attempting further forks to the bottom of the priority list. Does anybody else think this might be a good idea? I guess I should try to conjure up an example session which demonstrates the performance problems. As always, please tell me if I'm completely wrong about the way the system works. Yours, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
