Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features
On 5/23/2012 5:58 PM, Makarius wrote:
On Wed, 23 May 2012, gottfried.barrow at gmx.com wrote:
While experimenting, I saw that Linux Proof General provides certain
things that jEdit doesn't. Two being that the external provers work,
and that Linux PG can do searches on the Isabelle source code.
Can you explain what you mean? What exactly does not work?
The sledgehammer suite should work smoothly in Isabelle/jEdit of
Isabelle2012. It has been tested many times, and there have been many
calls to report problems over several weeks.
I was talking about Cygwin Proof General and jEdit for Isabelle2011. In
either one, the provers either never came back with a message, or they
came back with a timed-out message. Occasionally, they would return the
results of what they could or couldn't prove. In Linux Proof General,
the provers would start to return the results after a few seconds. I
haven't tried any external provers in Isabelle2012. I'm interested in
Isabelle as a theorem assistant.
Moreover, jEdit is particular good at searching text files, see its
"hypersearch". Emacs traditionally sucks in that respect.
I was talking about Proof General's feature to search the Isabelle logic
theories for a keyword in the lemma names, theorem names, definition
names, etc.. (Would that be the "Find Theorem" menu command?) I haven't
seen that I can do that in jEdit. I use PowerGREP and a regular
expression to search on the complete src/HOL folder. One like this:
Virtually all Isabelle/Isar language elements are explained in the
bulky isar-ref manual, see also
Note that PDF files produced by Latex cannot be searched reliably for
anything outside A-Za-z0-9. So "show types" might work, but
"show_types" not. Complain to Don Knuth and Leslie Lamport about not
using proper ASCII by default.
Ah, so "reliably" explains everything. In Acrobat, searching on
"show_types" works in this isar-ref.pdf,
http://isabelle.in.tum.de/doc/isar-ref.pdf, which was created in
January, 2011, and which I found now using Google to search on
"show_types" and "isar-ref.pdf", but it doesn't work for Acrobat when
searching in the latest 2012 isar-ref.pdf.
LaTeX is too amazing and generous as a product for me to complain to the
primary authors. Complaining about that would be like me complaining to
you about Isbelle when there's a decent workaround for some deficiency
But in my pursuit for the best proof assistant, I did a little research
on Lamport's TLA+2
Somewhere in my research, I read that it was using Isabelle as one of
the provers, but to do the proving automatically. That's nice, I
suppose, if you want automatic proving. For me, at this point, automatic
proving is not what I want. The great thing about Isabelle is that it
can do automatic proving, but it's also a proof assistant.
Thanks for the info,
This archive was generated by a fusion of
Pipermail (Mailman edition) and