Email Gateway (Aug 19 2022 at 14:02): Email Gateway (Aug 19 2022 at 14:02):From: Gottfried Barrow <igbi@gmx.com>
PRELIMINARY ERROR REPORT
Rather than send two emails, I put this error report in here, because
it's no big deal.
In my type class helper source, I had a subsection command immediately
followed by another subsection command, as shown below, where the first
command ended with a ) instead of a }.
What's shown below will cause no error in the PIDE. I only found the
error when I inserted a print_classes after the wrongly terminated
subsection command. An inserted print_classes also doesn't cause an
error; it just doesn't do anything.
subsection{test 1)
(print_classes. This wasn't here at first.)
subsection{test 2}
term "int"
BACK TO THE TYPE CLASSES
There are 179 type classes imported with Complex_Main (plus one more
imported with BNF), of which 82 are used for nat, 106 for int, 110 for
rat, 143 for real, and 88 for complex.
Attached is a screenshot showing what the attached THY will show you
about those 180 type classes. Use print_locale! instead of
print_locale to see all the theorems for a type class. For some type
classes, print_locale! will take a long time to process.
Those who love their 5mm mechanical pencils will someday also love type
classes.
Algebra type classes stay true to the "abstract" in "abstract algebra".
Also, former 5mm-mechanical-pencil-addicts will love being able to do
abstract numeric calculations with numbers that have types of type
classes, such as these:
value "1 + (2::'a::numeral)"
(* (1::'a::numeral) + 1 + 1 *)
value "1 + (2::'a::linordered_semidom)"
(* (1::'a::linordered_semidom) + 1 + 1 *)
value "1 + (2::'a::ring_1)"
(* (1::'a::ring_1) + 1 + 1 *)
value "1 + (2::'a::field)"
(* (1::'a::field) + 1 + 1 *)
For concreteness, there is still nat, though the processing of the
successor function can require the help of n + 1 = Suc(n) neurons:
value "1 + (2::nat)"
(* Suc (Suc (Suc (0::nat)) *)
Regards,
GB
type_class_sidekick_helper.png
type_class_sidekick_helper.thy
Email Gateway (Aug 19 2022 at 14:03):From: Makarius <makarius@sketis.net>
There is no error in the Prover IDE, because the above is correct. We
can be glad that the editor and the prover mostly agree on the basic
syntax of the sources.
Isabelle outer syntax has a variety of "delimited tokens" with slightly
different rules for nesting and escapes (or lack thereof):
(* (* nested *) comments, without escapes *)
{* non-nested verbatim text, without escapes *}
"double-quoted string, with escapes for \" and \\, but without nesting"
back-quoted string, with escapes for \ and \\, but without nesting`
That's mainly it, but still a bit complex, not to say complicated. The
lack of nesting and need for escapes introduces extra potential for
confusion, as well as occasionaly need for {*} in latex inside
non-nestable {* ... *} chunks.
Incidents and confusion like this happen about 0.5 times per year on this
mailing list. To make an end of this, I have introduced a new concept in
the Isabelle repository version some weeks ago: uniform balanced quotes
that don't need any escapes: the so-called "text cartouches".
It is all ready to be actually used, lets say as a start for verbatim text
like this
section ‹abc›
text ‹abc›
in addition to existing {* abc *} or "abc" in these syntax slots.
I am still hesitating because of an unknown number of people who are still
stuck with Proof General, which presently does not know about this change
of the token language.
If there are remaining Proof General users who want to prove that this
ancient thing is not quite dead yet, we can move over to
proofgeneral-devel@inf.ed.ac.uk to sort out the (simple) things that need
to be done to support text cartouches in Emacs as well.
Alternatively, one could take the subtitle of the talk by Carst Tankink at
INRIA-MSR this week into serious considerations:
The Last March of Proof General
That was before an audience of Coq users, who were still confined to
prover interfaces from 15 years ago.
Makarius
Email Gateway (Aug 19 2022 at 14:03):From: Gottfried Barrow <igbi@gmx.com>
On 14-03-21 12:34, Makarius wrote:
There is no error in the Prover IDE, because the above is correct. We
can be glad that the editor and the prover mostly agree on the basic
syntax of the sources.
Thanks for the explanation.
I actually subscribe to the idea that for one to claim there are
software errors or software bugs, one needs to understand the
developer's intent and the software's purpose, unless the problem is
obvious, like the PIDE freezing. However, I can jump to conclusions, or
forget to cover myself with words like "possible" or "could be", and
emails sent in can't be edited later on.
Incidents and confusion like this happen about 0.5 times per year on
this mailing list.
Though, if lurker_multiplier =100, then there are (100 * 0.5) - 0.5
= 49.5 unreported incidents of confusion like this per year, for those
who never complain about problems, whether real or perceived.
To make an end of this, I have introduced a new concept in the
Isabelle repository version some weeks ago: uniform balanced quotes
that don't need any escapes: the so-called "text cartouches".
I understand from this that ‹abc› is not a replacement for (abc).
If you're taking requests, and another set of unused delimiter symbols
becomes available, it would be nice to have something like that for
comments, (...).
In verbatim source, I exclusively use (...) for comments, which I also
display in a PDF, using a typewriter font to control the spacing. I
never use --{...} or --"...". The symbols (...) have symmetry, and
(...) works better with standard 2-space indentation.
Here's an example, where the spaces may get lost here:
(*This is stuff...
and so forth...*)
If I had ‹abc› for source comments, I could do something like this:
‹|This is stuff...
and so forth...|›
Everything is still currently good.
Regards,
GB
Email Gateway (Aug 19 2022 at 14:06):From: Makarius <makarius@sketis.net>
On Mon, 24 Mar 2014, Gottfried Barrow wrote:
I understand from this that ‹abc› is not a replacement for (abc).
So far it is just some funny token syntax, in addition to what has already
accumulated in the past 20-30 years. One could in principle do it like
LISP, and use just one kind of parentheses for everything, but that is
hardly readable.
The intention of {* ... *} from 15 years ago was to provide a manner of
"quoting" informal text, such that formal material (types, terms,
theorems) can be "anti-quoted" inside it, but without any conflict with
the typical double-quotes of Isabelle inner syntax. IIRC, {* ... *} was
not made nestable for simplificity: Emacs did not support nested comments
at that time, so it happened to be the same for (* ... *), althouth the
latter have alsways been nestable in Isabelle.
Today the prover and editor agree on the Isabelle token language, so more
precision matters.
If you're taking requests, and another set of unused delimiter symbols
becomes available, it would be nice to have something like that for comments,
(...).In verbatim source, I exclusively use (...) for comments, which I also
display in a PDF, using a typewriter font to control the spacing. I never use
--{...} or --"...". The symbols (...) have symmetry, and (...) works
better with standard 2-space indentation.
(* ... *) are just source comments, like % in LaTeX.
Normally, you write comments semi-formally via "-- {* ... *}" or
"text {* ... *}" then they are also rendered by Isabelle document
preparation. Source comments can have funny side-effects on whitespace
here.
The envisioned reform would cover all occurrences of {* ... *} uniformly,
so you could write something like this:
-- ‹abc›
That certainly has symmetry. If you don't like the spacing of the Unicode
characters, you can use a different font, or even make your own with a
font editor.
This visual tinkering is more important for printed documents in LaTeX,
but IIRC you have not even tried that yet.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC