Email Gateway (Aug 22 2022 at 11:53): Email Gateway (Aug 22 2022 at 11:53):From: Gottfried Barrow <igbi@gmx.com>
Greetings,
The previously stated suboptimal, non-response-non-feedback formality
applies; a very scary formality under unknown circumstances, before the
knowns become known; a formality not to be fully formally stated more
than once every 6 months, or at least not twice within a week, even at
the expense of being ambiguous.
If I'm covering info already covered, I apologize more than those who
apologize for the possibility of sending out duplicate notices for calls
for submissions.
This is just a report that I get an error for a session run that I don't
get in the PIDE.
The following outer syntax command causes an error in the session run,
but not in the PIDE:
FOOBAR\<open>test\<close>\<open>test\<close>
If a space is put between the two commands '\<close>\<open>', then there
is no error, or if quotes are used instead of cartouche delimiters.
I include the example theory and outer syntax command below. A small
image is attached showing the failure in the session run.
Thanks,
GB
(* THEORY ***)
theory i151113a
imports Complex_Main ("$GEZ/m/IsE")
keywords "FOOBAR" :: diag
begin
ML
\<open>Outer_Syntax.command @{command_keyword "FOOBAR"}
"(IsE) IMM general text/text tag"
(Parse.text -- Parse.text >> (fn _ => Toplevel.keep (fn _ =>
())))\<close>
FOOBAR\<open>test\<close>\<open>test\<close>
(*
I.prog \<open>w,p\<close> \<open>\<open>f\<bar>ROOT\<close>\<close> \<open>
session "i151113a" (i151113a) = "HOL" +
options [quick_and_dirty = true]
theories
"i151113a"
\<close>
~I.prog \<open>bash.bash\<bar>w,ss,con0\<close>
\<open>\<open>f\<bar>root_run.bash\<close>\<close> \<open>
root_run="isabelle build -v -d . -g i151113a"
printf "%s\n" "$ ${root_run}"
${root_run}
\<close>
*)
end
151113a_session_error_2_cartouche.png
Email Gateway (Aug 22 2022 at 11:53):From: Makarius <makarius@sketis.net>
On Fri, 13 Nov 2015, Gottfried Barrow wrote:
The previously stated suboptimal, non-response-non-feedback formality
applies; a very scary formality under unknown circumstances, before the
knowns become known; a formality not to be fully formally stated more
than once every 6 months, or at least not twice within a week, even at
the expense of being ambiguous.
Can you say this again in plain words?
This is just a report that I get an error for a session run that I don't
get in the PIDE.The following outer syntax command causes an error in the session run, but
not in the PIDE:FOOBAR\<open>test\<close>\<open>test\<close>
If a space is put between the two commands '\<close>\<open>', then there
is no error, or if quotes are used instead of cartouche delimiters.
Isabelle outer syntax is normally written with a bit more space, e.g. like
this:
FOOBAR \<open>test\<close> \<open>test\<close>
You are nonetheless right, that there is a mistake in the scanner for
cartouches in Isabelle/ML, and it disagrees with the Isabelle/Scala
version. I have changed that 3 weeks ago here:
http://isabelle.in.tum.de/repos/isabelle/rev/760e21900b01
Thus the coming winter release should work better in this respect. When
the first release candiates are announced, you should definitely try them.
There is a good chance that other improvements are in conflict with your
way of writing Isabelle documents. See also
http://isabelle.in.tum.de/repos/isabelle/file/f1b257607981/NEWS#l85
Makarius
Email Gateway (Aug 22 2022 at 11:53):From: Gottfried Barrow <igbi@gmx.com>
On 11/14/2015 9:42 AM, Makarius wrote:
Can you say this again in plain words?
Makarius,
Part of its meaning was to say that I won't respond back to anyone who
responds back to me. But to show respect, among other reasons, such a
rule should be applied with discretion.
There are jokes to be made, but all this is no joking matter. It is also
an example of a problem where there is no good solution. The purpose of
a "bug tracking" system would be narrowly defined, but this is a forum,
and a forum is about engaging with people as humans. (Note: As to "bug
tracking" systems, though I don't agree with how you dealt with a
particular event, your philosophy sounds reasonable to me. In the end,
though, apart from this, I consider "things" like that to be "Isabelle
internal politics", and not for me to be concerned with.)
First, I just state another rule of mine about how I operate on the web,
where I consider this as part of the web. My rule is not to engage with
people privately who aren't personal friends. If something starts in
public, I make a point of keeping it in public.
There's this problem that I want to protect my technical interests, by
reporting problems, but the traffic is light here, and so I can end up
creating a big footprint here. I do want a footprint on the web, but I
don't want one here. I do searches on the isabelle-user's page, and
there I am, showing up way too much.
Stating a formality was maybe the third iteration of trying to solve
this problem.
Isabelle outer syntax is normally written with a bit more space, e.g.
like this:FOOBAR \<open>test\<close> \<open>test\<close>
Let us consider that your time is more valuable than mine.
You tell me how to do things, but then I don't do it your way. At this
point, it has already been a waste of your time to read this, and the
last two sentences.
When you can see my ideas as a whole, then it won't be a waste of your
time to tell me how I should do things. In a just a few minutes, you'll
you be able to say, "Yea, there's a few good ideas here, I see why
you're having to do things different", or, "This is worthless, there's
no good reason for you to be doing things different.".
The use of no space would be specific to using "FOOBAR" as a
text-text-argument markup tag, in a way that's meant to take up as
little space as possible. As to two-arg outer syntax tags, there is also
text-term and term-text. Below, I say that new additions to releases
eliminate any special needs.
You are nonetheless right, that there is a mistake in the scanner for
cartouches in Isabelle/ML, and it disagrees with the Isabelle/Scala
version. I have changed that 3 weeks ago here:
http://isabelle.in.tum.de/repos/isabelle/rev/760e21900b01
And this would be in line with how I think I should operate sometimes,
that problems like these have been taken care of, or will eventually get
taken care of, so there's no need for me to get involved. But then the
flip-side-analogy is 10 people getting served, who came in after me; I
assume I'll get served, but I don't, because they lost my order.
Thus the coming winter release should work better in this respect.
When the first release candiates are announced, you should definitely
try them. There is a good chance that other improvements are in
conflict with your way of writing Isabelle documents. See also
http://isabelle.in.tum.de/repos/isabelle/file/f1b257607981/NEWS#l85
I continue to welcome new additions, and I see the addition of
\<^verbatim> and \<^emph>.
I try to build on what others have done, so to the extent that the new
features line up with what I think I need, or to the extent that they
only can be used in one way, I use them the normal way. To your chagrin,
I may use them differently.
What I do shouldn't undermine anything. For me, it's the real deal. For
others, I hope to make it a demo of what could be done, most likely in a
more sophisticated way.
I end this mentioning three "features", some outer syntax commands that
get interpreted as LaTeX newtheorem environments, where the source that
follows is put in a fancyverb environment with line numbers, directly
underneath the newtheorem title. The 3rd feature would be "subtle"
syntax that gets interpreted as a very specific LaTeX equation environment.
I ask, "Do these features exist?", and, "If they don't, should you make
implementing them a priority just for me?"
The answers are no and no. What I want is more textbook style. What you
guys needs is more journal style.
I could explain what my ideas are for the two-text argument of FOOBAR
above, as a tag, but it would be a waste of your time. If I ever produce
something, it'll already have been superseded by a new feature, or
you'll very quickly be able to look see at what might interest you.
New features sometimes eliminate a need for what I've done, but
sometimes they don't. Given enough time, anything I've done, you'll have
done better, but I have to commit now.
With all due respect, I don't respond to those who respond back to me.
Regards,
GB
Email Gateway (Aug 22 2022 at 11:53):From: Makarius <makarius@sketis.net>
There is already a "tag" feature that allows to wrap Isabelle document
commands (like 'text') or other formal command (e.g. proof commands) in a
LaTeX environment.
An example can be seen here:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015/src/Doc/Implementation/ML.thy#l563
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015/src/Doc/Implementation/document/style.sty#l39
Maybe that is already sufficient to implement all 3 points above.
Makarius
Email Gateway (Aug 22 2022 at 11:53):From: Gottfried Barrow <igbi@gmx.com>
Markarius,
I suppose I should finish what I started, which requires that I attempt
to explain some of my ideas.
I attach two images which show what I did the first year in 2012, when I
implemented about 9 ZFC axioms based on Obua's THY. The particular image
shows work on permutative rewrite rules. T.Nipkow tipped me off about
those. As to the words in the image, don't pay too much attention to
that. I say more about the images below.
Thanks for the links. I opened the document. I'll use some of it to
argue that we're not in sync as to our current vision of what the
internals of a THY should look like.
(NOTE: At line 564 all I see special is '%mlex'. You might mean that
commands are available to tie into the low-level machinery. If that's
what you mean, I don't know how much that helps me. Using machinery can
require getting educated about the machinery. It's much easier to get
educated about things like parsing with PEG.js and Node.js, than it is
to get educated about Isabelle machinery. What I say below may reflect
that I didn't get your drift, but I think we're still at odds.)
First, by all appearances, you prioritize according to what want. With
syntax, what's not there must reflect your own personal preferences.
Now, I state two opinions:
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.
You say, "Maybe that is already sufficient to implement all 3 points
above. " No. (SEE NOTE ABOVE)
My markup "tags" are outer syntax definitions. They wrap what they're
supposed to mark up, and nothing wraps the markup tags, because wrapping
requires additional characters and symbols. What I have as outer syntax
may also sometimes be used in textual exposition, where, of course, it's
text, though still markup, but that's not wrapping, that's using tags in
text. (SEE NOTE ABOVE)
EXPLAINING THE FOOBAR COMMAND
Defining too many outer syntax commands is no good, so my FOOBAR was a
general purpose text-text command, one use being a LaTeX equation
environment. Everything is subject to further change, but I show its
use, where the period represents \<cdot>, and "<" and ">" represent
cartouche delimiters.
.<x + y = z + w
= m + y
= q + r><eq.jkl1608>
The alignment of the '=' symbols may get lost.
I will parse that equation into a LaTeX environment, inserting
end-of-lines, and whatever else is necessary. The '\<open>eq\<cdot>' is
the part of the tag that tells me it's an equation environment. It's
possible, given the numerous types of LaTeX equation environments, I
might want 'e1', 'e2', etc. to represent other kinds of environments.
I could change 'eq' to 'q', but the '\label', 'jkl1608',is most of the
clutter, so there's no reason to save one letter.
If all my syntax is defined, I can also have a term-text command, so
that my formula is an active term, rather than just text.
IMAGES, MORE IMAGES
In 2012 and 2013 I developed my funky markup language, with just a
little knowledge of regular expressions. Since then, the words "parsing"
and "grammars" sunk in to my conscientious. It's the result of being
exposed to the talk of computer scientists, who deal in languages.
I'm trying to get back to where I was, but with much cleaner syntax.
It'll take me six months to a year to get there, because I'm also trying
to work on getting some number systems, vectors, and boolean logic done.
The first image is my funky markup, in the THY, which is fairly
readable. The second image shows my PDF. These things involve personal
preference, but I like how my PDF looks.
I've moved on, on some things, but it formed the basis of some things. I
can't converge back, from the divergence. I'm too deep in. What's most
important is that I actually finish something.
Regards,
GB
151114a_Z_thy.png
151114b_Z_pdf.png
Email Gateway (Aug 22 2022 at 12:24):From: Gottfried Barrow <igbi@gmx.com>
Makarius,
This email is to finish things up before I send in another email, about
the big problems with RC1.
My game has changed, so I installed. I don't do proof with Isabelle
anymore, so my need for help will be near zero.
I only do programming with Isabelle. The right foundation has to be
laid, and programming is part of the foundation; there's not enough time
to do both.
The first part is to you. The rest is just me talking.
I jumped to conclusions about \<^emph>, but the associated symbol for
the command is good. Not having true italics is no big loss, but not
having a true bold font would be a really big loss.
The extra bullet symbols are good.
I got everything converted that's important.
You switched the way Windows paths work, but I found those problems when
you put out a test release last year. Here's how I now have to set
USER_HOME to be able to change my home folder:
set USER_HOME=/cygdrive/e/D_1/w rk/g_d/gezz
I had some ML in between {...}, which allowed me to not having
matching cartouches. Using 'isabelle build' wouldn't allow that. Now I
have a dummy right cartouche like this:
val split1 = IsE.split_symS_delim_to_snd "\<open>" setup1; val _ =
"\<close>"
I tell you that to let you know that all the programming commands I've
implemented are all dependent on the cartouche delimiters.
BAD PROBLEMS
I'll send in a different email about the bad problems. There's been some
bad process runaway, a blue screen of death, and bad hanging for the
64-bit Windows version.
FRONT END MATH
I've been driven by a simple number theory problem, where the proof was
based on manipulating base ten digits.
The long story is too long, but here's a good book:
Computer Arithmetic and Verilog HDL, by Cavanagh
https://www.crcpress.com/Computer-Arithmetic-and-Verilog-HDL-Fundamentals/Cavanagh/9781439811245
That was supposed to give me the model for computer arithmetic in
Isabelle/HOL, for number systems.
In my mind, I just break up a decimal number as a sum of digits,
multiplied by the appropriate power. In Isabelle/HOL, it's not simple at
all, because all the basic groundwork isn't there. It seems true types
for at least bases 3, 5, 7, and 10 should be there.
Now, take a standard function, "f:A --> B", where A and B are elements
of the power set of the natural numbers. How do you easily state A and B
as your domain and codomain in HOL?
You don't, not easily. It could be reasonably easy, but right now it's
not. Part of the problem is just a "syntax feature problem". It's not a
logic problem.
Nothing in all this is a problem with the software. The software is
powerful enough, if people are flexible and will fill in all the gaps.
Regards,
GB
Email Gateway (Aug 22 2022 at 12:28):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Apr 25 2024 at 12:23 UTC