Re: [isabelle-dev] NEWS: Dockable window Find
On Fri, 20 Sep 2013, Holger Gast wrote: The layers 2+3 offer extensive means of customization. To come back to the above example, one does, of course, not set StyleRanges on the SWT widget oneself. One registers with the JFace TextViewer's syntax highlighting mechanism and produces them on demand -- for instance from the semantic markup offered by Isabelle/Scala. Again: Why not make this practical, and tell Andrius Velykis about it? He has already Isabelle/Eclipse that is more than just a proof of concept or a small demo, so it deserves to catch up with the quality standards of Isabelle/jEdit. -- and all the portability issues will probably come back once again in a different form. Actually, probably not: the Eclipse IDE is widely used on the platforms that Isabelle supports and the IBM engineers are doing a constantly great job at keeping the differences under the hood of SWT and the whole system running. Since the Eclipse/JFace/SWT stack is actually used in industry for end-user applications, there is a lot of pressure to succeed. The available delta-pack makes it straightforward to package an application for different platforms. Above you could just as well substitute IBM for Oracle, and Eclipse/JFace/SWT for whatever frameworks Oracle has in the portfolio (e.g. Swing, Java FX), and make syntactically the same claim. After 5 years of working on a real application with JVM + x at the bottom, I just don't believe any such talk about industrial frameworks any more. Anyway, this thread is going in circles, back to the point where it started 5 years ago. The only difference is that Isabelle/jEdit has become real in the meantime -- with a lot of extra work that was not anticipated at the start (both due to evil companies like Oracle or Apple, and chaotic communities like Linux XYZ). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit interface
On Thu, 19 Sep 2013, Makarius wrote: On Wed, 18 Sep 2013, Tobias Nipkow wrote: I just noticed the following behaviour in 705f0b728b1b: When the cursor remains fixed in the theory window and I scroll in that window with the help of the scoll bar, the output window goes blank when the line with the cursor is no longer visible. I have no idea when that changed but in Isabelle 2013 it was not like that - the output would not go blank. I think it is just a consequence of the major reforms of the document execution model from this summer. Since this is my own department it will be easy to address, and not require descending into the dungeons of JDK sources again. I will come back to this within a few days. changeset: 53780:ef62204a126b user:wenzelm date:Sat Sep 21 20:58:32 2013 +0200 files: src/Tools/jEdit/src/document_view.scala description: caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view); It remains to be seen if this is exactly the right notion of visibility to get Output of proof states as expected in most situations. The point here is that the system gives up old prover output when it is considered unreachable by GUI components. This conserves scarce JVM memory resources (see also d598b6231ff7). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Find theorems and Sledgehammer Panels
On Thu, 5 Sep 2013, Christian Sternagel wrote: Last time I tried, there was no auto completion available in the input of the find theorem panel. Which makes the variant of typing find_theorems yourself in the main buffer more convenient for me at the moment. With Isabelle/322a3ff42b33 there is now completion for the history text field behind it. It is again one of these typical instances of spending 2h to make it work on Linux and Windows, and requiring days or weeks to find out why Apple/Oracle don't quite manage on Mac OS X: the focus change after completion selects all text. (Problem still pending.) Also I experienced already several hangs with this panel as well as the sledgehammer panel. For the former that means that even after waiting for a long time nothing shows up, whereas for the latter the whole main buffer stays in a grayish highlighted state and does no longer produce output in response to edits (and also doesn't respond to clicking cancel). This sounds again like a total-existence-failure due on Fedora. Was last time I tried already on jdk-7u40? Just a straw of hope ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Total failure of sledgehammer
Hi Larry, Am 13.09.2013 um 21:17 schrieb Lawrence Paulson l...@cam.ac.uk: That fixed it. One of the Australians has run into the same issue with MaSh. The issue should be addressed starting with Isabelle/8d9f4e89d8c8. If you're willing to give MaSh a second try, you could try to set MASH=yes again. To be sure that no stale data or zombies lie around, I would recommend running the following commands: pkill -f ython.*server.py rm -fr ~/.isabelle/mash/ Thank you for the report sorry for the invconvenience! Regards, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer Nitpick spy mode
Dear all,
Starting with Isabelle/58d1b63bea81, Sledgehammer and Nitpick have a spy mode
[*] that log all invocations to those two tools in
~/.isabelle/spy_{sledgehammer,nitpick}. If you are willing to be part of a
big experience in the name of science, please add
SLEDGEHAMMER_SPY=yes
NITPICK_SPY=yes
to your ~/.isabelle/etc/settings file to enable the logging. And let me know
at some point that you have enabled the logging, so that I will remember to bug
you [*] to get the files after X months. The information stored is very crude
-- e.g. no names of theories, theorems, or constants are or will ever be
stored. It's just to get a picture of how useful (or not) these two tools are
in the wild.
Thanks for your collaboration!
Jasmin
[*] Tobias suggested calling it prism. The recent news provide us with some
other interesting names.
[**] bug in the meaning of annoy or bother you, not conceal a miniature
microphone, of course. ;)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit on Mac OS X
On Mon, 23 Sep 2013, Makarius wrote: This is a note on jEdit in general: https://sourceforge.net/projects/jedit/ There is some recent revival of activity around Mac OS X. Hardcore users of that platform are encouraged to look closely at current jEdit versions -- maybe the daily builds for jEdit 5.2pre1 -- to see how it works, and add items to one of the many trackers of that project. A few more hints: This only makes sense with Oracle Java 7 (e.g. the current 7u40), not the old Apple Java 6. Moreover, it might be actually easier to use the jedit SVN repository with something like ant build, ant run etc. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit on Mac OS X
This is a note on jEdit in general: https://sourceforge.net/projects/jedit/ There is some recent revival of activity around Mac OS X. Hardcore users of that platform are encouraged to look closely at current jEdit versions -- maybe the daily builds for jEdit 5.2pre1 -- to see how it works, and add items to one of the many trackers of that project. I have myself submitted various patches already, even though I am only a part-time Mac user myself (since 2008). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
Some more details: until 0d0c20a0a34f we have the expected behavior. With changeset: 52622:e0ff1625e96d user:wenzelm date:Fri Jul 12 16:19:05 2013 +0200 summary: localized and modernized adhoc-overloading (patch by Christian Sternagel); term bind (Some my_abbrev) f is not accepted at all (red, but no error message; but I think this is an orthogonal issue of implicit assumptions on my side that where not correct and which was resolved in the meanwhile). Nevertheless, this is the changeset I suspect to introduce the new behavior, since here the implementation of insert_internal_same (which is now called insert_overloaded) is drastically changed. Before this changeset variants are always Consts and thus replacing variants with their overloaded constant is easily done by pattern-matching on variants. After this changeset, variants may be arbitrary terms (due to localization). Now replacing a variant by the corresponding overloaded constant is done by rewriting (as Florian already pointed out, this happens in insert_overloaded) as follows fun insert_overloaded ctxt variant = (case try Term.type_of variant of NONE = variant | SOME T = Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [Option.map (Const o rpair T) o get_overloaded ctxt o Term.map_types (K dummyT)] variant); Apparently this interferes with abbreviations. Am I doing anything strange here? cheers chris On 09/24/2013 01:06 PM, Christian Sternagel wrote: Dear Florian and Peter, first, sorry for my long silence, I was on holidays. On 09/20/2013 12:30 AM, Florian Haftmann wrote: Hi Peter, hi Christian Referring to Isabelle_12-Sep-2013: When using overloading from Monad_Syntax, abbreviations are no longer displayed in output syntax: is this »no longer« referring to the state of Isabelle2013? Or did it also go wrong then? This works as expected with Isabelle2013. Most likely, my recent localization of adhoc overloading caused the new behavior (which I agree is not nice). I was not aware of this myself, thanks for bringing it to my attention. theory Scratch imports Main ~~/src/HOL/Library/Monad_Syntax abbreviation my_abbrev \equiv [True] term foo (Some my_abbrev) f (* Yields: foo (Some my_abbrev) f *) term bind (Some my_abbrev) f (* Yields: Some [True] = f*) A first analysis: theory Monad_Syn imports Main ~~/src/Tools/Adhoc_Overloading begin consts bind :: ['a, 'b ⇒ 'c] ⇒ 'd adhoc_overloading bind Set.bind Predicate.bind Option.bind List.bind abbreviation my_abbrev \equiv [True] term foo (Some my_abbrev) f (* Yields: foo (Some my_abbrev) f *) term bind (Some my_abbrev) f (* Yields: bind (Some [True]) f *) The monad syntax is not to blame, the problem is already in adhoc overloading. Using declare [[show_variants]] term foo (Some my_abbrev) f (* Yields: foo (Some my_abbrev) f *) term bind (Some my_abbrev) f (* Yields: Option.bind (Some my_abbrev) f *) Going to the corresponding lines in adhoc_overloading.ML: fun uncheck ctxt = if Config.get ctxt show_variants then I else map (insert_overloaded ctxt); I roughly guess something in insert_overloaded modifies the term in a way that the abbreviation does not apply any longer (again, only a rough guess). Thanks for the nice analysis. @Christian: maybe you have a suggestion what is going on here? At the moment not. I will investigate this issue and come back to the mailing list as soon as I find out more. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
