Re: [isabelle-dev] Isabelle/jEdit output panel
Stacking of tooltips is nice. Also that these stay open until they are closed explicitly is far more convenient than the previous behavior. A tiny remark: for linux (and I guess also windows) users, it is surprising to have icons on the top-left of a window, rather than top-right :D. I'm just saying. cheers chris On 10/05/2012 11:40 PM, Makarius wrote: On Fri, 21 Sep 2012, Makarius wrote: This also means that tooltips, hyperlinks etc. should now work the same for Output, just as for the input text. The next step will be to make tooltips and popups themselves use the same technology recursively. The latter is now addressed in Isabelle/a1bd8fe5131b, which uses the new Pretty_Tooltip everywhere for input or output. It also allows some stacking of tooltips: activating the formal link in one tooltip opens another. Thus a tooltip for type information can open another one for sort information on the displayed type variables, for example. Loss of focus or ESCAPE dispose such windows. Technically, this is a bit like computer game programming: one needs to play with GUI events until it works smoothly in the application. There are still some uneven situations here, notably the keyboard focus. 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] Isabelle/jEdit output panel
On 10/11/2012 08:35 AM, Christian Sternagel wrote: A tiny remark: for linux (and I guess also windows) users, it is surprising to have icons on the top-left of a window, ... not surprising for all users, e.g. Ubuntu has these icons on the top-left as well. rather than top-right :D. I'm just saying. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Graphview
Hi all, the recently established graphview IMHO has currently two disadvantages: * Misfit of node annotation size wrt. to the size of the full graphs – node annotations are not readable within a reasonable size coverage of the graph. * Does not scale well (e.g. class_deps from Main.thy). What are the plans for the next release? Graph browsing is a tool too vital that it can be set inoperative. Is there any chancing for improvements, or will there be a switch towards the classical browser alternatively? Cheers, 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] Shadowing of theorem names in locales
HOL-Probability (in Isabelle/bb5db3d1d6dd) and Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this patch. A surprising change is found in Markov_Models: We get an error when an assumption has the same name as a fact in the locale: locale loc begin lemma X: True .. lemma assumes X: X shows True ^- raises Duplicate fact declaration local.X vs. local.X Is this easily avoidable? I think this might confuse people and add a maintenance burden when one adds a fact to a locale with a popular name. - Johannes Am Mittwoch, den 10.10.2012, 16:51 +0200 schrieb Makarius: On Tue, 9 Oct 2012, Makarius wrote: On Sun, 7 Oct 2012, Florian Haftmann wrote: After some pondering I would argue that this should be forbidden: * (Complete) shadowing is a constant source of confusion. * Global interpretations are impossible then, since they would result in two global theorems with the same name. I've started some experiments with this idea and will report the empirical results soon ... After some detours I am now back on Isabelle/28e37eab4e6f. In principle, the last big reform of locale + interpretation name space prefixes has addressed the situation already, where each locale scope is locally strict, but composing several of them in locale expressions etc. works by mandatory or non-mandatory prefixes. Actual strictness checking is part of the underlying name space policy, when bindings are applied and react with some naming. The local context of the locale construction is particularly important here. It was merely a historical left-over that fact bindings were not checked strictly: (1) in distant past facts were never strict and totally un-authentic (2) the Isar proof body mode allows to override 'notes' as it does for 'fixes'. So with the ch-strict changeset applied to the critical spot of local notes, the namespace policy enforces the concentual locale scopes. Applying this in practice leads to many surprises about situations found in existing theory libraries, though. Some of the changsets leading up to Isabelle/28e37eab4e6f already sort this out. Some other ad-hoc changes are attached as ch-test here. With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1 the following sessions fail: BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module, HOL-Algebra, HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs, Markov_Models, Ordinal, Ordinary_Differential_Equations, Pi_Calculus, Presburger-Automata, PseudoHoops, Psi_Calculi, Refine_Monadic, Simpl, Slicing, Topology, Transitive-Closure-II, Valuation So the question if ch-strict can be activated soon is mainly a matter of library space. It is up to emerging volunteers to sort it out further. (For me it was interesting to see how Isabell/jEdit works on the JinjaThreads monster session. See also AFP/77f79b2076f1 of the result of investing 3GB for poly, 4GB for java, and quite a bit of CPU time and elapsed time.) 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] Hooks for postprocessing sessions!?
Hi Florian, this sounds similar to ideas that (Alex and) Lars had to allow find_theorems to search on all Isabelle sessions. As far as I know, they have an implementation for this feature in their shelf. Lukas On 10/11/2012 02:44 PM, Florian Haftmann wrote: Hi all, recently I had the idea to generate reports for all accessible Isabelle sessions containing e.g. * all constants (with types) declared in a session * all types declared in a session * all classes declared in a session * all theorems declared via »theorem« * ... The rationale is that this would allow for a quick analysis especially of the AFP to find out which generally useful »auxiliary« stuff is hidden there (e.g. http://afp.hg.sourceforge.net/hgweb/afp/afp/file/e9fa38f86b76/thys/Binomial-Heaps/SkewBinomialHeap.thy#l1643). Is there already feasible hook interface to hook in, e.g. in present.ML, or can this only be done by an ad-hoc patch? Cheers, Florian ___ 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] Graphview
Hi Florian, Thanks for your feedback. The main developer Markus Kaiser is giving a presentation next week and we will discuss further steps. Here's a part of a private German discussion with Makarius that explains how to switch back to the classical browser (in PG/Emacs). in http://isabelle.in.tum.de/repos/isabelle/rev/7529c77ee92e ist nun alles erstmal integriert. Einige Sachen funktionieren aber noch nicht so glatt, z.B. ein voller class_deps graph von HOL/Main. Das eine oder andere Detail habe ich möglicherweise auch kaputt gemacht. Man kann in isabelle tty oder emacs mit der print mode option -m graphview das neue Tool aktivieren, sonst wird wie bisher der alte browser verwendet. Das gilt einheitlich für alle commands die intern auf display_graph basieren. Isabelle/jEdit verwendet stets Graphview in einem eigenen Dockable Window -- auch wenn das noch nicht Produktionsqualität erreicht. Lukas On 10/11/2012 01:31 PM, Florian Haftmann wrote: Hi all, the recently established graphview IMHO has currently two disadvantages: * Misfit of node annotation size wrt. to the size of the full graphs -- node annotations are not readable within a reasonable size coverage of the graph. * Does not scale well (e.g. class_deps from Main.thy). What are the plans for the next release? Graph browsing is a tool too vital that it can be set inoperative. Is there any chancing for improvements, or will there be a switch towards the classical browser alternatively? Cheers, Florian ___ 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] Isabelle/jEdit output panel
On Thu, 11 Oct 2012, Christian Sternagel wrote: Stacking of tooltips is nice. Also that these stay open until they are closed explicitly is far more convenient than the previous behavior. A tiny remark: for linux (and I guess also windows) users, it is surprising to have icons on the top-left of a window, rather than top-right I've fine-tuned the behaviour several times in the past few days, so it is relevant to refer to lasting changeset ids as usual. The justification for the latter detail is here: changeset: 49727:2fe56b600698 user:wenzelm date:Sun Oct 07 16:15:31 2012 +0200 files: src/Tools/jEdit/src/isabelle_rendering.scala src/Tools/jEdit/src/pretty_tooltip.scala description: make buttons closer to original mouse position; Linux does not have any standards for placement of window control element, so I ignored that aspect above; the mouse movement was taken as decisive. I still get occasionally confused after trying to move the tooltip with its titel bar. There is also the confusion when the detached tooltip has become a jEdit dockable and the user tries to clone it: the result is perfectly correct wrt. the dockable window model, but still confusingly empty. Nonetheless, the basic functionality should work now without big surprises, like a tooltip stack that cannot be closed at all. (This is Isabelle/e3945ddcb9aa at the moment.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Graphview
On Thu, 11 Oct 2012, Florian Haftmann wrote: * Misfit of node annotation size wrt. to the size of the full graphs – node annotations are not readable within a reasonable size coverage of the graph. * Does not scale well (e.g. class_deps from Main.thy). I've made 1-2 rounds of refinements of the codebase already, and worked slowly towards these most imminent issues. (Presently at Isabelle/e3945ddcb9aa.) The class_deps non-scalability probably stems from the omission of the transitive reduction (Hasse diagram). This was probably done due to the anticipated locale graph visualization (which does not quite work), or it might be just an omission. I was about to add the reduction 2 days ago, but got stuck elsewhere. (Graph operations are always critical, and not to be rushed in any way. We had famous drop-outs in that module already.) What are the plans for the next release? Graph browsing is a tool too vital that it can be set inoperative. Is there any chancing for improvements, or will there be a switch towards the classical browser alternatively? The release probably happens shortly after the start of the year -- I still don't see the details of the schedule. As usual the general plan is to put things into shape, or disable things that are not in shape. (I will make another round on Graphview pretty soon.) Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Hooks for postprocessing sessions!?
On Thu, 11 Oct 2012, Lukas Bulwahn wrote: this sounds similar to ideas that (Alex and) Lars had to allow find_theorems to search on all Isabelle sessions. As far as I know, they have an implementation for this feature in their shelf. I was wondering about that recently. So far the only visible result was an unclear status of find_theorems.ML (e.g. in Isabelle/e3945ddcb9aa). At some point I would like to see find_theorems.scala as well. Concerning HTML processing and add ons: as a result of some changes due to the new build tool, there are still some loose ends. I was considering more drasting renovations, like moving the functionality into Isabelle/Scala, but did not get very far. I got stuck with WWW_Find and the question of its dependence on old HTML functionality, which is not immediately clear. My present plan for the release was to put classic HTML generation just into the old form again, such that the index looks more ordered and the session information appears in the proper directories. I also need to update the Admin scripts to produce the HTML library for release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Graphview
The class_deps non-scalability probably stems from the omission of the transitive reduction (Hasse diagram). This was probably done due to the anticipated locale graph visualization (which does not quite work), or it might be just an omission. The latter. I am not aware of any locale graph visualization apart from a sketch two (?) years ago on the mailing list. 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] Hooks for postprocessing sessions!?
On 11.10.2012 17:00, Makarius wrote: On Thu, 11 Oct 2012, Lukas Bulwahn wrote: this sounds similar to ideas that (Alex and) Lars had to allow find_theorems to search on all Isabelle sessions. As far as I know, they have an implementation for this feature in their shelf. I was wondering about that recently. So far the only visible result was an unclear status of find_theorems.ML (e.g. in Isabelle/e3945ddcb9aa). At some point I would like to see find_theorems.scala as well. I never got around to add the whole thing to the Isabelle repository. This is partly related to the fact, that I only have an hackish way to hook into the build process and generate the index. I always wanted to revisit this. I'll set it on my list for after the next paper deadline. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Graphview
On Thu, 11 Oct 2012, Florian Haftmann wrote: The class_deps non-scalability probably stems from the omission of the transitive reduction (Hasse diagram). This was probably done due to the anticipated locale graph visualization (which does not quite work), or it might be just an omission. The latter. I am not aware of any locale graph visualization apart from a sketch two (?) years ago on the mailing list. The result is called Graphview now. The 'locale_deps' command will give you the locale aspect of it, but the result is not very usable at the moment. A side question here: Is there a sensible way to make 'print_locale' informative about its axiomatic basis, or its view in terms of the goal presented in interpretation. See also changeset 7b6aaf446496, where I trashed your earlier attempt at it without looking very closely at it -- the priority was to unify the pretty output / pretty tooltip model and get rid of hardwired locale content of the graphview tool. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Hooks for postprocessing sessions!?
On Thu, 11 Oct 2012, Lars Noschinski wrote: On 11.10.2012 17:00, Makarius wrote: On Thu, 11 Oct 2012, Lukas Bulwahn wrote: this sounds similar to ideas that (Alex and) Lars had to allow find_theorems to search on all Isabelle sessions. As far as I know, they have an implementation for this feature in their shelf. I was wondering about that recently. So far the only visible result was an unclear status of find_theorems.ML (e.g. in Isabelle/e3945ddcb9aa). At some point I would like to see find_theorems.scala as well. I never got around to add the whole thing to the Isabelle repository. This is partly related to the fact, that I only have an hackish way to hook into the build process and generate the index. I always wanted to revisit this. I'll set it on my list for after the next paper deadline. It would be also interesting to hear how the conceptual problems of off-line searching are addressed. At the moment we have several partial online solutions. The standard Isabelle document model -- the one being used in Isabelle/jEdit -- is more and more taking grounds from the old HTML stuff. There is already a function to emit one bit XML document here: http://isabelle.in.tum.de/repos/isabelle/file/bb5db3d1d6dd/src/Pure/PIDE/document.scala#l477 There is another function to turn external XML into the internal markup tree. The big conclusion of all this might be pretty close, but as I've said I got distracted by old ML sources around find_theorems / WWW_Find. I don't expect anything on my side before the coming release, though. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
