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

[Makarius]

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
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

[Gottfried Barrow]

Post by Makarius
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.

Post by Makarius
Isabelle outer syntax is normally written with a bit more space, e.g.
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.

Post by Makarius
You are nonetheless right, that there is a mistake in the scanner for
cartouches in Isabelle/ML, and it disagrees with the Isabelle/Scala
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.

Post by Makarius
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

[Makarius]

Post by Gottfried Barrow
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?"

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

[Makarius]

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.


Makarius

[Gottfried Barrow]

Post by Makarius
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,

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