Re: [isabelle-dev] sledgehammer
On Sat, 31 Aug 2013, Lawrence Paulson wrote: It doesn't always work in the panel either. Some lurking bugs maybe. Can you be more specific? The word bug has no meaning at all. The sledgehammer panel has had only 1-2 rounds of refinements so far, and more precise observations by testers on this mailing list will be required to make it work smoothly for the coming release. I'm not sure what you are allowed to do while sh is running. You should be allowed to do anything you like -- it is fully asynchronous and stateless. In the worst case the system will cancel some sledgehammer request when you edit the command span that it is attached to. (There is a fine point here, since the white space after a command belongs to it, so editing that will remove the sledgehammer query operation as well.) Problems that might be still there are most likely due to propagation of interrupts in the huge stack of tools and system layers we have piled up. So one needs to watch closely the status of top (or top -o cpu on Mac OS X), especially for E Prover processes (e-1.8 from Isabelle/2b5580da3874 might have made this warning obsolete). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: re-checking of main buffer
On Sat, 31 Aug 2013, Christian Sternagel wrote: Assuming that the grayish background highlighting really indicates prover activity in the background This is outdated_color (RGB=EEE3E3 by default). It means that the asynchronous protocol is in an intermediate state where the editor has no confirmation from the prover about the last round of updates yet. The prover needs to update certain internal administrative structures of the document model until this confirmation (the assignment) can be given back to the editor. This requires usually a few milliseconds, but depends on availability of CPU resources, and can get into the range of 0.5..2 seconds. (What are your hardware parameters?) Until recently (notably in Isabelle2013) these update -- assign cycles of the document model involved explicit cancellation of all running executions of the prover *before* doing anything. There was a restart of transactions that were still needed in the next document version. This was OK for the majority of quick proof commands, but noticable for slow things like 'fun' or heavy proof tools. With the integration of sledgehammer etc. into the document model, the end of this approach was come: accidental cancellation and restart of big ATP jobs was not feasible. So I reworked the whole approach quite substantially. As a consequence the prover never stops, it merely refrains from starting new tasks. Then edits are applied on-line and old tasks are cancelled afterwards if they are no longer needed. This means that there are fewer CPU resources available for doing the administrative update of document content. Often it is just the protocol thread itself, which pretends to be another worker thread for this purpose (this guarantees progress, but a fully saturated worker farm might still work against it). For my part, I've seen the change in behaviour and got used to it after a few days. It is just a matter of tradeoff between seeing more outdated text views vs. long-running tools continuing all the time undisturbed. I am not aware of a genuine problem -- if there is one you should report that again. I recently noticed that sometimes a re-check of the whole buffer An actual re-check would be something else: new execs assigned to existing command transactions, involving a change to pink and purple etc. This should not happen here, unless there is something wrong in the implementation. In fact the new strictly monotonic model should involve fewer re-checks. In the past, a long-running proof step upwards in the buffer could cause a reset to that position with a fresh start of everything in between. when I select the second by auto (typically S+Home, since the courser is positioned directly behind it after just having typed it) and then replace the selected region by something different, the whole buffer is highlighted (thus re-chekced or re-parsed?). Re-parsed is yet another thing: whenever you do some physical edits on the buffer, Isabelle/Scala will check on its side if anything has structurally changed to tell the prover about it. This requires some JVM resources, but it should not be visible in the editing process. Vacous updates in that respect are ignored. On the other hand, just scrolling around is a full update of the document model, and might cause brief appearance of the outdated color scheme. This is particularly relevant to the new print functions and query operations of the document model. Uncovering parts of the text might cause the prover to do anything from plain 'print_state' to 'sledgehammer' (in its auto mode). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] numpad doesn't work
On Fri, 30 Aug 2013, Makarius wrote: These days a numpad is relatively rare on keyboards. (I have one at the big laptop at home, but it has quite different behaviour than the more regular numpads on old-style stand-alone keyboards.) I have made some quick tests with my Sony Vaio at home, with its slightly odd arrangement of cursor keys and numeric keypad. The *numeric* mode of it is indeed dead -- I am normally using it for cursor movement, in order to be able to use that keyboard at all. This needs more investigation, but is probably due to the activation of some worarounds of jEdit that are explained in its sources like this: /** Various hacks to get keyboard event handling to behave in a consistent manner * across Java implementations. This type of stuff should not be necessary, but * Java's keyboard handling is crap, to put it mildly. * * @author Slava Pestov */ It was probably a mistake to heed comments in code -- they are usually very unreliably source of information. What did improve, though, was a situation with ESCAPE handling when tooltips compete with text selection. Anyway, it looks like another dive into the depths of history of keyboard handling on Windows, Linux, Mac OS X -- the JVM has preserved all the old ways faithfully. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
Am 02/09/2013 11:18, schrieb Makarius: The sledgehammer panel has had only 1-2 rounds of refinements so far, and more precise observations by testers on this mailing list will be required to make it work smoothly for the coming release. Some observations: - When clicking on the generated proof it is appended to the end of the proof text preceding the invocation point. It would be better to insert a newline first - otherwise the proof develops in a horizontal rather than the standard vertical direction. - Sometimes I click on the generated proof and it is not pasted into the theory text. It just doesn't work, even if I click repeatedly. I cannot reproduce this reliably. - Once one has clicked on a proposed proof and it has been pasted into the theory window, this does two things: a) it stops the rest of the running atps. b) it disables all the proposed proofs, i.e. no more click-and-paste for any of them. Neither is desirable and I thought at least a) was not the case in the past. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] including raises Attempt to perform non-trivial merge of theories
On Tue, 13 Aug 2013, Andreas Lochbihler wrote: I get the error Attempt to perform non-trivial merge of theories when I include a bundle from another theory and there are at least two imports. In the attachment, there's an example. This should work in Isabelle/ef65d5ee60cf. Are there any remaining problems in the concrete application behind the example? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
I have also noticed the first issue you mention. Regarding your other points, a) seems logical to me (you have made your choice), while b) possibly simplifies the implementation significantly (otherwise you need to remember to replace the previous choice rather than to append the text), and it is only necessary in the fairly unusual case where your first choice simply didn't work. I agree that the generated proof should start on a fresh line, because these calls are often quite lengthy text strings. Larry On 2 Sep 2013, at 11:31, Tobias Nipkow nip...@in.tum.de wrote: - Sometimes I click on the generated proof and it is not pasted into the theory text. It just doesn't work, even if I click repeatedly. I cannot reproduce this reliably. - Once one has clicked on a proposed proof and it has been pasted into the theory window, this does two things: a) it stops the rest of the running atps. b) it disables all the proposed proofs, i.e. no more click-and-paste for any of them. Neither is desirable and I thought at least a) was not the case in the past. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] including raises Attempt to perform non-trivial merge of theories
Hi Makarius, The error has already gone away in cb82606b8215 when Ondřej moved all the Quotient_... theories to Main, i.e., there was no non-trivial merge necessary any more. My concrete application works as expected at the moment. Andreas On 02/09/13 12:56, Makarius wrote: On Tue, 13 Aug 2013, Andreas Lochbihler wrote: I get the error Attempt to perform non-trivial merge of theories when I include a bundle from another theory and there are at least two imports. In the attachment, there's an example. This should work in Isabelle/ef65d5ee60cf. Are there any remaining problems in the concrete application behind the example? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
Am 02/09/2013 13:13, schrieb Lawrence Paulson: I have also noticed the first issue you mention. Regarding your other points, a) seems logical to me (you have made your choice), while b) possibly simplifies the implementation significantly (otherwise you need to remember to replace the previous choice rather than to append the text), and it is only necessary in the fairly unusual case where your first choice simply didn't work. If you take asynhronous processing seriously you shouldn't have to wait until the end before you make your choice but you should be able to revert your decision if something better comes up. In such cases the user should be responsibe for removing the first proof. But you are right, this could lead to complications in the implementation. Tobias I agree that the generated proof should start on a fresh line, because these calls are often quite lengthy text strings. Larry On 2 Sep 2013, at 11:31, Tobias Nipkow nip...@in.tum.de wrote: - Sometimes I click on the generated proof and it is not pasted into the theory text. It just doesn't work, even if I click repeatedly. I cannot reproduce this reliably. - Once one has clicked on a proposed proof and it has been pasted into the theory window, this does two things: a) it stops the rest of the running atps. b) it disables all the proposed proofs, i.e. no more click-and-paste for any of them. Neither is desirable and I thought at least a) was not the case in the past. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] conflict between code_identifier constant and module_name
Two months ago, Florian replaced code_module with code_identifier (6646bb548c6b). Now, I
am having trouble using the greater capabilities of code_identifier. I would like to
assign a constant to a different module, say
code_identifier constant replicate \rightharpoonup (SML) My_Module.rep
Then, code generation works fine as long as there is no module_name involved:
definition test where test = replicate
export_code test in SML
export_code test in SML module_name foo (* fails due to module dependency
cycles *)
Unfortunately, many idioms internally use module_name -- for example, all of the following
raise errors due to module dependency cycles:
ML {* @{code test} *}
value [code] test 3 (0 :: nat)
lemma test = foo quickcheck
The same problem also occurs with type constructors. Therefore: What is the intended way
of using code_identifier with constants?
Best,
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release
The French summer vacation period has ended, so I've switched myself now into consolidation mode to put things into shape for release. The first release candidates of Isabelle2013-1 will probably happen in the first or second week of October. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL iff notation
For uniformity I almost always use = and would not like to see it printed as --. Tobias Am 02/09/2013 16:24, schrieb Makarius: (This is just a side-track on HOL notation, which came to me when cleaning up theories with old ASCII replacement syntax like | -- - Un Int etc. -- which is very easy with explicit C+b completion in Isabelle/jEdit.) Isabelle/4379d46c8e13 (Oct 2005) introduces alternative iff syntax for equality on booleans, with print_mode 'iff'. I can't remember a particular reason for the print mode, instead of having that syntax always on. I find myself using the iff notation most of the time to make theories look nice. Are there clubs of iff vs. non-iff? If almost everybody is a member of the iff club we could just remove that print mode. (We don't have to consider that for the coming release, to avoid any real-time pressure on this question.) 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] The coming release
The earlier the better because, as I told you at ITP, I have a course starting in the middle of October and they need to use a new Isabelle, in the worst case a release candidate. Tobias Am 02/09/2013 15:37, schrieb Makarius: The French summer vacation period has ended, so I've switched myself now into consolidation mode to put things into shape for release. The first release candidates of Isabelle2013-1 will probably happen in the first or second week of October. 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] HOL iff notation
On Mon, 2 Sep 2013, Lawrence Paulson wrote: I tend to use -, but I'm afraid I don't know what a print mode is. A print mode allows to change the way how the system prints things; there are command line options -m MODE or Isabelle settings to various isabelle tools for that. Sometimes print modes have a genuine purpose, e.g. for different protocols of the prover: Proof General, Isabelle Process, latex, HTML etc. Sometimes print modes are just there to allow everyone's favourite syntax to coexist in the system. (The latter is an aspect of very old Isabelle insider jokes that nobody remembers now.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL iff notation
On Mon, 2 Sep 2013, Makarius wrote: I find myself using the iff notation most of the time to make theories look nice. Are there clubs of iff vs. non-iff? If almost everybody is a member of the iff club we could just remove that print mode. I've forgotten to point out the relationship to this isabelle-users thread about Isabelle operator precedence: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-November/msg00020.html Part of it was some confusion about infixl vs. infix of HOL eq and not_equal, which was coming from a bit too many variants being there, and some of them not quite right (it is probably right at Isabelle/b46e6cd75dc6). Back then I wrote: I think the = notation is going back to a time even before the 'infixl' / 'infixr' macros for the general mixfix form, and there were also some special tweaks for output and breaks unlike regular infixes. 'infix' is much younger than all that. In the last 10 years, there have been some slight reforms towards more regularity of notation for eq/not_equal in HOL. It might be worth trying again to make it all just plain infix 50, although just from the ancienticity of it it could cause some surprises in some dark corners. Trying the latter, i.e. using just plain infix 50 for = and its negated version, reveals problems rather early. For example in Set.thy: lemma subset_eq [no_atp]: A ≤ B = (∀x∈A. x ∈ B) by blast So any of the infixes with priority 50 will cause problems that do not exist with the iff notation, since that has weaker priority. The latter also allows to remove many parentheses. The above example also has ≤ instead of ⊆ for sets, which is somehow related. (Continuing that train of thought will inevitably expose cans of worms, so this speculative thread is definitely not relevant for the coming release.) Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL iff notation
To me, the ability to use = (on booleans) as an alternative to - is an artefact of HOL, rather than something to encourage. Almost always, - is more readable. At least that's my view. Larry On 2 Sep 2013, at 19:42, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Are there clubs of iff vs. non-iff? If almost everybody is a member of the iff club we could just remove that print mode. (We don't have to consider that for the coming release, to avoid any real-time pressure on this question.) I am definitely a member of the iff-club. Partly for precedence reasons, but also because you can recognize predicate equations immediately. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Improved completion mechanism
On Mon, 2 Sep 2013, Makarius wrote: In Isabelle2013 the completion popup was not triggered when deleting characters (with backspace). Now this is the case and it seems to cause more frequent hangs for me (since deleting is typically done very fast). Is this behavior intentional, and if yes, what is the gain? SideKick had a special flag for backspace treatment, which was off by default. By not using SideKick anymore that behaviour came out naturally from the way things work. I have observed the change myself, and started thinking if it is good or bad. So far I consider it as good -- a more natural flow of typing, e.g. when potential completions are accidentally missed in the first attempt. Generally, there is quite a difference in the completion behaviour with the 3 options for it, and the possibility to do explicit completion via C+b. Training my fingers a bit more, I've found that the backspace behaviour makes it hard to delete keywords that can be completed. So I am considering to get rid of it again. Missed completions can be completed via C+b after deletion of bad parts -- I actually did not have C+b when trying this at first. The hangs are yet a different story to be sorted out. I do want to know which bleeding edge Linux component is responsible for disrupting Java keyboard input. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL iff notation
On 03/09/2013, at 12:24 AM, Makarius makar...@sketis.net wrote: Are there clubs of iff vs. non-iff? If almost everybody is a member of the iff club we could just remove that print mode. (We don't have to consider that for the coming release, to avoid any real-time pressure on this question.) I like both. I mostly use =, because it is less typing. I usually prefer output being equal to input, but I will use - for presentation occasionally (in that sense, the print mode is ideal for me). I also still use == quite a bit, I never understood why it is discouraged so much. It has the better precedence, and I use it mostly for the difference between a definition and an equation, which non-Isabelle people seem to understand. Cheers, Gerwin 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
Re: [isabelle-dev] HOL iff notation
Same here. - cheers chris Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Are there clubs of iff vs. non-iff? If almost everybody is a member of the iff club we could just remove that print mode. (We don't have to consider that for the coming release, to avoid any real-time pressure on this question.) I am definitely a member of the iff-club. Partly for precedence reasons, but also because you can recognize predicate equations immediately. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ 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] NEWS: Improved completion mechanism
On 09/02/2013 06:30 PM, Makarius wrote: On Sat, 31 Aug 2013, Christian Sternagel wrote: First note that for me keyboard input to Isabelle/jEdit typically hangs every 10 minutes or so, depending on how fast I type (but this is an old and known issue). I was hoping that it would have disappeared altogether. So far the speculation was that the hang is due to the window manager and its built-in conflicts with JWindow etc. The popups are now done without separate window, as plain Swing JComponent. So the persisting hang indicates some problem in more elementary key hangling or plain text insertion into the text buffer. I have myself done a lot of empirical tests recently on several quite different systems, and I am also typing very fast, but did not see any problem like that. Just for the record: the above mentioned hand also sometimes happens when typing V ... E ... R ... Y ... slowly ;). It is just more frequent when typing faster (mainly because a hang only ever happens directly after having pressed a key). It looks like we need to make another round in the game of guessing at oddities that Fedora Linux might have installed. Yes please. How can I be of assistance (as apparently the only person having this kind of issue ;) ... maybe I should just buy a new computer, however, Fedora Linux is my preferred Platform, so maybe as soon as I get my hands on a different machine having Fedora installed -- which might take some time -- I should check whether this is specific to *my* laptop or a general issue of Fedora; or did we establish an answer already)? chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
