Email Gateway (Aug 22 2022 at 11:51): Email Gateway (Aug 22 2022 at 11:51):From: Gottfried Barrow <igbi@gmx.com>
Greetings,
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.
DESCRIPTION OF THE PROBLEM
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.
ISAR AS A MATHEMATICAL LANGUAGE
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.
Regards,
GB
151110_session_error_no_PIDE_error.png
Last updated: Apr 24 2024 at 16:18 UTC