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:

    (?x)
    (class|definition|lemma|lemmas|name|theorem)[\s]+.*
    (
    (?<![a-z])multiply
    )

Virtually all Isabelle/Isar language elements are explained in the bulky isar-ref manual, see also http://isabelle.in.tum.de/dist/Isabelle2012/doc/isar-ref.pdf
...
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.

    Makarius

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 it has.

But in my pursuit for the best proof assistant, I did a little research on Lamport's TLA+2 (http://research.microsoft.com/en-us/um/people/lamport/tla/tla2.html).

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,
GB








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.