Email Gateway (Aug 18 2022 at 19:55): Email Gateway (Aug 18 2022 at 19:55):From: gottfried.barrow@gmx.com
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.
I don't need either of those, but it would be nice to get all the
information features that PG provides through the menus, such as "show
types". This is because I would like to exclusively work in Cygwin jEdit.
Below, I reference a mailing list thread, and I give my input, but I'll
make my request first.
REQUEST: It would be nice to have a help file that gives a short
description of what the commands do that correspond with the many Proof
General menu commands, such as "show types". Additionally, in the help
file, it would be nice to have a screenshot which shows me what
additional information I'm supposed to be looking for when I perform the
command.
All that would take time, so I expect that I'll be firing up Proof
General, looking for menu commands that give me useful information, and
asking the mailing list what command I use to get that information in
the source file.
Now, some details from a thread:
Tobias asked, "How can I see the possible cases in an induction, i.e.
Show me cases in PG?"
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02677.html
Consequently, Larry asked for menus in jEdit that provides such things:
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02681.html
Markarius says it's non-trivial to implement diagnostic functions in the
Isabelle/jEdit engine:
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02683.html
Brian Huffman says
@@http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02678.html@@:
You can type the command "print_cases" into your theory file (this
also works in PG).
But then the real question is, how do we expect new users to discover
this feature?
Brian's comment described and describes my situation. I knew I wanted to
see types, and that PG would show types, and that "show_types" was being
talked about in the tutorial, but I didn't know how to get jEdit to show
me types.
I eventually figured out how to do it.
To show types in jEdit, I insert this command:
declare [[show_types]], or
ML{* Config.put show_types true;*}
However, I don't know where I found how to do those commands. I've done
a grep on the Isablle distribution folder, and though I find
"show_types" in certain PDFs, I don't find anything that explicitly
tells me how to use it. This kind of thing is a problem for a newbie:
I'm on page 3 of the tutorial, I want to see types, I know that Proof
General's menus can activate showing types, but I don't want to use
Proof General, I want to use jEdit.
Having a description of all the commands like "show_types" would be
useful even if the Isabelle/jEdit engine had a menu system like Proof
General. Inserting a series of commands like "declare [[show_types]]"
into the source code would be useful when creating templates. It would
also be useful to be able to put those commands into a source file
that's imported by other source files.
As to menus that would insert these commands into the source code,
that's very simple to create in jEdit. Any folder and macro files I put
in my USER_HOME "Isabelle2012\jedit\macros" will show up under the
jEdit/Macros dropdown menu.
Here's a screenshot of my jedit/macros folder. I've created a macro for
"declare [[show_types]]":
jEdit allows you to record macros, but all I did was copy a line of
macro code from another macro file. Inside "declare [[show_types]].bsh"
is this line of code:
textArea.setSelectedText("declare [[show_types]]");
Through jEdit Options/jEdit/Shortcuts, I assigned a shortcut to this
macro. I can delete and insert the command to my heart's content. After
I get past page 3 of the tutorial, and I create a foundational theory
that everything else imports, I might put these kind of commands in my
foundational theory.
To summarize, it would be nice to have a list of commands like
"show_types" with a description of what they do, and a screenshot
showing the info they provide, if someone has the time to do that.
--GB
Email Gateway (Aug 18 2022 at 19:55):From: Makarius <makarius@sketis.net>
On Wed, 23 May 2012, gottfried.barrow@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.
Moreover, jEdit is particular good at searching text files, see its
"hypersearch". Emacs traditionally sucks in that respect.
Having a description of all the commands like "show_types" would be
useful even if the Isabelle/jEdit engine had a menu system like Proof
General.
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
It is the most authentic and most up-to-date of Isabelle/Isar manuals.
You can see what Proof General emits on the isabelle process buffer, and
then look up the command in the manual. This does not really work for the
stateful things, though. For "show_types" you should read the general
explanations about "configuration options" in the isar-ref manual, and
maybe use 'print_configs' to get an idea what is available. The isar-ref
manual also has a formally generated index with hyperlinks.
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
Email Gateway (Aug 18 2022 at 19:55):From: gottfried.barrow@gmx.com
On 5/23/2012 5:58 PM, Makarius wrote:
On Wed, 23 May 2012, gottfried.barrow@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
Email Gateway (Aug 18 2022 at 19:55):From: Lars Noschinski <noschinl@in.tum.de>
You can use the "find_theorems" command for that (which is the same PG
uses, but jEdit does not provide a menu item for it).
-- Lars
Email Gateway (Aug 18 2022 at 19:56):From: gottfried.barrow@gmx.com
Thanks, Lars. I didn't find "find_theorems" in any of the docs, but I
found some examples here:
http://www.cse.unsw.edu.au/~cs4161/10s2/Demo12.thy
I also found "src/Pure/Tools/find_theorems.ML". I'm trying to study some
ML, so maybe I'll figure out completely how to use it from that file.
And there's also a short note in "Isabelle Primer for Mathematicians",
http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf
The command is better than the Proof General menu command anyway.
Thanks again,
GB
Email Gateway (Aug 18 2022 at 19:57):From: gottfried.barrow@gmx.com
Being in the habit of using the Acrobat search is what messed me up. The
phrase "find_theorems" is listed in the index, but I had searched on
"find", and it didn't show up in the search, so I didn't even think
about the index. "Reliable" is the key word; searching on "show types"
in Acrobat had found me some "show_types".
Thanks,
GB
Email Gateway (Aug 18 2022 at 19:57):From: Lars Noschinski <noschinl@in.tum.de>
Many PDF viewers choke on "fi", as generates an fi-ligature instead of
two letters f and i.
-- Lars
Email Gateway (Aug 18 2022 at 19:59):From: gottfried.barrow@gmx.com
In a PDF, I frequently highlight text and do a CNTL-b to create a
bookmark, so I've seen over and over that "fi" in the text gets
converted to a symbol similar to what Prince used when he became "The
Artist Formerly Known as Prince."
However, it never occurred to me that "fi" in a word would cause
problems with Acrobat search. Now I know. Thanks, because Acrobat search
is useful if I know its limitations.
--GB
Email Gateway (Aug 18 2022 at 19:59):From: Lars Noschinski <noschinl@in.tum.de>
On 30.05.2012 18:35, gottfried.barrow@gmx.com wrote:
On 5/29/2012 2:29 AM, Lars Noschinski wrote:
On 26.05.2012 03:58, gottfried.barrow@gmx.com wrote:
Being in the habit of using the Acrobat search is what messed me up. The
phrase "find_theorems" is listed in the index, but I had searched on
"find", and it didn't show up in the search, so I didn't even think
about the index.Many PDF viewers choke on "fi", as generates an fi-ligature instead of
two letters f and i.
[...] as [LaTeX] generates [...]
However, it never occurred to me that "fi" in a word would cause
problems with Acrobat search. Now I know. Thanks, because Acrobat search
is useful if I know its limitations.
[1] suggests that this problem can be solved at document generation
time. Maybe this is worth investigating.
-- Lars
Email Gateway (Aug 18 2022 at 19:59):From: Makarius <makarius@sketis.net>
I didn't know yet that Acrobat Reader could cause such extra problems.
Which version is it?
The tiny Sumatra PDF browser that is now bundled with Isabelle2012 seems
to be able to find and copy paste "find theorems" (without underscore) in
isar-ref.pdf without problems. You get that by default when you invoke
"isabelle doc isar-ref" in the Cygwin-Terminal. See also
http://blog.kowalczyk.info/software/sumatrapdf/free-pdf-reader.html
Just on the day of the Isabelle2012 announcement Sumatra PDF was updated,
which now causes some odd invitation to update when starting up the first
time. The positive aspect is that this project seems to be quite active,
so that the Windows platform now gets a PDF rendering engine of equal or
better quality than Poppler on Linux.
Makarius
Email Gateway (Aug 18 2022 at 19:59):From: gottfried.barrow@gmx.com
I use Adobe Acrobat Pro X, which is the version that lets you edit the
PDFs. When I do a search on "find" in isar-ref.pdf, only "Find" on page
221 is found. I get the same results with Adobe Reader X.
I did searches with two other PDF readers: STDU Viewer
<http://www.stdutility.com/stduviewer.html>, and PDF-XChange Viewer
<http://www.tracker-software.com/product/pdf-xchange-viewer>.
The STDU Viewer search returns the same results as Adobe. The
PDF-XChange Viewer search finds lots of "find", including "find
theorems" for the command "find_theorems".
On page 30, I selected "finding" in the 3 PDF viewers and the 1 PDF
editor mentioned above. I copied the text into a text file. Here's what
I get:
?nding (PDF-XChange)
?nding (STDU Viewer)
nding (Adobe Reader X)
nding (Adobe Acrobat Pro X)
Which is not what I really got in the text editor. There were two
non-"f" or non-"i" characters preceding "nding" for Adobe.
It appears it's as Lars says about the "fi", and PDF-XChange does some
extra work to find the "fi" in a word, and Acrobat doesn't.
--GB
Email Gateway (Aug 18 2022 at 19:59):From: Makarius <makarius@sketis.net>
I've done investigations occasionally over the years -- it is an old and
well-known problem, and still waiting for really good solutions.
My last attempt was stopped in winter 2011, see
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2012/doc-src/pdfsetup.sty
with the critical \iffalse to disable the "experimental treatment of
replacement text".
I had first started with cmap as recommended on the above stackexchange.
One of the aspects mentioned in that thread is old OT1 vs. T1. I had
other motivations than "fi" ligatures to use T1, but it did not work out
for two reasons, IIRC: (1) conflict with the rail package for syntax
diagrams, (2) lack of scalable cm fonts for T1.
Point (1) no longer applies, since @{rail} is now an Isabelle
antiquotation (see the isar-ref manual for its documentation).
Point (2) -- status unknown. Maybe some improvements have emerged in the
meantime.
in 2010/2011 I ended up trying something completely different, using
"ActualText" markup for PDF. It essentially allows to define a plain text
model for the rendered text. This is a nice idea, but most browsers still
have problems with it. Trying it again just now with the above
pdfsetup.sty and \ifpdf instead of \iffalse to activate the markup, it
produces the following result for isar-ref.pdf of Isabelle2012:
http://www4.in.tum.de/~wenzelm/test/isar-ref.pdf
Using latest Acrobat Reader 10.1.3 in Windows 7 on the Isar proof on page
10/11 and copy/pasting into Isabelle/jEdit works almost:
+ Isabelle symbols fine, but need to be decoded on target
+ hidden quotes around inner syntax fine, but sometimes odd extra spaces
- indentation is lost
- page header gets in the way
- fi ligatures don't work, e.g. "finally"
Sumatra PDF 2.1 just ignores the ActualText markup, but is able to copy
the "finally" correctly :-)
Over all these years there has been a tension of HTML vs. PDF. I
originally preferred proof documents with proper typesetting and
pagination, but this now gets in the way for fully formal online text.
My hope is that someone who really understands HTML4/CSS2 or HTML5/CSS3
could give some hints how to make high-quality rendering of formal
documents like the Isabelle manuals, or any other Isabelle document
from applications.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC