Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE

On 1/9/2016 9:00 AM, Makarius wrote:
Have you tried Isabelle2016-RC0 already?

It provides many new things concerning document markup and markdown. Very few LaTeX macros are remaining. Since you are using creative add-ons to Isabelle document preparation, there is also a chance that something stops working.

Now is still a chance to work it out. Later in the release process, further changes will be less likely.



Thanks for the notice. I would have also sent this direct to you, but I was unsubscribed. Moderated emails can take a while to get to the list, and I prefer to keep things in sync.

(Important first things: No, I haven't installed it, which requires the long explanation. I'm hoping to have my expectations fulfilled on the "many new things". Specifically, that "\<^emph>" produces real italicsin the PIDE. As to what "\<^verbatim>" looks like, I have no idea what to expect.

Judicious use of bold and italic can be huge in helping the eyes sort through dense "code". The other things I'll look forward to are more bullet-like symbols.

About two years ago, I asked for an italic font. If that somehow influenced you, thanks for eventually providing the feature. If you forgot about that, thanks anyway. I always keep in mind that the foundation and work on Isar, as a graphical language, started at least 10 years before I discovered Isabelle.

The benchmark for any new, graphical addition is the cartouche delimiters. I think those are the single, most important contribution that will ever be made in relation to "visible markup". A tangent on that would be my opinions about non-visible, WYSIWYG, Mathematica-style "markup". Having worked with Mathematica a little, I don't desire that kind of setup, with its huge learning curve, and use of binary files for documents. (If the PIDE was like that, though, it might actually be good.)

I believe your mix of non-visible markup with visible markup, in a text document, reaches some happy, practical compromise. WYSIWYG editors, for word processors and HTML editors, have caused me tons of grief. Commonly, I would have big explosions of the text, when editing things like bullet lists.)


Pertinent is some history about Donal Knuth being compulsive about fonts with TeX, and about how Steve Jobs was compulsive about how the Mac looked. Both of them where influenced by "artistic things". (Includes some history about the long dev process of Knuth's TeX, heavily related to fonts.) (The Mac and Steve Jobs. Some stories about him being compulsive about detail, in relation to calligraphy.)

I'll put you in their category as far as having demonstrated technical, artistic ability, which is not the same as me saying you're an artist, since "artist" generally means something different. You would have to say whether you think you're an artist.

I said the above as part of saying that, at this point, nothing I do from here on out has anything to do with the quality of what you've produced, or with any particular design choice you make or have made, such as your particular choice for symbols and markup.

I can't explain much, because it's all about a 4 year evolution, which started about September, 2011, which was when I did my experiments to try and put all the source in a THY into a verbatim environment, and then run the THY through the document build. It didn't work; I guess it's related to the need to run the source through the prover engine; at this point, I don't care about the reasons.

That was the start of use of the scripting language of WinEdt to do things myself, and use Windows MikTex to build the PDF from the THY.

My opinions about the PDF appearance, when theorems and proofs are formally stated with Isabelle/Isar, mixed in with English and traditional use of LaTeX math formulas, can be represented by these two things, though there are many other things involved:

1) I insist on heavy use of the \newtheorem environment, in very specific ways.

2) I insist on the use of the fancyverb package with \newtheorem, in very specific ways.

I attach two screen shots. What those show are my "modeling" of the use of a newtheorem environement title, which is followed by the THY source in a fancyverb environment.

I'm repeating what I've said before, but to emphasize what I've said even more, for the PDF "model" of my THY, these are a must. They are not optional.

I would rather have only a THY, looking something like I show, than also have a PDF, but not THY "modeling" of a PDF document with a "newtheorem environment look".

At this time, you cannot provide me with THY markup that's similar to what I show, that will also a produce a PDF through 'isabelle build'.

If you don't provide me with one single thing that I need, then I have to do it all. My "official start point" was May 2012. My point for a willingness to do things the "Isabelle way" came to an end, somewhere within two to three years of my start point.

I have to produce something. To produce something I have to commit to something specific. I don't care about the perfect way of doing anything anymore. The chance to do things the "Isabelle distribution way" came and went. Surely, even 3.5 years is too long to have to spend just to get to where I can get an understanding of what I might should do.

I don't blame anyone. If you want a reason, it's that there's not enough education material to ensure that people's energy gets channeled. That there's documentation, yes there is, or I wouldn't have started all this.


If I wrote a book here, it wouldn't get read, and it would take me a lot of work, so I shorten all this.

On the user list, I don't want to be the face of the non-PhD Isabelle user community. Just guessing, it appears there might be 10 active, non-dev users in the world, who are not part of the high-attrition group who keep cycling through here and on SO.

I put it at 10 to be safe. There could be a lot of lurkers, but probably not. So, maybe it's 3, who have stuck with it for over 1-2 years.

That's related to my not wanting to be a user who obtains high visibility because I post, and because other users don't post or don't post much.

So, I don't install so that I don't post. If I install, and find a problem, I'll want to post about. I don't want to post, so I don't install.

I can't be a good team player. That's the way it has to be.

Thanks for a great product. If it comes to your attention that I have railed heavily against Isabelle, whatever it means, it doesn't mean that Isabelle is not the best proof assistant in the world that uses simple types. To say "the best" would imply there's something even close. There's not, which makes it even more impressive.

As to simple types, in comparison to dependent types, I think I learned this: type inference, it's huge when it comes to readability, at least when foundational clutter can be hidden, which is a lot of the time. But it's whatever a person needs.

For now, any success with proof assistants, by anyone, in any way, with any product, tweaked in any way, with any type system... that success will benefit every other player in the realm of proof assistants.

If a particular user doesn't succeed, it will probably be because the user went unheard. In that case, it won't matter what the user did, whether they did things different, or did things the same.

Oh yeah, I almost forgot to provide the all-important images. Three things:

1) The PDF is to provide the world a self-contained document, that's independent of the software.

2) The readability of the THY is to provide myself a document that I enjoy reading.

3) The readability of the THY is also to make it easy to present the contents of the THY to the world, such as with videos on Youtube. Frequent presentations are only practical if there's not much preparation overhead.

The PDF can be sacrificed at the beginning. At the end, when it's time to check out, it becomes everything. If it ends up that the PDF can't be read purely for the ideas that it contains, then Isabelle, for me, will all have been a total waste of time.

A book-form of an answer here would be talking more about the significance of what's in the image. One image shows some programming with JavaScript in the PIDE. The other image shows some logic.

Correction opportunity: I formerly said "a tip" to credit Manual Eberl for explanations on StackOverflow, on how to tap into "CARD" for the 'vD' shown, and how to use the dummy(?) variable. The datatype 'vD' will be big for me, but only if I can get to it.

Getting to things, in general, for me, is a big problem in relation to the upper limit of mortality. But then, I thinks that applies to everyone.


On 1/9/2016 9:00 AM, Makarius wrote:
On Sat, 14 Nov 2015, Gottfried Barrow wrote:

1) A TeX file, full of LaTeX commands, isn't readable.

2) When a THY is marked up heavily in LaTeX, the THY isn't readable.

3) Should I go further? Isar commands, such as 'subsubsection', which are fashioned after the corresponding LaTeX commands, contribute nothing to readability, and in fact, hinder readability, just like LaTeX.

This is not criticism on my part. It's a reflection of what has been important to you, given that you prioritize according to what you want.

My goal? Eliminate all use of LaTeX from THY documents (other than a few infrequently used commands), and moreover, eliminate "verbose" Isar commands that distract from readability.

Here's a LaTeX command from ML.thy: \begin{verbatim}

A LaTeX verbatim command like that will never be in my THY. In my THY, verbatim environment markup never has to be used, except for the few places outside of a newtheorem environment, and there the syntax is reasonably subtle.

Have you tried Isabelle2016-RC0 already?

It provides many new things concerning document markup and markdown. Very few LaTeX macros are remaining. Since you are using creative add-ons to Isabelle document preparation, there is also a chance that something stops working.

Now is still a chance to work it out. Later in the release process, further changes will be less likely.


Attachment: 160110a_node_simd.png
Description: PNG image

Attachment: 160110a_vD.png
Description: PNG image

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