[isabelle] Session run errors but no PIDE errors


As a formality, I state that I prefer no feedback, not that anyone wants to give it, but if given feedback, I'll not respond to it, a suboptimal formality, but necessary. That others might discuss what I report, I don't concern myself with that.

This email is to show an example of what I had mentioned, that I can scroll to the bottom of my THY and no errors show up in the right-vertical-status-bar, but there are errors in my THY.

Before I was doing periodic session runs, this was a huge source of consternation. Now that I'm doing sessions runs, it's not a problem at all, it's a part of finding problems with the normal workflow.

I wouldn't report this, but I don't recall seeing a report about this.

(1) Below, I describe the circumstances surrounding the error, and to support that, I attach a screenshot.

(2) As a tangent to my talk about defining outer syntax commands, I state some opinions about the configurability of Isar, as a front-end language to a powerful logic engine, and front-end to powerful proof tools, namely Sledgehammer, Nitpick, and the slew of proof methods, along with the absolute essential ability to perform single proof steps with natural deduction. But back to the configurability of Isar as a language,

a) that the configurabilityis a great feature of Isabelle/HOL as a software product,

b) another feature being the configurability of inner syntax, part of that being a good selection of graphical symbols,

c) and another feature being a PIDE that allows these features to be what they are, where from my observations, these front-end features are near exclusively because of one person, M.Wenzel, with whom I have no affiliation, formally or informally, and did I forget to mention the proof language as a front-end feature?

  d) There is also the Isar proof language as a front-end feature.

e) Quoting myself from the past, everyone either gets too little credit, or way too much. You work to blow your horn, and I'll work to blow mine.

(3) As part of (2), I say that I hope the configurability of Isar/Isabelle/HOL doesn't get locked down just to try and control the language. Fragmentation of language is only bad if the fragmentation destroys good unity or prevents eventual good unity. Locking something down can prevent innovation, and prevent people experimenting to find the best way to use a language.


What I did was eliminate a custom outer syntax synonym for 'term'. This resulted in some errors that I was notified about, and I changed those uses of the eliminated synonym. I then scrolled to the bottom of the theory, at which time I ran the session command with the very useful 'I.prog'. When I did that, the console notified me of errors.

In the image, it can be seen that the upper part of the right-vertical-status-bar is light purple. I suppose the light-purple means that area wasn't rechecked.

As to PIDE options, the only change I remember, concerning this, is "Editor Reparse Limit 20000", where originally it is '10000'. It seems a bigger number there would make it better, but it may not matter. Before, I had it at '100000', and I got these errors, which is why I made an effort to implement session runs.

It's not a problem. I report it to alert anyone who would care, and so that M.Wenzel knows, though there's a good chance he already knows about something like this.


To say much more is to belabor the point of (3) above.

I define any outer syntax I want, to get synonyms for the normal syntax. Even so, it takes a lot of experimenting to find syntax that actually adds some value. Part of what I'm trying to achieve is to get a look similar to mathematical papers published with LaTeX. A big part of that look is the newtheorem environment.

It occurred to me that when I engage in shameless advertising, M.Wenzel may not like my configuring the syntax of Isar, and decide to lock the syntax down.

Ultimately, I assume everyone makes the best possible choices for their needs, whether personal or corporate, and so I look for independent solutions, rather than beg for features. It happens to be, I've discovered that Isabelle has a lot ability to implement solutions with ML, and did I forget to mention 'Isabelle_System.bash_output', also provided by M.Wenzel?

Fragmentation of technology can be bad, but it can also be good.

I speak now as the EZProphet. Here's what will happen with the language and logic of Isabelle/HOL and Isabelle/Isar:

1) The language/syntax will fragment, because when you give people new tools, they get original and new ideas, some good, but most being bad or nothing better.

2) After some period of time, there will be consolidation around the best use of the language/syntax.

3) After that, I don't know. After all, I'm just the EZProphet.


Attachment: 151110_session_error_no_PIDE_error.png
Description: PNG image

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