subject:"\[isabelle\-dev\] Remaining uses of Proof General\?"


On Fri, 27 Jun 2014, Peter Lammich wrote:


I have compiled a list of problems that I encountered during my work.


OK, I will go through it one by one to eliminate them -- either by 
pointing out known ways how to do it in Isabelle/jEdit, or by fine-tuning 
the system in this stage before the release.


Power users of Isabelle/jEdit are encouraged to contribute their own 
expertise, while keeping in mind that we are presently on a particular 
repository snapshot context.  Some general things are better discussed 
separately on isabelle-users; there will be also a follow-up thread next 
week for Isabelle2014-RC0 where a broader audience can participte.



Makarius

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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


My overall impression is that Isabelle/jEdit is usable but much less
mature than PG:
It does not scale well to large projects, and tends to be unstable.
It has many cool advanced features, but lacks important basic ones.


Better reverse all that, just to simplify your life.  There might be 
technological fine points, but the big problems are phsychological ones. 
You need to leave PG behind and adopt a quite different system.



However, in my opinion, Isabelle/jEdit is approaching a level of 
maturity required for production use, once the user knows about its 
deficits and how to avoid them.


That is also a tautology: PG has tons of deficits, but working around them 
has become second nature to long-term users. In Isabelle/jEdit you need to 
get used to different behaviour, and make yourself productive with it.


*Any* system is just crap, but in different ways.


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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


SCALABILITY  STABILITY:

* Isabelle/jEdit gets really slow and unresponsive when many files are
loaded (you have to wait seconds for a keystroke to show its effect). As
all prerequisite theories (not in an image) are automatically loaded,
this is unavoidable. In PG, it's no problem to load a theory with many
prerequisites, nor to have many buffers open simultaneously.

NOTE: This problem could be solved in my case by 1) giving jEdit a
ridiculously large amount of heap space (4Gb) and, 2) using images for
prerequisite theories.


There is a conceptual difference here: PG edits only a single file, but 
the Prover IDE a whole project.  This usually works, if the resources that 
are available on current hardware is actually used.


A JVM heap space of 4 GB is not ridiculously large, but perfectly normal 
-- a cheap high-end laptop as at least 8 GB.  On my 5 years old 
workstation, I use 4-8 GB JVM heap routinely.  The l4.verified project 
has reported 16 GB of JVM heap requirements, which I would call quite 
reasonable for such a large thing.



If there are remaining resource problems, they need to be backed-up by 
proper experimental data: hardware parameters, Poly/ML memory options, JVM 
memory options, concrete examples etc.


It does not make sense to use Isabelle/jEdit in a way that PG was used 10 
years ago, concerning these important side-conditions.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* Isabelle/jEdit does not scale to large files. Error markers on the
right side are only displayed for a context around the current cursor
position. There seems to be no way to jump to the error position. If the
error happens to be displayed as a red bar on the right side of the
editor area, pixel-accurate mousing is required to jump to the error,
and not to a position dozens of lines away.


This needs more specific information about the experimental setup.  What 
means large?  Where were the errors coming from?


The so-called text overview column is indeed a performance bottle-neck. 
It is restricted by default to a portion of the text buffer, to avoid 
problems with real-time rendering of exessivley large files.  See also the 
system option jedit_text_overview_limit -- its default value 65536 is some 
kind of insider-joke.  You can try to enlarge that a bit, depending on 
your hardware performance.


That clickable area is convenient, but not strictly necessary.  It is 
absent in PG anyway.  Whenever the Prover IDE outputs an error message, 
e.g. in tooltips or the Output panel, it includes the source position 
information, *if* that is available.  In the repository versions we are 
talking about here, there is a \here symbol that is rendered as a 
Unicode house (for home position).  It replaces the textual 
representation from the past TTY era: (line 42 of file foo).  That 
symbol can be used as hyperlink using the normal PIDE idioms.


If the latter is missing, their might be a problem with the tool that 
emitted the error message.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* Isabelle/jEdit seems to be quite unstable. Within one week, it
  happened several (3 or 4) times that the whole thing just became
  unresponsive, and had to be restarted to continue work. In PG, those
  things happen perhaps once in a month.


The default guess is that the JVM has too little heap space.  You have 
called 4 GB unreasonably large before, which is an indication that your 
defaults are far too low.


If problems happen again with 4-8 GB JVM heap, you should describe what 
really happens, with clear experimental setup.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* Isabelle/jEdit does not support highlighting of paranthesis in the
output window (it does work in PG!). This is an essential feature to
read bigger goal states.

Moreover, the output buffer does not support middle-mouse-button
copy-and-paste on my ubuntu-box, while it perfectly works in the editor
window.


PG uses Emacs with its everything is a buffer model; Isabelle/jEdit uses 
jEdit + Java/AWT/Swing, with slightly different side-conditions. Both have 
sometimes advantages, and sometimes disadvantages.


The middle-mouse-button is an ancient X11 idiom that no other platform 
knows, and Swing does not support it.  The jEdit guys have retrofitted 
that ocasionally useful idiom to the standard jEdit text area, but it is 
absent in regular Swing GUI components.


You get other benefits from the more standard and less Unix/X11-centric 
approach in jEdit; it just needs more practice to discover the wealth 
jEdit features.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* Long list of warnings, e.g. duplicate simp rule, or tracing messages
produced by a method appear before the subgoals in the
 output, and thus makes them inaccessible without lots of scrolling.
This feature is a real flow-stopper when exploring proofs.

In PG, it is possible to have separate buffers for the goal-state, the
tracing, and the warning messages, thus you always see the current
subgoal you are working on without scrolling down some buffer every
time.


Just a few hints:

  * Regular messages (writeln, warning, error) also appear in the
squiggly rendering of the sources, to be hovered over and inspected
without scrolling *the* Output.  There is in fact no reason to have
just one (or two or three) focal points for certain printed results,
like in TTY / PG.

  * Tracing is a different topic -- it was never really sorted out
satisfactorily in the history of PG.  More than 1 year ago, Lars Hupel
made some efforts for modernized tracing in PIDE, but it got seriously
encumbered by PG legacy.  It still needs to be revisited just before
the Isabelle2014, to see if it can be made ready for prime time.

I don't see any show-stoppers here.  Just more potential for refinements, 
when PG is discarded.



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

Re: [isabelle-dev] Remaining uses of Proof General?


 That clickable area is convenient, but not strictly necessary.  It is 
 absent in PG anyway.  Whenever the Prover IDE outputs an error message, 
 e.g. in tooltips or the Output panel, it includes the source position 
 information, *if* that is available.  

The problem is, that I cannot make the output panel display the error
message, or get a tooltip on the error message, without *first* locating
its position in the editor window!?

Following example: Slightly change the simpset, and try to load
$AFP/Automatic_Refinement/Lib/Misc.thy, a 4400 lines beast. Change the
simpset so that it fails somewhere in the middle of the theory.
I only see a red mark in the theory-panel, but how do I navigate to the
error location?

In PG, I actually saw file-name/line-number/error-message. In
Isabelle/jEdit, the only way I know is to open the file, hope that the
text-overview column displays the error already, and try a precise
mouse-click to get to the location. If the error-column does not display
the error, because it is not within the limit, I have to scroll through
the file manually.

So am I missing some feature here that makes the workflow 
Navigate to an error in a theory file
simpler?


--
  Peter

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

Re: [isabelle-dev] Remaining uses of Proof General?


 The default guess is that the JVM has too little heap space.  You have 
 called 4 GB unreasonably large before, which is an indication that your 
 defaults are far too low.

OK, I'll try more on my 8Gb machine ... or upgrade my machine.


 If problems happen again with 4-8 GB JVM heap, you should describe what 
 really happens, with clear experimental setup.

Giving a clear experimental setup is a real problem for errors that
appear nondeterministically.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* If sledgehammer (both over panel and as command) is running, further
processing of the file is blocked/very slow. Thus, it is not possible
to run sledgehammer and, in parallel, continue exploration to find your
own proof. In PG, parallel sledgehammering works, and I used it
extensively. In Isabelle/jEdit I now think twice before I invoke
sledgehammer, because it just interrupts my workflow and I have to wait
for it to finish staring at the sledgehammer-window and doing nothing.


This sounds like some serious performance problem, and requires proper 
reports on your hardware and system parameters.


In Isabelle2014 the Sledgehammer integration is in its third generation. 
It is supposed to work without problems.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* Isabelle/jEdit cannot open a theory-file without processing it. This
is in particular a problem when porting stuff and opening the original
version of the same file to look something up. Even worse: Once opened,
you cannot close the file again, and it will remain in the theory panel
(with an error marker) until you quit jEdit.


You can in principle switch off the continous checking, e.g. in the 
Theories panel.


Slight inconveniences and potential for improvements remain, but this is 
no show stopper as far as I can tell.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


Moreover, I would like an incremental search, but there is probably a
jEdit pluging somewhere? (Probably with the same problems of entering
non-ASCII characters)


Other people have given some hints already.

You should also take the time to *print* and *read* the original jEdit 
user's guide, e.g. see http://www.jedit.org/index.php?page=docs.  It is a 
very powerful editor, and Emacs looks really awkward compared to it.



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

Re: [isabelle-dev] Remaining uses of Proof General?

On Fr, 2014-06-27 at 13:58 +0200, Makarius wrote:
 On Fri, 27 Jun 2014, Peter Lammich wrote:
 
  * Long list of warnings, e.g. duplicate simp rule, or tracing messages
  produced by a method appear before the subgoals in the
   output, and thus makes them inaccessible without lots of scrolling.
  This feature is a real flow-stopper when exploring proofs.
 
  In PG, it is possible to have separate buffers for the goal-state, the
  tracing, and the warning messages, thus you always see the current
  subgoal you are working on without scrolling down some buffer every
  time.
 
 Just a few hints:
 
* Regular messages (writeln, warning, error) also appear in the
  squiggly rendering of the sources, to be hovered over and inspected
  without scrolling *the* Output.  There is in fact no reason to have
  just one (or two or three) focal points for certain printed results,
  like in TTY / PG.
 
* Tracing is a different topic -- it was never really sorted out
  satisfactorily in the history of PG.  More than 1 year ago, Lars Hupel
  made some efforts for modernized tracing in PIDE, but it got seriously
  encumbered by PG legacy.  It still needs to be revisited just before
  the Isabelle2014, to see if it can be made ready for prime time.
 
 I don't see any show-stoppers here.  Just more potential for refinements, 
 when PG is discarded.


These hints do not adress the problem! During proving, I want to see the
goal state in first place, not the errors/warnings/etc. If I have to use
the mouse and scroll down to the goal state every time I change
something, this really interrupts the working flow during proof
development. 

Once I have finished the proof, I am interested in the error and warning
messages, and really appreciate the tooltips on the squiggly lines.

--
  Peter



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* When theories have inconsistent file/theory name, you will only find
the error by stepwise going back the chain of bad theory -  errors,
file by file. This is simply tedious. In PG, you got a backtrace in the
output, and could immediately identify the broken file.


I need to postpone this, to see if there is anything significant behind 
it.  There are indeed slight inconveniences in re-arranging theory file 
names, but I did not see much of that in the past few years of routine use 
of Isabelle/jEdit (e.g. for Isabelle + AFP maintenance).


Note that the Theories panel is the main point to look over a whole 
project, to see its status -- assuming that the basic project structure is 
right.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* Auto-Completion does not really work. You have to decide for a
completion delay. If you choose it too short, some completions will
not appear at all. If you choose it too long, it interrupts your typing
flow when entering special characters.

In PG, there is no context-sensitive completion at all ... the one in
jedit is actually not usable without
 tolerating .5sec completion delay on every special character you want
to type)

Moreover, the completion mechanism for entering special characters seems
not to be as mature as the one in PG was: When entering sequences that
should be completed, e.g., \lambda, this only works if there are no
characters behind. All in all, I am typing significantly more to enter
special characters than I did in PG.


This belongs to the long completion thread we've had some weeks ago.

You do need to change your practices of typing.  Moreover you do need to 
find completion options that work for you.  There might be even some kind 
of retro legacy setup that imitates old PG behaviour to some extent, but 
I leave it to others to find this out.


I can only say that I am myself typing less and less in recent years, but 
I am biased, since I know many fine-points of how it really works.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


* Disappearing Proofs in PG is a really nice feature to keep overview,
  in particular in larger files. In PG, I used it heavily. There is
  nothing similar in Isabelle/jEdit. Code-folding can be used to a
  certain extent, but it cannot handle apply-style proofs, and is not
  applied automatically as in PG.

Moreover, code-folding still seems not to work properly: Sometimes, 
fold-markers simply do not appear, sometimes they appear at completely 
wrong places. I'm not sure whether this is a non-deterministic effect, 
or depends on some garbage text at the end of the theory file.


jEdit has some fold support, but the Isabelle/jEdit version of it is still 
in the adhoc state of 2010, i.e. very basic and hardly usable.


I tried again for the coming release to make more of this work, but I got 
entangled into too many other problems.  This is also the reason, why I 
have started to spend signigicant time to make a clear slate, and 
eliminate the remaining uses of Proof General first.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


If problems happen again with 4-8 GB JVM heap, you should describe what
really happens, with clear experimental setup.


Giving a clear experimental setup is a real problem for errors that
appear nondeterministically.


The first thing is to describe the starting conditions:

  * Precise CPU model + memory size

  * Operating system

  * ML options (heap size, threads)

  * JVM options (heap size)

The second thing to point the the examples that were used, and give some 
hints about the concrete situation.



Makarius

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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


   * Regular messages (writeln, warning, error) also appear in the
 squiggly rendering of the sources, to be hovered over and inspected
 without scrolling *the* Output.  There is in fact no reason to have
 just one (or two or three) focal points for certain printed results,
 like in TTY / PG.

   * Tracing is a different topic -- it was never really sorted out
 satisfactorily in the history of PG.  More than 1 year ago, Lars Hupel
 made some efforts for modernized tracing in PIDE, but it got seriously
 encumbered by PG legacy.  It still needs to be revisited just before
 the Isabelle2014, to see if it can be made ready for prime time.

I don't see any show-stoppers here.  Just more potential for refinements,
when PG is discarded.



These hints do not adress the problem! During proving, I want to see the
goal state in first place, not the errors/warnings/etc. If I have to use
the mouse and scroll down to the goal state every time I change
something, this really interrupts the working flow during proof
development.


We should look at this together at VSL 2014, such that I see how your 
present workflow works.


PG has forced a certain model onto the proof assistant in 1998, and I 
adapted to that faithfully in 1999, without ever understanding the real 
policies.  This caused many problems, and in PIDE there is hardly anything 
about such policies: all messages are appended in some canonical order 
produced by the system.


As I have pointed out in my presentation at TUM last december, I would 
like to see some kind of Preview of such document state information 
eventually.  But that is music the future, as Florian Haftmann would say.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Makarius wrote:


On Fri, 27 Jun 2014, Peter Lammich wrote:


 * If sledgehammer (both over panel and as command) is running, further
 processing of the file is blocked/very slow. Thus, it is not possible
 to run sledgehammer and, in parallel, continue exploration to find your
 own proof. In PG, parallel sledgehammering works, and I used it
 extensively. In Isabelle/jEdit I now think twice before I invoke
 sledgehammer, because it just interrupts my workflow and I have to wait
 for it to finish staring at the sledgehammer-window and doing nothing.


This sounds like some serious performance problem, and requires proper 
reports on your hardware and system parameters.


In Isabelle2014 the Sledgehammer integration is in its third generation. It 
is supposed to work without problems.


This appears to be again one of these problems are kept secret situation 
that has made Isabelle2013-1 a failure, and left many questions after 
Isabelle2013-2 if the Isabelle release process still works.


It is important to note that I don't have any first-hand access to power 
users who do serious testing.  I do depend on proper problem reports, 
beyond there is a bug, it does not work.  Otherwise we need to stop 
making Isabelle releases.



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

Re: [isabelle-dev] Remaining uses of Proof General?

On Fr, 2014-06-27 at 14:22 +0200, Makarius wrote:
 On Fri, 27 Jun 2014, Peter Lammich wrote:
 
  If problems happen again with 4-8 GB JVM heap, you should describe what
  really happens, with clear experimental setup.
 
  Giving a clear experimental setup is a real problem for errors that
  appear nondeterministically.
 
 The first thing is to describe the starting conditions:
 
* Precise CPU model + memory size
vendor_id   : GenuineIntel
cpu family  : 6
model   : 42
model name  : Intel(R) Core(TM) i7-2720QM CPU @ 2.20GHz
stepping: 7
microcode   : 0x1a
cpu MHz : 2194.940
cache size  : 6144 KB
physical id : 0
siblings: 8
core id : 0
cpu cores   : 4
apicid  : 0
initial apicid  : 0
fpu : yes
fpu_exception   : yes
cpuid level : 13
wp  : yes
flags   : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov
pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx
rdtscp lm constant_tsc arch_perfmon pebs bts rep_good nopl xtopology
nonstop_tsc aperfmperf pni pclmulqdq dtes64 monitor ds_cpl vmx smx est
tm2 ssse3 cx16 xtpr pdcm pcid sse4_1 sse4_2 x2apic popcnt
tsc_deadline_timer aes xsave avx lahf_lm ida arat epb xsaveopt pln pts
dtherm tpr_shadow vnmi flexpriority ept vpid
bogomips: 4389.88
clflush size: 64
cache_alignment : 64
address sizes   : 36 bits physical, 48 bits virtual
power management:

+

8Gb of memory, 8Gb of swap space

 
* Operating system
Distributor ID: Ubuntu
Description:Ubuntu 12.04.4 LTS
Release:12.04
Codename:   precise

 
* ML options (heap size, threads)
 

ML_IDENTIFIER=polyml-5.5.2_x86-linux
POLYML_HOME=/home/lammich/.isabelle/contrib/polyml-5.5.2
ML_SYSTEM=polyml-5.5.2
ML_PLATFORM=x86-linux
ML_OPTIONS=-H 500
ISABELLE_POLYML=true

* JVM options (heap size)
JEDIT_JAVA_OPTIONS=-Xms2048m -Xmx4096m -Xss4m

I also attached the output of isabelle getenv -a


 
 The second thing to point the the examples that were used, and give some 
 hints about the concrete situation.

I will try to remember those if it occurs next. 

By the way, another Isabelle/jEdit user at our chair pointed out a
workaround if things seem to be frozen: Just go the beginning of the
current file and make a change there ... this usually wakes up the IDE
again.


--
  Peter


LC_PAPER=de_DE.UTF-8
ISABELLE_TMP_PREFIX=/tmp/isabelle-lammich
CVC3_REMOTE_SOLVER=cvc3
SSH_AGENT_PID=1991
LC_ADDRESS=de_DE.UTF-8
LC_MONETARY=de_DE.UTF-8
ISABELLE_ATP=/home/lammich/devel/Isabelle-devel/src/HOL/Tools/ATP
ML_IDENTIFIER=polyml-5.5.2_x86-linux
ISABELLE_FONTS=/home/lammich/devel/Isabelle-devel/lib/fonts/IsabelleText.ttf:/home/lammich/devel/Isabelle-devel/lib/fonts/IsabelleTextBold.ttf
JEDIT_HOME=/home/lammich/devel/Isabelle-devel/src/Tools/jEdit
Z3_NEW_SOLVER=/home/lammich/.isabelle/contrib/z3-4.3.2pre-1/x86_64-linux/z3
GPG_AGENT_INFO=/tmp/keyring-my6CuJ/gpg:0:1
JEDIT_SYSTEM_OPTIONS=-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true 
-Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle
MIRABELLE_THEORY=Main
EXEC_PROCESS=/home/lammich/.isabelle/contrib/exec_process-1.0.3/x86_64-linux/exec_process
KODKODI_PLATFORM=x86-linux
SHELL=/bin/bash
TERM=xterm
ISABELLE_BUILD_JAVA_OPTIONS=-Xmx1024m -Xss1m
XDG_SESSION_COOKIE=e98a42690e78d743ed7935360007-1403084616.517570-346887857
ISABELLE_IDENTIFIER=
ISABELLE_COMPONENTS_MISSING=
ISABELLE_JDK_HOME=/home/lammich/.isabelle/contrib/jdk-8u5/x86_64-linux
ISABELLE_MAKEINDEX=makeindex
Z3_NEW_HOME=/home/lammich/.isabelle/contrib/z3-4.3.2pre-1/x86_64-linux
ISABELLE_PROCESS=/home/lammich/devel/Isabelle-devel/bin/isabelle_process
Z3_NEW_INSTALLED=yes
ISABELLE_JAVA_EXT=/home/lammich/.isabelle/contrib/jdk-8u5/x86_64-linux/jre/lib/ext
LC_NUMERIC=de_DE.UTF-8
WINDOWID=67827196
ISABELLE_DOCS_RELEASE_NOTES=ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:README_REPOSITORY
MIRABELLE_TIMEOUT=30
GNOME_KEYRING_CONTROL=/tmp/keyring-my6CuJ
ISABELLE_BIBTEX=bibtex
DVI_VIEWER=xdg-open
Z3_REMOTE_SOLVER=z3
REPLY=
ISABELLE_SETTINGS_PRESENT=true
ISABELLE_BUILD_OPTIONS=
MUTABELLE_IMPORT_THEORY=Complex_Main
POLYML_HOME=/home/lammich/.isabelle/contrib/polyml-5.5.2
Z3_COMPONENT=/home/lammich/.isabelle/contrib/z3-3.2-1
GTK_MODULES=canberra-gtk-module:canberra-gtk-module
ISABELLE_PLATFORM_FAMILY=linux
ISABELLE_SLEDGEHAMMER_MASH=/home/lammich/devel/Isabelle-devel/src/HOL/Tools/Sledgehammer/MaSh
ISABELLE_PATH=/home/lammich/.isabelle/heaps:/home/lammich/devel/Isabelle-devel/heaps
USER=lammich
ML_SYSTEM=polyml-5.5.2
LC_TELEPHONE=de_DE.UTF-8

Re: [isabelle-dev] Remaining uses of Proof General?


Some more explanations on the meta-model of this thread:

  * We have about 1 week left on isabelle-dev, to discuss whatever might
prevent using Isabelle/jEdit smoothly, and why people fall-back on PG
as a reflex.

  * Then there will be Isabelle2014-RC0, as a published release candidate,
but *without* forking the Isabelle repository yet.  The same question
and discussion will continue on isabelle-users, for that version, and
as anticipation for Isabelle2014.

  * Then there will be VSL 2014 at Vienna, with the Isabelle workshop,
ITP, UITP and more.  I am myself around 13..18-Jul-2014 (inclusive
interval).  People can show me things personally, to see where the
remaining snags are.

  * Then we are heading towards the Isabelle2014 release, with the normal
Isabelle2014-RC1 and *with* forked repository, shortly after the
ITP/UITP week of VSL.

People who are staying themselves longer at VSL and are involved in
the Isabelle2014 lift-off need to keep this in mind: after the fork
changes need to be sent to me, not pushed onto the main Isabelle
repository.

Some time after the release fork, we can look again what the present 
answer to the ultimate question is: Are there remaining uses of Proof 
General, or is Isabelle2014 the last release that supports it? 
(Hopefully not: Is Isabelle2014 the last release ever?)


The Isar TTY loop and its Proof General add-on has become a big burden in 
recent years -- both are essentially legacy.  So it is worth spending 
extra time to deal with this seriously.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 27 Jun 2014, Peter Lammich wrote:


 * Writing tools in ML (ML-blocks in thy-file)


Just a side remark: in the repository version we are talking about, and 
thus the coming release, ML in auxiliary files works smoothly and often 
better than the ML blocks, because the file gets its own ML mode.


There is nothing wrong about ML blocks, just an equal balance between 'ML' 
and 'ML_file' to choose whatever fits best the size of the ML code module.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-26 Thread Makarius

This is a reminder that this thread is still open, until the end of next 
week when the question will be moved to isabelle-users, with the 
appearance of Isabelle2014-RC0 (that will be published from the running 
repository *without* a repository fork yet).


At the moment (06599233e54e) there are no remaining uses of Proof General 
to the best of my knowledge.  If anybody has counter-examples they should 
be put on the table for discussion.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-26 Thread Peter Lammich

Hi all.

I have given Isabelle/jEdit another try and worked with it for almost
two weeks, on different tasks:
  * Porting the CAVA afp entries (depending on 300 theory files) from
2013-2 to devel.

  * Formalizations and proof development (The standard usage)

  * Writing tools in ML (ML-blocks in thy-file)

I have compiled a list of problems that I encountered during my work.
I have added descriptions to how PG solved these problems.

The problem report here refers to Isabelle version 2ccd6820f74e.

My overall impression is that Isabelle/jEdit is usable but much less
mature than PG:
It does not scale well to large projects, and tends to be unstable.
It has many cool advanced features, but lacks important basic ones. 

However, in my opinion, Isabelle/jEdit is approaching a level of
maturity required for production use, once the user knows about its
deficits and how to avoid them. I will continue using Isabelle/jEdit for
a few more weeks, hoping that a few more basic features will be
added/fixed before the next release ...


SCALABILITY  STABILITY:

* Isabelle/jEdit gets really slow and unresponsive when many files are
loaded (you have to wait seconds for a keystroke to show its effect). As
all prerequisite theories (not in an image) are automatically loaded,
this is unavoidable. In PG, it's no problem to load a theory with many
prerequisites, nor to have many buffers open simultaneously. 

NOTE: This problem could be solved in my case by 1) giving jEdit a
ridiculously large amount of heap space (4Gb) and, 2) using images for
prerequisite theories.

* Isabelle/jEdit does not scale to large files. Error markers on the
right side are only displayed for a context around the current cursor
position. There seems to be no way to jump to the error position. If the
error happens to be displayed as a red bar on the right side of the
editor area, pixel-accurate mousing is required to jump to the error,
and not to a position dozens of lines away.   

In PG, you could always jump to the position where processing failed by
Ctrl-. . Moreover, you got error messages with file names and line
numbers, that you could use to navigate to the error position easily.

* Isabelle/jEdit seems to be quite unstable. Within one week, it
happened several (3 or 4) times that the whole thing just became
unresponsive, and had to be restarted to continue work. In PG, those
things happen perhaps once in a month.

IMPORTANT FEATURES THAT ARE MISSING  OVERLY TEDIOUS WORKFLOWS

* Isabelle/jEdit does not support highlighting of paranthesis in the
output window (it does work in PG!). This is an essential feature to
read bigger goal states. 

Moreover, the output buffer does not support middle-mouse-button
copy-and-paste on my ubuntu-box, while it perfectly works in the editor
window.

* Long list of warnings, e.g. duplicate simp rule, or tracing messages
produced by a method appear before the subgoals in the 
  output, and thus makes them inaccessible without lots of scrolling.
This feature is a real flow-stopper when exploring proofs. 

In PG, it is possible to have separate buffers for the goal-state, the
tracing, and the warning messages, thus you always see the current
subgoal you are working on without scrolling down some buffer every
time.

* If sledgehammer (both over panel and as command) is running, further
processing of the file is blocked/very slow. Thus, it is not possible
to run sledgehammer and, in parallel, continue exploration to find your
own proof. In PG, parallel sledgehammering works, and I used it
extensively. In Isabelle/jEdit I now think twice before I invoke
sledgehammer, because it just interrupts my workflow and I have to wait
for it to finish staring at the sledgehammer-window and doing nothing. 


* Isabelle/jEdit cannot open a theory-file without processing it. This
is in particular a problem when porting stuff and opening the original
version of the same file to look something up. Even worse: Once opened,
you cannot close the file again, and it will remain in the theory panel
(with an error marker) until you quit jEdit.

In PG, it is no problem to open a file without processing it.

* The standard search (Ctrl-F) function does not allow to enter
non-ASCII characters at all. This is a real show-stopper if you search
for a text containing such characters. In PG, you could at least use
\... - tokens to enter non-ASCII characters.

Moreover, I would like an incremental search, but there is probably a
jEdit pluging somewhere? (Probably with the same problems of entering
non-ASCII characters)


* When theories have inconsistent file/theory name, you will only find
the error by stepwise going back the chain of bad theory -  errors,
file by file. This is simply tedious. In PG, you got a backtrace in the
output, and could immediately identify the broken file.


* Auto-Completion does not really work. You have to decide for a
completion delay. If you choose it too short, some completions will
not appear at all. If you

Re: [isabelle-dev] Remaining uses of Proof General?

2014-06-26 Thread John Wickerson

Great list Peter!

 * The standard search (Ctrl-F) function does not allow to enter
 non-ASCII characters at all. This is a real show-stopper if you search
 for a text containing such characters. In PG, you could at least use
 \... - tokens to enter non-ASCII characters.
 
 Moreover, I would like an incremental search, but there is probably a
 jEdit pluging somewhere? (Probably with the same problems of entering
 non-ASCII characters)

There is already an incremental search, but by default it has no keyboard 
shortcut. Myself, I have re-bound Ctrl-F to Incremental Search Bar, and am 
quite happy with that. (This is in jEdit's Global Options, then Shortcuts.)

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Jasmin Christian Blanchette

 (For now the list of Remaining uses of Proof General / Emacs seems to be 
 empty.  If there is anything remaining, this thread is still open to 
 submissions.)

Let me make this list nonempty again.

In the course of a day, I typically find myself pulling from the Isabelle 
repository several times. I am encouraged in this by my use of Mercurial 
queues. So it's not untypical that my HOL image is slightly out of date, 
usually in a harmless way. Sometimes I fire up Proof General just because I 
know it will take the image as is instead of forcing me to rebuild it (and 
waste 4 minutes of my time).

This is not a big issue, and I presume that if Proof General stopped to exist, 
I would adapt my workflow accordingly -- e.g. by getting into the habit of 
rebuilding HOL after each pull. But the above observation is connected with 
Andrei's corridor full of smart people. Sometimes I would just wish 
Isabelle/jEdit could allow me to do the quick-and-dirty things the more 
primitive Proof General allowed -- a I know what I'm doing flag so to speak.

Jasmin

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Makarius


On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:

In the course of a day, I typically find myself pulling from the 
Isabelle repository several times. I am encouraged in this by my use of 
Mercurial queues. So it's not untypical that my HOL image is slightly 
out of date, usually in a harmless way. Sometimes I fire up Proof 
General just because I know it will take the image as is instead of 
forcing me to rebuild it (and waste 4 minutes of my time).


There is already isabelle jedit -n to bypass the automatic build. I 
never use that myself, because I no longer do the bootstrap dependency 
management in my head.


When I do have to step out of the self-build chain of the tool 
infrastructure, e.g. when working on the sources of Isabelle/Pure or 
Isabelle/jEdit sources, I use a separate jEdit editor process that is not 
Isabelle/jEdit. Another option is to use the last official release of 
Isabelle/jEdit to edit a few files elsewhere.



Sometimes I would just wish Isabelle/jEdit could allow me to do the 
quick-and-dirty things the more primitive Proof General allowed -- a I 
know what I'm doing flag so to speak.


I guess it is more I knew how it used to be done in the old times with 
Proof General end Emacs. Isabelle/jEdit does allow much more things than 
was possible before, it only needs to be discovered.


Sometimes my impression is that it would be better to discard Proof 
General on the spot, so that people have free mental energies to work in a 
more productive way with slightly more up-to-date tools.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Jasmin Blanchette


Am 25.05.2014 um 14:59 schrieb Makarius makar...@sketis.net:

 On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
 
 In the course of a day, I typically find myself pulling from the Isabelle 
 repository several times. I am encouraged in this by my use of Mercurial 
 queues. So it's not untypical that my HOL image is slightly out of date, 
 usually in a harmless way. Sometimes I fire up Proof General just because I 
 know it will take the image as is instead of forcing me to rebuild it (and 
 waste 4 minutes of my time).
 
 There is already isabelle jedit -n to bypass the automatic build. I never 
 use that myself, because I no longer do the bootstrap dependency management 
 in my head.

Aha!

-n   no build dialog for session image on startup

I thought this only controlled whether the dialog is shown; not whether the 
build takes place.

Jasmin

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-25 Thread Makarius


On Sun, 25 May 2014, Jasmin Blanchette wrote:


   -n   no build dialog for session image on startup

I thought this only controlled whether the dialog is shown; not whether 
the build takes place.


That was once a separate build_dialog tool, but it is now just an implicit 
build, so I will remove this confusing word.


The build_dialog was meant to let Proof General participate in 
contemporary Isabelle infrastructure, but it was never used and 
discontinued about 1 year ago.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-24 Thread Makarius


On Tue, 29 Apr 2014, Matthew Fernandez wrote:

Currently most of my theories are generated by another tool. When 
debugging the generated theories, I often have to open a file that I 
know contains many broken proofs. In these circumstances it can be 
beneficial to have a way of stepping into the middle of a broken proof 
to explore, while ignoring all the following (also broken) proofs).


In Isabelle/578dc6b4be89 and d11d11da0d90 from about 2 weeks ago there is 
a slightly refined treatment of error recovery, such that continuous 
checking no longer bumps into other toplevel statements / proofs.


That is still not the real thing, just the second round of adhoc 
improvements after the first one in 2010.  Proper structural recovery 
needs to come at some point, with more formal indendation, and the final 
discontinuation of hard tabulators -- not for the coming release, though.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-24 Thread Makarius

This is not a remaining use of Proof General, but of the Emacs text 
editor: trimming the final newline of theory sources for document 
preparation.  This could lead to extra white space between sections in the 
last decades, but it was just one of these habits to take care of that 
manually.


jEdit has its own built-in smartness concerning the last line, and some 
well-known problems coming from it, especially for plugin authors who need 
to paint something into the text buffer.  Since there is no realistic 
chance to remove superfluous newlines manually, Isabelle/5fc1c2098964 now 
does that unconditionally during document preparation.


(For now the list of Remaining uses of Proof General / Emacs seems to be 
empty.  If there is anything remaining, this thread is still open to 
submissions.)



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-13 Thread Andreas Lochbihler


Thanks a lot.

Andreas

On 12/05/14 20:07, Florian Haftmann wrote:

1. Violation of well-sortedness constraints: type ... not an instance of
...

declare [[show_sorts]]
code_thms constant to be exported

Then, I use educated guessing and Emacs' incremental search to navigate
the code equations that have been output until I find the fault --
usually, it's just a missing [code] or [code del] declaration for some
constant that has introduced a quantifier or set comprehension.



I would really appreciate support for navigating code equations in the
output (e.g., Ctrl-click on a constant on the RHS of an equation takes
me to the code equation of that constant (in the output of code_thms).

For this particular case, it would also be useful to get the chain of
propagation for the sort constraint like in GHC (arising from the use of
...), but since Isabelle's code generator strengthens sort constraints
for intermediate functions, this would be a list (tree/graph) of
functions that trace the propagation.


I will have to think about something like that seriously.


Here, I have two suggestions for improvements:

a) Provide an entry to the code preprocessor such that I can trace the
transformation of the code equations for a given (set of) constants.
Currently, I only know how to trace the preprocessing of *all* code
equations, but I am not interested in most of this trace.


I will consider this.


b) [code_abbrev] is the worst code generator attribute that I know of,
because there's no reverse [code_abbrev del]. Each time I have to get
rid of a code abbreviation, I have to figure out once again how
[code_abbrev] transforms the theorem before it calls [code_unfold] and
[code_post]. Please add the [code_abbrev del] attribute.


See now http://isabelle.in.tum.de/repos/isabelle/rev/40213e24c8c4


And while I am at it, here is another point that makes my life
unnecessarily hard, but it's not related to jEdit vs. PG:

3. Problems with Code_Evaluation.term_of and friends

The term reconstruction functions are not displayed in code_thms because
of the section obfuscation in Code_Evaluation. I do not understand why
this has to be obfuscated. I always have to go via export_code and read
the generated code to figure out what the code equation for one of these
overloaded constants is. And it's bad luck if export_code raises an
error because some of the code equations are invalid.


See now http://isabelle.in.tum.de/repos/isabelle/rev/1e50fddbe1f5

Florian


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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-12 Thread Makarius


On Fri, 2 May 2014, Makarius wrote:


On Tue, 29 Apr 2014, Andreas Lochbihler wrote:

Until then there are various approximations:

  * Multiple floating instances of Output, with different Update / Auto
update state.

  * The Output / Detach button to produce an unchanging Info window on the
spot.


In Isabelle/c2ddbf327bbd the former Detach button is now a menu item in 
all dockable windows that support this concept of producing a stand-alone 
Info window from a snapshot of the content.


Since Query and Info already do a good job for keeping track of 
invididual state output, outside the auto-update mode of Output, I was 
wondering if it is time to *discontinue* its special buttons:


   Output / Update
   Output / Auto update

These are remains from early experimental generations of Isabelle/jEdit 
some years ago.  Is anyone actually using that in current repository 
versions, not the last release?



Since former Proof General and Emacs users often prefer keyboard over 
mouse, the following standard jEdit actions might be interesting:


  left-docking-area
  right-docking-area
  top-docking-area
  bottom-docking-area

  close-docking-area

They are bound by default to Emacs-style multi key sequences, e.g.
C+e C+DOWN.

In fact, the similarity to C+e DOWN for subscript in Isabelle/jEdit has 
already caused some confusion to someone trying the latter, and not 
knowing about Emacs ways to treat keyboards.  Thus I learned about the 
existance of the other key sequence in the first place, but also that 
Emacs usage cannot be expected from regular users today.



  Makarius

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-12 Thread Makarius


On Tue, 29 Apr 2014, Thomas Sewell wrote:


 Back to the actual technical questions.  What are the main performance
 bottle-necks here? Printing of intermediate goal states?  Or applying
 intermediate steps repeatedly?


I suspect that the problem is not that the printing or the intermediate 
calculations are taking too long. It's that printing the output the user 
wants to see is waiting on some other computation finishing, creating 
the sensation of lag.


Some evidence to back this up: I tried an adjustment a while ago in 
which I had the goal state print incrementally. Even if some of the 
subgoals took a while to print, you'd see the line with goal (12 
subgoals) immediately, and then the subgoals as they were formatted. 
The short summary is that this helped a little sometimes, but I often 
still saw an empty Output panel for seconds after moving the cursor to a 
line that the continuous checker had already processed.


Fast rewind to the start of this sub-thread, with the standard procedure 
according to Tim the Enchanter:


   * What are your exact hardware parameters: CPU, main memory?

   * What is your operating system?

   * What are your ML system settings, e.g. as shown by isabelle build -? ?

   * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
 JEDIT_JAVA_OPTIONS ?

   * What are the options threads and parallel_proofs ?

To put this into proper context some clues about the actual applications 
would also help to put obscure speculations into the bright light of 
empirical science.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-12 Thread Florian Haftmann

1. Violation of well-sortedness constraints: type ... not an instance of
...

declare [[show_sorts]]
code_thms constant to be exported

Then, I use educated guessing and Emacs' incremental search to navigate
the code equations that have been output until I find the fault --
usually, it's just a missing [code] or [code del] declaration for some
constant that has introduced a quantifier or set comprehension.

I would really appreciate support for navigating code equations in the
output (e.g., Ctrl-click on a constant on the RHS of an equation takes
me to the code equation of that constant (in the output of code_thms).

For this particular case, it would also be useful to get the chain of
propagation for the sort constraint like in GHC (arising from the use of
...), but since Isabelle's code generator strengthens sort constraints
for intermediate functions, this would be a list (tree/graph) of
functions that trace the propagation.

I will have to think about something like that seriously.

Here, I have two suggestions for improvements:

a) Provide an entry to the code preprocessor such that I can trace the
transformation of the code equations for a given (set of) constants.
Currently, I only know how to trace the preprocessing of *all* code
equations, but I am not interested in most of this trace.

I will consider this.

b) [code_abbrev] is the worst code generator attribute that I know of,
because there's no reverse [code_abbrev del]. Each time I have to get
rid of a code abbreviation, I have to figure out once again how
[code_abbrev] transforms the theorem before it calls [code_unfold] and
[code_post]. Please add the [code_abbrev del] attribute.

See now http://isabelle.in.tum.de/repos/isabelle/rev/40213e24c8c4

And while I am at it, here is another point that makes my life
unnecessarily hard, but it's not related to jEdit vs. PG:

3. Problems with Code_Evaluation.term_of and friends

The term reconstruction functions are not displayed in code_thms because
of the section obfuscation in Code_Evaluation. I do not understand why
this has to be obfuscated. I always have to go via export_code and read
the generated code to figure out what the code equation for one of these
overloaded constants is. And it's bad luck if export_code raises an
error because some of the code equations are invalid.

See now http://isabelle.in.tum.de/repos/isabelle/rev/1e50fddbe1f5

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] Remaining uses of Proof General?

2014-05-12 Thread Makarius

The list of remaining uses of Proof General is shrinking dramatically 
every day.  We can continue this a bit more during May, all referring to 
ongoing repository development.


During the month of June, I will be mostly on vacation.  After that the 
convergence towards the release needs to start.  There will be probably 
Isabelle2014-RC0 for the VSL/ITP event at Vienna in mid July, i.e. a 
release candidate *before* the usual fork to the release repository.


Starting with the RC versions for the release, I will pose the same 
question about remaining uses of Proof General on isabelle-users, so that 
everybody can participate.


I have just inspected some old sources by someone else with Isabelle/jEdit 
from Isabelle2012, which was really good and solid back then, but looks 
now old and crappy.  It shows that Isabelle/jEdit has already a long 
history on its own, and it is hardly new, but an established thing.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread Thomas Sewell


Thanks Makarius.

A few of us at NICTA have ported this change to our various versions of 
Isabelle and begun playing with it. It seems to improve the situation 
sometimes, though we haven't yet got a feel for when in particular it 
helps. In fact, we haven't really understood what the change does.


On 07/05/14 22:59, Makarius wrote:

On Mon, 5 May 2014, Makarius wrote:


 Users running on batteries might also want a mode that restricts all
 threads to the behaviour above.


Have you tried that with threads = 1 (there is also a special 
treatment for high-priority prints in that mode)?  So far I guess 
that most people run with defaults, without any idea of the tuning 
parameters.


See also:

changeset:   56875:f6259d6fb565
user:wenzelm
date:Tue May 06 16:05:14 2014 +0200
files:   etc/options src/Pure/PIDE/command.ML
description:
explicit option parallel_print to downgrade parallel scheduling, which 
might occasionally help for big and heavy scripts;



In principle this is an instance of the too many options syndrome, 
but here the implicit change of behaviour on 1 core is merely made 
explicit. Moreover, according to the waterbed-syndrome in its 
positive sense, it means that options added here inevitably cause 
other old/obsolete options to be removed faster.




I completely agree that having too many options is a problem. There's no 
point having them if noone knows that they're there, or which ones to 
try. That said, I think it's a good path for performance adjustments 
which might or might not be helpful. I suspect you could get away with 
adding far more options than you plan to have in the end, and keep only 
the ones that end up with a quorum of users. I'm a bit of an optimist 
though.


This sounds a bit too pragmatic and opportunistic to me.  What is 
special about print tasks anyway, apart from their priority?  The 
recent concept for asynchronous print functions makes print tasks 
rather general, and there are more automated provers or disprovers in 
that category than actual printing.


What is even more important than prints, is the main protocol thread, 
which presently needs to work against the whole farm of worker threads 
to update certain administrative structures of the document model.  If 
I knew a proper way to reduce the priority (or to pre-empt) worker 
threads for that, I would do it.  But it probably needs some work by 
David Matthews on the ML thread infrastructure.




Consider me an unashamed pragmatist. I see a similarity between 
task/thread scheduling in Isabelle and task/thread scheduling in 
operating systems. All modern operating systems are full of ad-hoc 
heuristics designed to bump up the priority of tasks that are likely to 
create I/O requests or update things for the user. A parallel make, 
for instance, will run much faster if the OS prioritises the compile 
tasks that are still reading files ahead of the ones that have begin 
compiling and computing. This keeps the disk working throughout the 
build. Windows raises the priority of in-focus windows, and Mac OS X 
pushes the audio threads of apps up to the highest priority, etcetera.


I may have misspoken with regard to print task. I guess I meant task 
that will produce output which at some point the user has directly 
requested into their output panel, query panel etc. If we see the user 
as an external resource like a hard disk, these are the tasks we need to 
front-load to keep the external task running at full capacity. I see the 
some of the other output tasks, which possibly produce counterexamples 
or which produce squiggly lines which are possibly helpful, as lower 
priority.


Preempting long-running tasks would change the tradeoffs a lot. Another 
possibility would be to introduce a yield-point (cooperative 
multitasking) which a task can execute, which will possibly cause its 
execution to be delayed in favour of a higher priority task. Adding that 
to the tactic combinators would make nearly all Isabelle workloads much 
finer-grained.


Well, those are just my thoughts. Thanks for the adjustment, I hope it 
solves our responsiveness problems.


Best wishes,
Thomas.


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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread Makarius


On Thu, 8 May 2014, Thomas Sewell wrote:


 If I knew a proper way to reduce the priority (or to pre-empt) worker
 threads for that, I would do it.  But it probably needs some work by
 David Matthews on the ML thread infrastructure.


Consider me an unashamed pragmatist.


The important point is that a system like Isabelle cannot be built on the 
basis of pragmatism.  It is occasionally helpful to recall the cultural 
foundations on which one is standing.


The system can be used pragmatically, or rather practically, of course.


I see a similarity between task/thread scheduling in Isabelle and 
task/thread scheduling in operating systems. All modern operating 
systems are full of ad-hoc heuristics designed to bump up the priority 
of tasks that are likely to create I/O requests or update things for the 
user.


Definitely.  I've introduced the slogan of Isabelle as logical operating 
system already in 2007, when the parallel batch mode with its ML threads 
was still new.  Many years later that has become reality in PIDE 
interaction, but it was much harder to get there than anticipated.  In 
recent years I have become more cautious in the ambitions of what the 
system is meant to do. It is already too far ahead of anything else in the 
ITP world, and hardly anyone understands how it really works.



A parallel make, for instance, will run much faster if the OS 
prioritises the compile tasks that are still reading files ahead of the 
ones that have begin compiling and computing. This keeps the disk 
working throughout the build.


Luckily Isabelle no longer depends on make and its many historical 
problems.  The Isabelle build tool is fast, because it does not access all 
these files over and over again.  Thus the need for extra tricks is 
avoided, by giving up old habits from the 1970-ies.



Preempting long-running tasks would change the tradeoffs a lot. Another 
possibility would be to introduce a yield-point (cooperative 
multitasking) which a task can execute, which will possibly cause its 
execution to be delayed in favour of a higher priority task. Adding that 
to the tactic combinators would make nearly all Isabelle workloads much 
finer-grained.


That sounds rather obvious, but also like even more complication.  David 
Matthews has provided a nice simplified version of pthreads in Poly/ML. 
He could probably do more, but even on the more complex JVM the influence 
on thread scheduling is limited.


My canonical approach in such situations is to ask: Is there a way to 
avoid the need for all that extra weight?  It requires looking at concrete 
applications carefully, to disprove their approach as something that 
could be done differently, with less impact on resources.


That is not pragmatic, but it is how genuine scientific progress usually 
works.



Makarius

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread David Matthews


On 08/05/2014 11:25, Makarius wrote:

On Thu, 8 May 2014, Thomas Sewell wrote:


 If I knew a proper way to reduce the priority (or to pre-empt) worker
 threads for that, I would do it.  But it probably needs some work by
 David Matthews on the ML thread infrastructure.


Preempting long-running tasks would change the tradeoffs a lot.
Another possibility would be to introduce a yield-point (cooperative
multitasking) which a task can execute, which will possibly cause its
execution to be delayed in favour of a higher priority task. Adding
that to the tactic combinators would make nearly all Isabelle
workloads much finer-grained.


That sounds rather obvious, but also like even more complication.  David
Matthews has provided a nice simplified version of pthreads in Poly/ML.
He could probably do more, but even on the more complex JVM the
influence on thread scheduling is limited.


I've had a look at providing thread priority in the Poly/ML thread 
package and I may have a go at including something.  Poly/ML leaves 
thread scheduling to the pthreads library which really means to the OS 
and what is available depends on the particular OS.  In general pthreads 
allows control over both priority and scheduling policy.  I've done 
some tests on what various OSs allow for user (i.e. non-privileged) threads.

Linux. Does not allow either policy or priority to be changed.
Mac OS X.  Allows both policy and priority to be changed.
Cygwin/Windows.  Single scheduling policy.  Allows priority to be changed.
FreeBSD.  Allows priority but not policy to be changed.

What this means is that ML code that wants to set a thread priority is 
going to have to make some enquiries about the priority range allowed.


It looks as though adding a yield function would not be hard.  There's 
a question about whether you would really want to use it.  There is a 
cost involved even if there is no other thread that can be scheduled so 
you wouldn't want to call it too often.


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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-07 Thread Makarius


On Mon, 5 May 2014, Makarius wrote:


 Users running on batteries might also want a mode that restricts all
 threads to the behaviour above.


Have you tried that with threads = 1 (there is also a special treatment for 
high-priority prints in that mode)?  So far I guess that most people run with 
defaults, without any idea of the tuning parameters.


See also:

changeset:   56875:f6259d6fb565
user:wenzelm
date:Tue May 06 16:05:14 2014 +0200
files:   etc/options src/Pure/PIDE/command.ML
description:
explicit option parallel_print to downgrade parallel scheduling, which 
might occasionally help for big and heavy scripts;



In principle this is an instance of the too many options syndrome, but 
here the implicit change of behaviour on 1 core is merely made explicit. 
Moreover, according to the waterbed-syndrome in its positive sense, it 
means that options added here inevitably cause other old/obsolete options 
to be removed faster.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-07 Thread Makarius


On Fri, 2 May 2014, Makarius wrote:


On Tue, 29 Apr 2014, Andreas Lochbihler wrote:


   text ‹
  @{term ‹A \un B›}
   ›
 
   Here the \un works as expected -- the cartouche remains intact

   independently of its
   content, as long as the funny parentheses are nested properly.
 But this correct nesting is exactly the problem. When I type \un while
 writing the above, the closing parenthesis are not there yet. The prover
 sees something like

 text {* @{term A \un

 lemma foo: ... by ...


But why? In the ancient times, input was always sequential, as depth-first 
traversal of the intended tree structure.  In less ancient times, some people 
proposed rigid structural editors to make it impossible to escape from nested 
boxes (still seen today in TeXmacs), although that is a bit awkward.  In the 
past 10 years or so, the standard IDE approach has arrived somewhere in the 
middle: the user is free to type intermediate non-sense, but the editor makes 
it easy to get it right by default.


See also:

changeset:   56842:b6e266574b26
user:wenzelm
date:Sat May 03 20:31:29 2014 +0200
files:   src/Tools/jEdit/etc/options 
src/Tools/jEdit/src/completion_popup.scala

description:
yet another completion option, to imitate old less ambitious behavior;


It allows to ignore the language context of the prover.

This is also an attempt to retain sanity, when masses of users complain 
about having to learn new things in the coming release.  Hopefully some 
will do some actual testing of this big space of features, and report 
problems before the release and not after it.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-05 Thread Makarius


On Mon, 5 May 2014, Thomas Sewell wrote:


 The basic assumption is that each proof task does not run too long, and if
 it does it is something to be improved in the application to make it more
 smooth.  In contrast, Proof General makes it more easy to produce huge and
 heavy proof scripts that can be hardly handled by anyone else later.



Right. That seems to be the assumption that's being violated in the few 
cases where people are still keen on ProofGeneral, for instance, in 
Andreas' big complicated tactic applications.


One needs to understand two important things here: technology and 
psychology.


15 years ago, there were certain technological side-conditions both in the 
prover and in Emacs, which made Proof General what it is.  Later people 
got used to that and optimized their workflow accordingly.  Certain 
manual task scheduling became second nature to them.


5 years ago, the prover was quite different and the JVM + Scala + jEdit 
platform imposed other technological side-conditions of what can be 
done.  Again, people need to get used to that and optimize their 
workflow, but in addition one needs to unlearn old habits from Proof 
General,


This psychological factor makes it difficult to see the genuine technical 
problems that still need to be addressed.  As usual it helps to show the 
actual situation, either just the sources, or a video of the usual 
workflow, or a demonstration with personal presence.



Let me make a proposal. I think that various users would appreciate it 
if one of the worker threads was reserved for print jobs caused by 
moving the cursor (highest priority tasks) and their dependencies 
(assuming more than one worker thread). That would hopefully make it 
easier to control the delay. If the user is cautious with moving the 
cursor and if enough proof dependencies have been processed, the system 
*should* be as responsive as PG. The delay would also be mostly 
unaffected by the proof task runtime, only the print task runtimes, 
which might be easier for an advanced user to manage.


This sounds a bit too pragmatic and opportunistic to me.  What is special 
about print tasks anyway, apart from their priority?  The recent concept 
for asynchronous print functions makes print tasks rather general, and 
there are more automated provers or disprovers in that category than 
actual printing.


What is even more important than prints, is the main protocol thread, 
which presently needs to work against the whole farm of worker threads to 
update certain administrative structures of the document model.  If I knew 
a proper way to reduce the priority (or to pre-empt) worker threads for 
that, I would do it.  But it probably needs some work by David Matthews on 
the ML thread infrastructure.



Users running on batteries might also want a mode that restricts all 
threads to the behaviour above.


Have you tried that with threads = 1 (there is also a special treatment 
for high-priority prints in that mode)?  So far I guess that most people 
run with defaults, without any idea of the tuning parameters.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-04 Thread Thomas Sewell


On 03/05/14 00:05, Makarius wrote:

On Tue, 29 Apr 2014, Thomas Sewell wrote:

I tried an adjustment a while ago in which I had the goal state print 
incrementally. Even if some of the subgoals took a while to print, 
you'd see the line with goal (12 subgoals) immediately, and then 
the subgoals as they were formatted. The short summary is that this 
helped a little sometimes, but I often still saw an empty Output 
panel for seconds after moving the cursor to a line that the 
continuous checker had already processed.


I strongly suspect that the print request was waiting in a queue 
somewhere. The system would become responsive again once it finished 
doing something else.


That is the normal future task farm, with its restricted worker thread 
pool.  All PIDE execution works via some Future.fork, with different 
priorities in the queue.  Proof tasks have low priority, print tasks 
have high priority. Once a task is running on some thread, it 
continues and cannot be preempted by newer tasks with higher priority.


The basic assumption is that each proof task does not run too long, 
and if it does it is something to be improved in the application to 
make it more smooth.  In contrast, Proof General makes it more easy to 
produce huge and heavy proof scripts that can be hardly handled by 
anyone else later.




Right. That seems to be the assumption that's being violated in the few 
cases where people are still keen on ProofGeneral, for instance, in 
Andreas' big complicated tactic applications.


The case where I get into trouble is in implementing a package-lite. I 
put together a collection of tactics or computations in ML blocks and 
execute them at some point in a theory via setup or ML. It's a bit like 
setting up a proper package and invoking it, but without the implied 
robustness or generality. Some of these can run for a minute or longer. 
They're the kind of computations that users might want to control.



With regard to the future task farm: This is pretty much what I'd 
expected. So we see a delay if all the available threads are executing 
tasks that take a while and are not the current print task. Adding more 
threads reduces the chance of this happening, but not much. The higher 
priority for print tasks means the delay will end as soon as any thread 
becomes available, so the more threads the faster on average that will 
happen, but without guarantees.


Let me make a proposal. I think that various users would appreciate it 
if one of the worker threads was reserved for print jobs caused by 
moving the cursor (highest priority tasks) and their dependencies 
(assuming more than one worker thread). That would hopefully make it 
easier to control the delay. If the user is cautious with moving the 
cursor and if enough proof dependencies have been processed, the system 
*should* be as responsive as PG. The delay would also be mostly 
unaffected by the proof task runtime, only the print task runtimes, 
which might be easier for an advanced user to manage.


Users running on batteries might also want a mode that restricts all 
threads to the behaviour above.


As always, I have no idea how difficult that would be.



On incremental printing: it's easy to implement by generalising a 
couple of the relevant Pretty operations to produce a Seq.seq 
internally rather than a list.


That would probably violate some implicit assumptions about print 
modes, which are a slightly odd intrusion into the purity of Pretty.T.


What was the reason for incremental printing anyway?  Just performance 
for huge goal states?  There are other bottle-necks concerning that, 
and if goals really do get that big one should think about other ways 
to expose them, not by printing in the old-fashioned way.


Incrementality might have other reasons and actual benefits.  In the 
early years of PIDE I had more ambitions for that, but it caused so 
many additional problems in the document model and the GUI that I 
removed most of it for the sake of delivering something that is 
sufficiently stable to be usable in practice.


The reason for the experiment was that I was fixing some proofs 
somewhere, I forget where, which had relatively fast tactics executing 
on large, slow-to-print goals. I was probably in a context where Simpl 
was loaded, where printing is slower than usual (probably the 
print/parse translations, I've had a look and got nowhere.)


It occurred to me that I could debug some of my mistakes faster if I 
just knew whether or not the tactic I'd typed had solved a goal, and 
many more if I just saw the first goal. But the time saved is probably 
lost again adjusting the goals limit, and it's annoying to do by hand. 
Incremental output seemed like a good idea.




It looked promising initially, but then became really annoying, 
because Isabelle/jEdit or PIDE resets the Output buffer each time it 
gets more to display. So if you scroll down to look for something, 
you get scrolled back up for each time a

Re: [isabelle-dev] Remaining uses of Proof General?


On Tue, 29 Apr 2014, Thomas Sewell wrote:

I tried an adjustment a while ago in which I had the goal state print 
incrementally. Even if some of the subgoals took a while to print, you'd 
see the line with goal (12 subgoals) immediately, and then the 
subgoals as they were formatted. The short summary is that this helped a 
little sometimes, but I often still saw an empty Output panel for 
seconds after moving the cursor to a line that the continuous checker 
had already processed.


I strongly suspect that the print request was waiting in a queue 
somewhere. The system would become responsive again once it finished 
doing something else.


That is the normal future task farm, with its restricted worker thread 
pool.  All PIDE execution works via some Future.fork, with different 
priorities in the queue.  Proof tasks have low priority, print tasks have 
high priority. Once a task is running on some thread, it continues and 
cannot be preempted by newer tasks with higher priority.


The basic assumption is that each proof task does not run too long, and if 
it does it is something to be improved in the application to make it more 
smooth.  In contrast, Proof General makes it more easy to produce huge and 
heavy proof scripts that can be hardly handled by anyone else later.



On incremental printing: it's easy to implement by generalising a couple 
of the relevant Pretty operations to produce a Seq.seq internally rather 
than a list.


That would probably violate some implicit assumptions about print modes, 
which are a slightly odd intrusion into the purity of Pretty.T.


What was the reason for incremental printing anyway?  Just performance for 
huge goal states?  There are other bottle-necks concerning that, and if 
goals really do get that big one should think about other ways to expose 
them, not by printing in the old-fashioned way.


Incrementality might have other reasons and actual benefits.  In the early 
years of PIDE I had more ambitions for that, but it caused so many 
additional problems in the document model and the GUI that I removed most 
of it for the sake of delivering something that is sufficiently stable to 
be usable in practice.



It looked promising initially, but then became really annoying, because 
Isabelle/jEdit or PIDE resets the Output buffer each time it gets more 
to display. So if you scroll down to look for something, you get 
scrolled back up for each time a subgoal prints, which can give the 
sensation that the editor is fighting you.


There is a deeper conceptual problem here.  Several independent entities 
want to update content of some GUI component: output window, tree view 
etc.  This requires a merge of these change of the GUI state, but that 
is usually only done by a hard reset on one side, ignoring the other side. 
You can see that in jEdit's SideKick tree view, Isabelle/jEdit's Output 
dockable with scrollbar and folds, or even just in a plain Terminal with 
the scrollbar.



Makarius

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

Re: [isabelle-dev] Remaining uses of Proof General?


On Tue, 29 Apr 2014, Andreas Lochbihler wrote:


 text ‹
@{term ‹A \un B›}
 ›

 Here the \un works as expected -- the cartouche remains intact
 independently of its
 content, as long as the funny parentheses are nested properly.
But this correct nesting is exactly the problem. When I type \un while 
writing the above, the closing parenthesis are not there yet. The prover sees 
something like


text {* @{term A \un

lemma foo: ... by ...


But why? In the ancient times, input was always sequential, as depth-first 
traversal of the intended tree structure.  In less ancient times, some 
people proposed rigid structural editors to make it impossible to escape 
from nested boxes (still seen today in TeXmacs), although that is a bit 
awkward.  In the past 10 years or so, the standard IDE approach has 
arrived somewhere in the middle: the user is free to type intermediate 
non-sense, but the editor makes it easy to get it right by default.


Isabelle/jEdit still lacks serious templating, but there are beginnings of 
it in the completion mechanism. The outer quotations and antiquotations 
have specific support already: a single keystroke ` offers a template for 
a well-formed cartouche, and the @{ prefix completes to a well-formed @{} 
with the cursor in the middle.  Even Proof General had C-c C-a C-a for 
isar-antiquote already.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Tue, 29 Apr 2014, Andreas Lochbihler wrote:

There are hardly any performance problems in terms of computing power, 
possibly except for Isabelle processing a slow call to auto over and 
over again. The efficiency problem is the interaction with the IDE. I 
use the Find panel a lot, but then my output panel is not visible at the 
same time (that's why I would like to split the right dock in two). And 
when I scroll upwards to find a snippet of tactic script that I want to 
copy, the output updates and my current goal state is gone.


The mechanics of the Output panel are a bit old-fashioned, still assuming 
a single-focus proof script model.  At some point I would like to see a 
proper Preview of a certain part of proof document, with state output 
just in the right spots (zero or more depending on proof structure).


Until then there are various approximations:

  * Multiple floating instances of Output, with different Update / Auto
update state.

  * The Output / Detach button to produce an unchanging Info window on the
spot.

  * The more flexible docking framework provided by the MyDoggy plugin,
although it is unclear if that is more than a nice experiment by one
of the old-time jEdit developers.


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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-02 Thread Andreas Lochbihler


On 02/05/14 16:16, Makarius wrote:

On Tue, 29 Apr 2014, Andreas Lochbihler wrote:


 text ‹
@{term ‹A \un B›}
 ›

 Here the \un works as expected -- the cartouche remains intact
 independently of its
 content, as long as the funny parentheses are nested properly.

But this correct nesting is exactly the problem. When I type \un while writing 
the
above, the closing parenthesis are not there yet. The prover sees something like

text {* @{term A \un

lemma foo: ... by ...


But why? In the ancient times, input was always sequential, as depth-first 
traversal of
the intended tree structure.  In less ancient times, some people proposed rigid 
structural
editors to make it impossible to escape from nested boxes (still seen today in 
TeXmacs),
although that is a bit awkward.  In the past 10 years or so, the standard IDE 
approach has
arrived somewhere in the middle: the user is free to type intermediate 
non-sense, but the
editor makes it easy to get it right by default.
I have used such templating mechanism with Eclipse and finally disabled them, because they 
caused me more work than what they saved. I usually prefer to enter both delimiters 
separately and to just see the matching parenthesis highlighted.


The reason is that I often add the delimiters only later. For example, when I write a 
single-identifier term, I use


text {* @{term my_constant} *}

and some time later, I figure out that I have to add something, e.g., a type constraint. 
Hence, I produce the following sequence of edits (the # denotes the position of the cursor)


text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}

With the template mechanisms that I have seen so far, I get the following 
sequence:

text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}

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

Re: [isabelle-dev] Remaining uses of Proof General?


On Fri, 2 May 2014, Andreas Lochbihler wrote:

The reason is that I often add the delimiters only later. For example, when I 
write a single-identifier term, I use


text {* @{term my_constant} *}

and some time later, I figure out that I have to add something, e.g., a type 
constraint. Hence, I produce the following sequence of edits (the # denotes 
the position of the cursor)


text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}

With the template mechanisms that I have seen so far, I get the following 
sequence:


text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}


I think the second form is not proper templating yet, just an escape hatch 
of the IDE to produce balanced quotes by default, since it is more often 
correct that the other way round.


The Isabelle text cartouches are an attempt to get rid of unbalanced 
quotes altogether, and reduce the problem to one of balanced parentheses. 
My ` completion is already better than the above, because it allows to 
select all 3 cases: balance template, left side, right side.


jEdit has already nice actions to select a code block, depending on the 
structure of parentheses.  What is missing are ways to add or remove an 
outermost pair of parentheses, which should not be too difficult to add. 
Independently of code blocks, the Isabelle/jEdit actions to modify control 
symbols already work with selections in a structured way.  The completion 
mechanism also knows a bit about the various forms of selection, and tries 
to do something sensible with them.


The abobe example could be also handled by a double-click to select the 
word of my_constant, and then perform a still hypothetical operation to 
enclose it in quotes of some form.



Note that when I say jEdit it refers to the jEdit text editor, while the 
Prover IDE is called Isabelle/jEdit.  Getting the basic terminology right 
helps to avoid confusion about what happens where, and who is ultimately 
responsible for it.


We have an increasingly complex situation of many Isabelle sub-languages 
and sub-systems, but being explicit about that is better than sweeping it 
under the carpet.  In contrast, the Coq guys have upheld the illusion of 
one main language longer, and actually removed their quotes around the 
term language long ago, and thus introduced many problems that persist 
until today.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-01 Thread Florian Haftmann

 But I try to process such
 theories with jEdit and only go back to XEmacs/PG when I cannot stand
 Isabelle/jEdit any longer (which usually happens when I debug the code
 generator setup).

That's an interesting observation.  What are the particular properties
of »debugging« here that make PG preferable?  Maybe it is just a
question of better code generation tool support.

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] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler

Hi Makarius,

On 28/04/14 23:10, Makarius wrote:

a) Given some text like

definition foo where foo = ...

when I add an attribute like [simp]: after the where, I get a symbol completion
popup to
replace the : with the element sign. Usually, my next thing is to move the
cursor with
the cursor keys. But the popup gobbles all the key strokes until I explicitly
close it
with ESC. As colons are used everywhere in Isabelle's outer syntax, it would
really be
great if the popup only appears when I am in inner syntax.

b) Sometimes, when I write a HOL term, I used to not get the completion popup
when I
enter something like \un if there were sufficiently many parse errors in that
partial
term. Even Ctrl-b did not help. However, I cannot reproduce it in a small
example at the
moment.

In the case a), I guess that you still have the completion delay 0.0, while I
presently
work with 0.5 to give the prover a chance to add semantic completion
information, before
any popups are shown.
My completion delay is 0.1. When writing Isabelle terms normally, this is the amount of
time that does not break my flow of typing.

text ‹
@{term ‹A \un B›}
›

Here the \un works as expected -- the cartouche remains intact independently of
its
content, as long as the funny parentheses are nested properly.
But this correct nesting is exactly the problem. When I type \un while writing the above,
the closing parenthesis are not there yet. The prover sees something like

text {* @{term A \un

lemma foo: ... by ...

What is funny is that Proof General was actually one of the main reasons of
moving only
slowly in such token language reforms.
I am glad that PG still works for most of my theories and I try to keep that state as long
as feasible. There are already problems with new keywords declared by AFP entries that are
not listed in the keywords file. I then usually insert ; as a delimiter. But I try to
process such theories with jEdit and only go back to XEmacs/PG when I cannot stand
Isabelle/jEdit any longer (which usually happens when I debug the code generator setup).

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler


On 28/04/14 23:18, Makarius wrote:

On Mon, 28 Apr 2014, Andreas Lochbihler wrote:


2. Reactivity when processing large files

With PG, I knew how to control the Isabelle prover. When I edit a large file in 
a larger
project like JinjaThreads, every now and then, Isabelle changes the background 
colour
from red to gray and then, apparently nothing happens for minutes before 
Isabelle turns
it red again and starts reprocessing. Is there some way to explicitly tell 
Isabelle that
it should now start to check again. Toggling continuous checking does not 
help.
Sometimes, I even have to close the theory file and reopen it again.


This sounds like the Poly/ML RTS is desparately trying to reclaim memory, by 
aggressive
sharing huge amounts of data.  Not long ago that situation lead into real 
memory problems
on my good old 32 GB machine, but David Matthews managed once again to postpone 
the
ultimate JinjaThreads implosion as a black hole of computing resources.

For now just the usual game, according to Tim the Enchanter:

   * What are your exact hardware parameters: CPU, main memory?

Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory


   * What is your operating system?

Ubuntu 12.04 LTS


   * What are your ML system settings, e.g. as shown by isabelle build -? ?

ML_PLATFORM=x86-linux
ML_HOME=~/.isabelle/contrib/polyml-5.5.1-1/x86-linux
ML_SYSTEM=polyml-5.5.1
ML_OPTIONS=-H 500


   * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
 JEDIT_JAVA_OPTIONS ?
JEDIT_JAVA_OPTIONS=-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4 
-Dactors.enableForkJoin=false



   * What are the options threads and parallel_proofs ?

threads = 0, parallel_proofs = 2

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler

On 28/04/14 22:25, Makarius wrote:

On Mon, 28 Apr 2014, Andreas Lochbihler wrote:

My main usage of PG is when I want to construct a complicated proof method call
like

(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp
del: ...)+

that collapses an apply script of a hundred lines. I haven't yet found a
convenient way
to write the apply script in Isabelle/jEdit, because of reactivity issues (see
item 2
below) and the continuous updates of the output window (when I scroll to some
other part
of the apply script using the cursor keys). Are there key bindings for
scrolling that do
not move the cursor?

This reminds me of a very old insider jokes from the mid-1990-ies: Dieter
Nazareth had
finished the W0 formalization where he had turned half-decent tactic scripts
into such
compact one-liners, and shortly afterwards Wolfgang Naraschewski had to
disentangle that
again for the full W formalization, or rather start from scratch. A few years
later, the
Isar language emerged and made that approach in principle obsolete.
I know, I have myself untangles such one-liners often enough when something has changed.
Nevertheless, I believe that I'm still faster to build these one-liners than write pretty
Isar proofs of hundreds of lines, just because the goal states are huge and all cases are
shown in the same way.

Back to the actual technical questions. What are the main performance
bottle-necks here?
Printing of intermediate goal states? Or applying intermediate steps
repeatedly?
There are hardly any performance problems in terms of computing power, possibly except for
Isabelle processing a slow call to auto over and over again. The efficiency problem is the
interaction with the IDE. I use the Find panel a lot, but then my output panel is not
visible at the same time (that's why I would like to split the right dock in two). And
when I scroll upwards to find a snippet of tactic script that I want to copy, the output
updates and my current goal state is gone. (I know I could disable the updating, but then
I have to enable it manually again.)

I can say more when I understand the actual problem better. In such situations
I normally
have to see the dynamics of how you actually work.

Maybe I can show you what my problems are at ITP in Vienna in July.

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread René Neumann

 What is funny is that Proof General was actually one of the main
 reasons of moving only
 slowly in such token language reforms.
 I am glad that PG still works for most of my theories and I try to keep
 that state as long as feasible. There are already problems with new
 keywords declared by AFP entries that are not listed in the keywords
 file.

'isabelle keywords $SESSION' can be used to generate a new keywords file
with all keywords of $SESSION.

- René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Makarius


On Tue, 29 Apr 2014, Andreas Lochbihler wrote:


* What are your exact hardware parameters: CPU, main memory?

Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory


That is a recent high-end laptop or a midrange desktop machine. 
JinjaThreads is *the* biggest Isabelle application on the planet, it 
deserves a proper workstation or server, lets say with 8 cores and 16 GB 
minimum (which is still small by today's standards).




ML_PLATFORM=x86-linux
ML_HOME=~/.isabelle/contrib/polyml-5.5.1-1/x86-linux
ML_SYSTEM=polyml-5.5.1
ML_OPTIONS=-H 500


That is OK for batch mode, but in interactive mode the GC time of the 
Poly/ML RTS will be quite noticable.


I will make a few experiments with x86_64 and some real memory beyond 16 
GB, and report my experience later.




* What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
  JEDIT_JAVA_OPTIONS ?
JEDIT_JAVA_OPTIONS=-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4 
-Dactors.enableForkJoin=false


This looks OK for that situation.  Note that you can strip the actors 
properties, since I have removed that altogether some days ago (e.g. 
326e8a7ea287).  The new JVM thread pool is hardwired to the *virtual* 
number of CPU cores, which is a bit high by default, but it is not used 
very much in Isabelle/Scala.




* What are the options threads and parallel_proofs ?

threads = 0, parallel_proofs = 2


Here we have the standard overloading / overheating of Intel hyperthreaded 
CPUs.  I reckon that most users have that problem, and experience bad 
reacticity that I never see myself, because I know more about multicore 
system tuning.


The maximum that makes sense on this hardware is threads = 4, as well as

  ML_OPTIONS=-H 500 --gcthreads 4

In the next Poly/ML release, David Matthews provides the means to have 
this as default.



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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Andreas Lochbihler

Hi Makarius,

Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and
ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to
working on small projects or refactoring existing sources. I really like the negative line
spacing setting and completion of fact names! Thanks!

My main usage of PG is when I want to construct a complicated proof method call
like

(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp
del: ...)+

that collapses an apply script of a hundred lines. I haven't yet found a convenient way to
write the apply script in Isabelle/jEdit, because of reactivity issues (see item 2 below)
and the continuous updates of the output window (when I scroll to some other part of the
apply script using the cursor keys). Are there key bindings for scrolling that do not move
the cursor?

Here are some things that could be improved in Isabelle/jEdit (I am currently on
Isabelle/4e2a0d4e7a82):

1. Symbol completion in PG was absolutely deterministic. The immediate symbol completion
in jEdit works great, too, I merely had to learn new sequences of key strokes. Symbol
completion of non-unique results is not satisfactory.

a) Given some text like

definition foo where foo = ...

when I add an attribute like [simp]: after the where, I get a symbol completion popup to
replace the : with the element sign. Usually, my next thing is to move the cursor with the
cursor keys. But the popup gobbles all the key strokes until I explicitly close it with
ESC. As colons are used everywhere in Isabelle's outer syntax, it would really be great if
the popup only appears when I am in inner syntax.

b) Sometimes, when I write a HOL term, I used to not get the completion popup when I enter
something like \un if there were sufficiently many parse errors in that partial term. Even
Ctrl-b did not help. However, I cannot reproduce it in a small example at the moment.

2. Reactivity when processing large files

With PG, I knew how to control the Isabelle prover. When I edit a large file in a larger
project like JinjaThreads, every now and then, Isabelle changes the background colour from
red to gray and then, apparently nothing happens for minutes before Isabelle turns it red
again and starts reprocessing. Is there some way to explicitly tell Isabelle that it
should now start to check again. Toggling continuous checking does not help. Sometimes,
I even have to close the theory file and reopen it again.

3. Navigation between theories files

In PG, I usually have only a small subset of the loaded theories and ML files open as
buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I use Ctrl-` to
go to the previous file, but going to a different one is a pain, because I have to search
it in the complete list of open files.

It would be great if there was a list of just those files that I had on my screen
previously, not all loaded files.

Moreover, when I close a file and then press Ctrl-` in the file that shows up, I do not
get to the file I have visited before the two, but to some arbitrary other. Can jEdit
remember the order in which files have been visited? XEmacs at least does this.

Maybe there are already solutions to the above annoyances, I just don't know them. There's
another thing I would like to see in jEdit: The window layout has three columns (one dock
on the left and one on the right) and the middle column (with the editor area) can be
divided in three rows (dock - text - dock). Is there some way that I can split the right
column into two rows to show two information areas at the same time (e.g. Output at the
top and Find below)?

Andreas

On 27/04/14 20:14, Makarius wrote:

Are there any remaining uses of Proof General, e.g. in the situation of current
Isabelle/5b6f4655e2f2 ?

This is neither a joke nor a running gag -- I just can't think of anything
myself after
the introduction of the spell checker.

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] Remaining uses of Proof General?

2014-04-28 Thread Peter Lammich

I'm still a regular user of PG. From time to time, I test
Isabelle/jEdit, and my reasons for switching back to PG are somewhat
similar to what Andreas reported. My main problems with Isabelle/JEdit
are:

1. I cannot really control what Isabelle/Jedit processes when, and it
invests computation power on the meaningless parts of the file
directly after the point where I am editing. I'm not even convinced that
it is the right approach to let Isabelle/jEdit's heuristics decide when
and what it processes, and make user intervention impossible at first
place (Or even worse, force the user into workarounds like inserting
semicolons or ends behind the current editing point, which seems to be
common practice among Isabelle/jEdit users)

2. In PG, when the processed region reaches the end of a theory file, I
can be pretty sure that everything is fine with this theory. In
Isabelle/jEdit, I have to scan the theory status panel manually for
remaining red or pink bars, which is very inconvenient for large
projects with hundreds of files.

Moreover, I find it a bit scary that severe errors related to
Isabelle/jEdit's document processing model (cf.
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00170.html)
can go undiscovered for several month, although most Isabelle users are
on Isabelle/jEdit these days. I ask myself: Have they got so used to
strange behaviours of the IDE that they do not realize severe errors any
more?


--
  Peter





On Mo, 2014-04-28 at 09:14 +0200, Andreas Lochbihler wrote:
 Hi Makarius,
 
 Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle 
 time (and 
 ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great 
 when it comes to 
 working on small projects or refactoring existing sources. I really like the 
 negative line 
 spacing setting and completion of fact names! Thanks!
 
 My main usage of PG is when I want to construct a complicated proof method 
 call like
 
 (fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... 
 simp del: ...)+
 
 that collapses an apply script of a hundred lines. I haven't yet found a 
 convenient way to 
 write the apply script in Isabelle/jEdit, because of reactivity issues (see 
 item 2 below) 
 and the continuous updates of the output window (when I scroll to some other 
 part of the 
 apply script using the cursor keys). Are there key bindings for scrolling 
 that do not move 
 the cursor?
 
 
 Here are some things that could be improved in Isabelle/jEdit (I am currently 
 on 
 Isabelle/4e2a0d4e7a82):
 
 1. Symbol completion in PG was absolutely deterministic. The immediate symbol 
 completion 
 in jEdit works great, too, I merely had to learn new sequences of key 
 strokes. Symbol 
 completion of non-unique results is not satisfactory.
 
 a) Given some text like
 
 definition foo where foo = ...
 
 when I add an attribute like [simp]: after the where, I get a symbol 
 completion popup to 
 replace the : with the element sign. Usually, my next thing is to move the 
 cursor with the 
 cursor keys. But the popup gobbles all the key strokes until I explicitly 
 close it with 
 ESC. As colons are used everywhere in Isabelle's outer syntax, it would 
 really be great if 
 the popup only appears when I am in inner syntax.
 
 b) Sometimes, when I write a HOL term, I used to not get the completion popup 
 when I enter 
 something like \un if there were sufficiently many parse errors in that 
 partial term. Even 
 Ctrl-b did not help. However, I cannot reproduce it in a small example at the 
 moment.
 
 
 2. Reactivity when processing large files
 
 With PG, I knew how to control the Isabelle prover. When I edit a large file 
 in a larger 
 project like JinjaThreads, every now and then, Isabelle changes the 
 background colour from 
 red to gray and then, apparently nothing happens for minutes before Isabelle 
 turns it red 
 again and starts reprocessing. Is there some way to explicitly tell Isabelle 
 that it 
 should now start to check again. Toggling continuous checking does not 
 help. Sometimes, 
 I even have to close the theory file and reopen it again.
 
 
 3. Navigation between theories files
 
 In PG, I usually have only a small subset of the loaded theories and ML files 
 open as 
 buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I 
 use Ctrl-` to 
 go to the previous file, but going to a different one is a pain, because I 
 have to search 
 it in the complete list of open files.
 
 It would be great if there was a list of just those files that I had on my 
 screen 
 previously, not all loaded files.
 
 Moreover, when I close a file and then press Ctrl-` in the file that shows 
 up, I do not 
 get to the file I have visited before the two, but to some arbitrary other. 
 Can jEdit 
 remember the order in which files have been visited? XEmacs at least does 
 this.
 
 
 Maybe there are already solutions to the above annoyances, I just don't know

Re: [isabelle-dev] Remaining uses of Proof General?


On Mon, 28 Apr 2014, Matthew Fernandez wrote:


On 28/04/14 04:14, Makarius wrote:

 Are there any remaining uses of Proof General, e.g. in the situation of
 current
 Isabelle/5b6f4655e2f2 ?


I'm mostly on Isabelle/jEdit now, but I do delve back into 
Isabelle/Emacs (is that the current terminology for this creature?)


I don't know all details about the terminology, which is also slightly 
varying over time.  There are Isabelle tools called emacs and jedit 
after the underlying text editors, which I introduced myself some years 
ago, alongside with isabelle tty (which actually uses rlwrap as editor 
if that is available).


isabelle emacs invokes Proof General or Isabelle Proof General (in 
contrast to the Coq version), or Proof General Emacs (in contrast to the 
Eclipse version) -- David Aspinall could explain that more precisely.  I 
used myself wrongly ProofGeneral over many years, and David never told 
me that until it was rather late, but I changed that habit afterwards.


isabelle jedit starts Isabelle/jEdit.  This was once a tiny Isabelle 
plugin for the jEdit text editor (so the distinction did not exist yet), 
but is now a rather big IDE based on jEdit and a lot of extra 
functionality provided by the plugin + a few JVM bootstrap tricks. 
Regular users of official releases also get a native application wrapper 
that was newly introduced in Isabelle2013-2, and is different from the 
jEdit distribution.



My reasons are mostly predictable execution, as I can control what the 
prover is up to with explicit stepping forwards and backwards. I can 
probably achieve the same result toggling continuous checking on/off in 
Isabelle/jEdit, but haven't invested the time in modifying my workflow.


Can you say more about typical situations?  When doing occasional 
debugging, either of tools or the system itself, I need more knowledge 
about what happens when exactly.  I never do this in Proof General these 
days, but within the Prover IDE in a buffer that contains only the main 
items of interest.  Then I edit carefully, based on educated guesses how 
the PIDE document model works, or I toggle the continuous checking that 
was newly introduced in Isabelle2013-2.



I've also encountered the problems discussed in other threads of the 
Isabelle/jEdit GUI locking up when some tactic is looping and the JVM 
heap being exhausted with no indication from the UI.


I reckon that this refers to the official Isabelle2013-2 release.  I have 
reworked many details of scheduling in the past few months, even just now 
when writing this email.  When the Isabelle2014-RC line starts (probably 
in July) you should look precisely at your typical applications to see how 
it works.  I don't want to see again a situation where problem reports 
trickle only slowly *after* the release is shipped.



Isabelle/Emacs is capable of running on underpowered machines which do 
not have enough resources to run Isabelle/jEdit. This is not a good 
reason for maintaining legacy support, but there may be users in this 
situation.


It is a normal sign of stagnation of some application that it suddenly 
runs blazingly fast on old or tiny hardware.  At ITP 2013 last summer I've 
seen a few Coq users working comfortably with CoqIDE or Proof General on 
netbooks are small laptops.  That surely can't be done with a full-scale 
Prover IDE like Isabelle/jEdit. When Proof General was young and strong, 
it was also huge and bloated compared to the hardware of that time, 
escpecially XEmacs was really heavy and we had many insider jokes about 
that.


The relation of hardware vs. software performance is not an accident, but 
the result of the normal balancing of trade-offs: How much functionality 
can we afford on a certain range of hardware at the moment?  I routinely 
walk through consumer electronics stores like Fnac Paris, to see what you 
get for 500..1000 EUR, to estimate what can be expected from typical 
users.  Then I test on 3 systematically on 3 dissimilar systems, 2 of them

actually  3 years old.


What I normally don't test is unplugged battery mode, because I am in the 
lucky situation of not commuting.  People who do that routinely, should 
make some systematic experiments with the nominal number of Isabelle/ML 
threads at 0.5 of the true number of cores, i.e. 0.25 of the virtual 
number of cores on Intel.  To simplify the calculation, just try the 
constant threads = 1 an see how it works.


Last summer at Rennes, someone was surprised to have a 2 core laptop 
running at 600% CPU, but it actually turned out a new i7 with 8 virtual 
CPUs.  The defaults were just burning down the batteries, without any 
extra benefit in those warm summer days.



Makarius

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

Re: [isabelle-dev] Remaining uses of Proof General?


On Mon, 28 Apr 2014, Andreas Lochbihler wrote:

My main usage of PG is when I want to construct a complicated proof method 
call like


(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... 
simp del: ...)+


that collapses an apply script of a hundred lines. I haven't yet found a 
convenient way to write the apply script in Isabelle/jEdit, because of 
reactivity issues (see item 2 below) and the continuous updates of the output 
window (when I scroll to some other part of the apply script using the cursor 
keys). Are there key bindings for scrolling that do not move the cursor?


This reminds me of a very old insider jokes from the mid-1990-ies: Dieter 
Nazareth had finished the W0 formalization where he had turned half-decent 
tactic scripts into such compact one-liners, and shortly afterwards 
Wolfgang Naraschewski had to disentangle that again for the full W 
formalization, or rather start from scratch.  A few years later, the Isar 
language emerged and made that approach in principle obsolete.



Back to the actual technical questions.  What are the main performance 
bottle-necks here? Printing of intermediate goal states?  Or applying 
intermediate steps repeatedly?


As you move the cursor over commands, the Output updates itself, without 
any activity from the prover.  The prover prints states as you change the 
editor view, e.g. by scrolling or resizing the window. You can disable the 
Auto-update of the Output dockable, but that does not affect the proof 
process, only the display.


You can prevent the prover from burning cycles either by reducing the 
number of worker threads, or disabling the continuous checking.


I can say more when I understand the actual problem better.  In such 
situations I normally have to see the dynamics of how you actually work.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Mon, 28 Apr 2014, Andreas Lochbihler wrote:


a) Given some text like

definition foo where foo = ...

when I add an attribute like [simp]: after the where, I get a symbol 
completion popup to replace the : with the element sign. Usually, my 
next thing is to move the cursor with the cursor keys. But the popup 
gobbles all the key strokes until I explicitly close it with ESC. As 
colons are used everywhere in Isabelle's outer syntax, it would really 
be great if the popup only appears when I am in inner syntax.


b) Sometimes, when I write a HOL term, I used to not get the completion 
popup when I enter something like \un if there were sufficiently many 
parse errors in that partial term. Even Ctrl-b did not help. However, I 
cannot reproduce it in a small example at the moment.


We should move anything concerning completion on specific threads on this 
mailing list, with explicit subject what it is about.  It will take quite 
some time for the coming release to stabilize in that respect.  There are 
a bit too many ambitious and smart mechanisms involved here.



For now just a few notes.

In the case a), I guess that you still have the completion delay 0.0, 
while I presently work with 0.5 to give the prover a chance to add 
semantic completion information, before any popups are shown.  That 
includes a no_completion markup produced by the prover, specifically for 
things like :, although this introduces a real danger of 
non-determinism.


The gobbling of key events by the popup should not happen, but there are 
some uncertainties due to key event workarounds in jEdit, and workarounds 
around these in Isabelle/jEdit.  The basic idea is that the popup consumes 
exactly those key strokes that are relevant to it, and passes everything 
else to the main text area -- this is also what jEdit usually does.  This 
behaviour has fluctuated concerning cursor left and right keys several 
times, and I need to check this once again soon.


For current 9c3f0ae99532 I confirm that the first cursor left/right event 
is indeed absorbed.



Case b) with \foo sequences happens whenever there is some semantic 
completion context and string literals involved: backslash sequences 
destroy the string token, and thus may change the context again. Here is 
an example:


text {*
  @{term A \un B}
*}

The language context for 'text' disables symbol completion, because it is 
in conflict with latex macros, as just seen on the thread on 
isabelle-users Symbol Shortcuts vs. LaTeX code.  The antiquotation 
changes the language context again to allow symbols, but the malformed 
string A \un B breaks that, and it falls back into the enclosing text 
context.  So the \un cannot be completed.


One of the motivations for backslash escapes is to make them different 
from usual legal input, but exactly that causes the problems here. I have 
started to think about making bad string tokens more acceptable to certain 
language layers, but that is once again an extra complication.



A different approach is to use new cartouche syntax instead, which 
addresses old issues of quotation robustness and escape confusion 
uniformly.  Using that token syntax, the above example becomes this:


text ‹
  @{term ‹A \un B›}
›

Here the \un works as expected -- the cartouche remains intact 
independently of its content, as long as the funny parentheses are nested 
properly. There is a different error, though: the term parser does not 
accept outer cartouche tokens yet.  It could allow that, but I found this 
too ambitious as a start for the new syntax.



What is funny is that Proof General was actually one of the main reasons 
of moving only slowly in such token language reforms.  We are back again 
in a dead-lock situation, and not the first time in the past few years. 
Leaving the old Emacs world behind more decisively would free a lot of 
hidden resources, and that could have been done at least 2 years ago 
without any regrets.


Of course there is no fundamental problem of Proof General supporting 
cartouches.  There was once special code for nested comments that could be 
reactivated.  The point is that somebody would have to do something, and 
not just expect that software magically maintains itself.



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

Re: [isabelle-dev] Remaining uses of Proof General?


On Mon, 28 Apr 2014, Andreas Lochbihler wrote:


2. Reactivity when processing large files

With PG, I knew how to control the Isabelle prover. When I edit a large 
file in a larger project like JinjaThreads, every now and then, Isabelle 
changes the background colour from red to gray and then, apparently 
nothing happens for minutes before Isabelle turns it red again and 
starts reprocessing. Is there some way to explicitly tell Isabelle that 
it should now start to check again. Toggling continuous checking does 
not help. Sometimes, I even have to close the theory file and reopen it 
again.


This sounds like the Poly/ML RTS is desparately trying to reclaim memory, 
by aggressive sharing huge amounts of data.  Not long ago that situation 
lead into real memory problems on my good old 32 GB machine, but David 
Matthews managed once again to postpone the ultimate JinjaThreads 
implosion as a black hole of computing resources.


For now just the usual game, according to Tim the Enchanter:

  * What are your exact hardware parameters: CPU, main memory?

  * What is your operating system?

  * What are your ML system settings, e.g. as shown by isabelle build -? ?

  * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
JEDIT_JAVA_OPTIONS ?

  * What are the options threads and parallel_proofs ?


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

Re: [isabelle-dev] Remaining uses of Proof General?