[isabelle-dev] the function "real"

[Lawrence Paulson]

The first phase of this project is finished: the function “real” now has the 
monomorphic type nat => real and is simply an abbreviation for the generic 
function, of_nat. In addition, the function “real_of_int” abbreviates the 
generic function of_int.

It took about a week to convert all the theories in the main Isabelle/HOL 
directory. Most of them needed little or no attention, the big exceptions being 
Probability (which frequently used “real” with the type ereal => real) and 
Decision_Procs, which contained many thousands of instances of “real” on 
integers and floats.

The main priority at the moment is to fix the decision procedure mir, which 
isn’t working but appears to be entirely unused. Then there is still a lot of 
cleaning up to do, especially in Real.thy and its ancestors. Two or three dozen 
theorems existed in duplicate forms, with versions for “real” separate from 
versions for the other coercions; occasionally these variants were named 
systematically, but often their names were unrelated from the originals, and 
the names of variables in the theorems were almost always different. The 
simplification status of the two variants generally differed as well. Thus the 
behaviour of the simplifier on a formula depended on which coercion had been 
used, and in 150 cases, the simplification itself included the mapping of one 
coercion to another (there were two equivalent theorems for doing this).

Innumerable type constraints have now become redundant (things such as 
real_of_int (i::int)), but I intend to leave them as they are. I have a lot of 
AFP entries to fix.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Isabelle/jEdit - Sidekick

[Mathias Fleury]

Hello list,

in the sidekick there is a "sub-panel"^1 below the sidekick (see the red 
rectangle in the joint screenshot). Is there a way to have line breaks in it? 
The difference between it and the tooltips that appear in the sidekick, is that 
the tooltips disappear, when moving the cursor, while the content of the 
"sub-panel" does not.


I think it would be even more useful if the full multiline theorem could be 
printed out (in the sidekick itself, there is not enough space).

Thanks,
Mathias


PS: I am posting to the dev mailing list, since the jEdit version changed since 
the 2015 release, but there are no line-breaks either in the stable version.


^1 it is probably not its real name, but I haven't found a better one in the 
Isabelle/jedit manual, 

 ___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: State panel

[Mathias Fleury]

Hello Makarius,

this might be intended, but in Isabelle/a99125aa964f from this morning the 
errors and warnings still goes to the output panel, which means that both panel 
have to be opened at the same time. 


Could you give us some insights about your workflow (for theorem proving) with 
the new state panel? I tried it this morning, but it did not fit nicely in my 
workflow, where I look at the output panel after typing a tactic to see if the 
goal is solved or what remains to prove. I would say that having ENTER bound to 
a command like "Insert Newline, Indent and update state panel" would be close 
enough to my workflow, but still solve the performance issues, you mentioned. 
Feedback from other users would be interesting here.


As a side question, is there a way to have two different panels docked at 
bottom open at the same time (i.e. splitting the bottom area into two parts and 
have two different panels in each)?


Thanks,
Mathias

> On 9 Nov 2015, at 21:41, Makarius  wrote:
> 
> * The State panel manages explicit proof state output, with jEdit action
> "isabelle.update-state" (shortcut S+ENTER) to trigger update according
> to cursor position.
> 
> * The Output panel no longer shows proof state output by default. This
> reduces resource requirements of prover time and GUI space.
> INCOMPATIBILITY, use the State panel instead or enable option
> "editor_output_state".
> 
> 
> This refers to Isabelle/bb20f11dd842.  The State panel has been around for a 
> while, without mentioning it explicitly.  It should now be sufficiently 
> consolidated for production use; even old GUI timing problems that caused 
> excessive flashing due to repaints should no longer happen.
> 
> Disabling option editor_output_state allows to get back to the traditional 
> Isabelle/jEdit behaviour, but tradtionalists might actually like the new 
> State panel better, because it is closer to Proof General (in the newer 
> 3-buffer model, not the truely traditional 2-buffer model).
> 
> 
>   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] NEWS: State panel

[Gerwin Klein]

> On 9 Nov 2015, at 9:41 pm, Makarius  wrote:
>
> * The State panel manages explicit proof state output, with jEdit action
> "isabelle.update-state" (shortcut S+ENTER) to trigger update according
> to cursor position.
>
> * The Output panel no longer shows proof state output by default. This
> reduces resource requirements of prover time and GUI space.
> INCOMPATIBILITY, use the State panel instead or enable option
> "editor_output_state".
>
>
> This refers to Isabelle/bb20f11dd842.  The State panel has been around for a 
> while, without mentioning it explicitly.  It should now be sufficiently 
> consolidated for production use; even old GUI timing problems that caused 
> excessive flashing due to repaints should no longer happen.

The separation looks like a good idea, but triggering state panel updates only 
on request doesn’t seem to mesh with how I use the interface these days. I’ve 
become very accustomed to the ability to immediately see the proof state by 
just navigating to the relevant command. It’s one of the things I really like 
about Isabelle/jEdit.

Maybe it’s because the shortcut doesn’t seem to be working for me (do I need to 
clear anything in my jedit settings first to get new defaults?), but even with 
a shortcut, I’ll now need two interactions to look at different proof states, 
when before I only needed one (navigate + shortcut as opposed to just navigate).

It’s true that producing proof state output for every single command in the 
document is a lot of overhead. Would triggering an update for each cursor 
movement (navigation/typing) be as bad as before in terms of overhead (or 
worse), or would it still be less?

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] NEWS: State panel

[Fabian Immler]

Hi Makarius,

I noticed some strange behavior: if one triggers state output on the same 
command but after changing the state, the state output does not change. 
Consider this example:

lemma
  assumes False
  shows "False ∧ False"
  (*using assms*)
  apply simp

If you trigger output on the "apply simp" command, you get 1 subgoal in the 
State panel.
Now uncomment "using assms" and trigger output again (on the "apply simp" 
command): the State panel does not change.

I just noticed that this behavior only occurs when the output is triggered with 
a keyboard shortcut, clicking on the "Update" button yields the expected 
behavior.

Having worked with the "new" interaction model for half a day, I am wondering 
if it could make sense to trigger output in the State panel also implicitly 
with cursor movements?
That would require less explicit interaction with the IDE but still save 
(some?) resources (if I am guessing correctly that previously all intermediate 
proof states have been pretty printed and rendered in the background while now 
it would only happen on demand).

Best regards,
Fabian


> Am 09.11.2015 um 21:41 schrieb Makarius :
> 
> * The State panel manages explicit proof state output, with jEdit action
> "isabelle.update-state" (shortcut S+ENTER) to trigger update according
> to cursor position.
> 
> * The Output panel no longer shows proof state output by default. This
> reduces resource requirements of prover time and GUI space.
> INCOMPATIBILITY, use the State panel instead or enable option
> "editor_output_state".
> 
> 
> This refers to Isabelle/bb20f11dd842.  The State panel has been around for a 
> while, without mentioning it explicitly.  It should now be sufficiently 
> consolidated for production use; even old GUI timing problems that caused 
> excessive flashing due to repaints should no longer happen.
> 
> Disabling option editor_output_state allows to get back to the traditional 
> Isabelle/jEdit behaviour, but tradtionalists might actually like the new 
> State panel better, because it is closer to Proof General (in the newer 
> 3-buffer model, not the truely traditional 2-buffer model).
> 
> 
>   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] NEWS: State panel

[Tobias Nipkow]

On 10/11/2015 14:20, Gerwin Klein wrote:



On 9 Nov 2015, at 9:41 pm, Makarius  wrote:

* The State panel manages explicit proof state output, with jEdit action
"isabelle.update-state" (shortcut S+ENTER) to trigger update according
to cursor position.

* The Output panel no longer shows proof state output by default. This
reduces resource requirements of prover time and GUI space.
INCOMPATIBILITY, use the State panel instead or enable option
"editor_output_state".


This refers to Isabelle/bb20f11dd842.  The State panel has been around for a 
while, without mentioning it explicitly.  It should now be sufficiently 
consolidated for production use; even old GUI timing problems that caused 
excessive flashing due to repaints should no longer happen.


The separation looks like a good idea, but triggering state panel updates only 
on request doesn’t seem to mesh with how I use the interface these days. I’ve 
become very accustomed to the ability to immediately see the proof state by 
just navigating to the relevant command. It’s one of the things I really like 
about Isabelle/jEdit.


I couldn't agree more, and others I spoke to confirm this. Thus it is 
unfortunate that this mode of working now requires an explicit flag that novices 
won't know about, apparently motivated by resource considerations. It would be 
better if people who run into resource problems (novices typically don't) can 
set a flag to disable the state being shown.


Tobias


Maybe it’s because the shortcut doesn’t seem to be working for me (do I need to 
clear anything in my jedit settings first to get new defaults?), but even with 
a shortcut, I’ll now need two interactions to look at different proof states, 
when before I only needed one (navigate + shortcut as opposed to just navigate).

It’s true that producing proof state output for every single command in the 
document is a lot of overhead. Would triggering an update for each cursor 
movement (navigation/typing) be as bad as before in terms of overhead (or 
worse), or would it still be less?

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





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