Email Gateway (Aug 19 2022 at 07:55): Email Gateway (Aug 19 2022 at 07:55):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I try not to ask these simple questions when I know so little, but I'd
need to ask this eventually. It's better to ask now, than later with a
couple thousand lines of code.
I've read the style guide in implementation.pdf, so I've read and seen
that the preferred identifier naming scheme uses the underscore
character "_". However, I don't like how it looks, but a bigger issue is
that I have to escape it in Latex. Right now, I'm not using the Isabelle
Latex processing.
I'm kind of settling on a combination of limited camelcase use, and
using the single quote character, ( ' ), to separate words in an identifier.
For example, I have the identifer "emS'is'unique". Below, I include a
very fledgling theory where I don't know what I'm doing. It's to show
some of my identifier naming.
I haven't seen any naming like "emS'is'unique". Is this just a matter of
preference, or would doing a lot of that come back to haunt me? I'm
assuming if I don't get errors in jEdit when doing that kind of thing,
it's not going to come back to haunt me.
(I haven't figured out if the unicode characters in an email like this
show up correctly in other's email readers.)
Thanks,
GB
theory sTs
imports Main
begin
(sT....The set type.)
typedecl sT
(scP...Axiom schema of comprehension property.)
type_synonym scP = "sT ⇒ bool"
axiomatization
(inS...Set membership predicate.)
inS:: "sT ⇒ sT ⇒ bool" and
(emS...The empty set.)
emS:: sT
where
(emE...The empty set is empty.)
emE: "∀a::sT. ¬(inS a emS)" and
(upS...Unordered pair set.)
upS: "∀(a::sT)(b::sT). (∃c::sT. ∀x. (inS x c) ⟷ (x = a) ∨ (x = b))" and
(scS...Schema set: axiom schema of comprehension.)
scS: "∀(a::sT)(P::scP). (∃b::sT. ∀x. (inS x b) ⟷ ((inS x a) ∧ (P x)))"
(Meaningless. It's merely a result of names.)
theorem emS'unique'meaningless : "(a = emS) ∧ (b = emS) ⟹ a = b"
by(auto)
theorem emS'is'unique: "a = emS ⟷ (∀x::sT. ¬(inS x a))"
apply(auto)
oops
end
Email Gateway (Aug 19 2022 at 07:58):From: Makarius <makarius@sketis.net>
On Tue, 3 Jul 2012, Gottfried Barrow wrote:
I've read the style guide in implementation.pdf, so I've read and seen
that the preferred identifier naming scheme uses the underscore
character "_". However, I don't like how it looks, but a bigger issue is
that I have to escape it in Latex. Right now, I'm not using the Isabelle
Latex processing.
The Isabelle document preparation system will solve these problems for
you. What are the reasons for not using it?
Generally, camelCaseWasInventedByPeopleWhoDidNotHaveUnderscoreAvailable
InTheireCharacterSet, probably around 1960/1970, before ASCII became
universally accepted. Spacing between words improves readability, this
was observed first about 3000 years ago -- the ancient Phoenicians and
early Greek writers did not know it yet. Classic fonts are also designed
to have capitals in front of words only, not in the middle. You can see
this especially in the Computer Modern fonts of LaTeX.
Even though our classic (Unix) standard of separating words by underscore
has been there from the beginnings (1980-ies/1990-ies), one reason why it
was made more explicit in recent years might be the advent of good
typographic screen fonts like Bitstream Vera. Then the rules for proper
typography become more important to screen display.
So why do many younger people still consider camel case as standard? My
theory on the main historical events is that:
* Xerox PARC that introduced the legendary Xerox Star computer system
with bitmap display, mouse, object-oriented programming for GUIs in
the 1970-ies was one of these labs living in the IBM-tradition of not
having "_" on the keyboard nor in the character set. So the classic
workaround to use camelCaseAsAnApproximation was employed. (You can
still see that in the "Axiom" programming language, for example, which
lacks "_" by default. It is from a genuine IBM lab.)
* Apple copied that to make the Lisa and Macintosch.
* MS copied that to make Windows.
* Almost everybody else copied that as well.
What remains are a few ancient guys like in the Isabelle, Coq, OCaml
communities, who did not submit to that invasion.
I'm kind of settling on a combination of limited camelcase use, and
using the single quote character, ( ' ), to separate words in an
identifier.For example, I have the identifer "emS'is'unique". Below, I include a
very fledgling theory where I don't know what I'm doing. It's to show
some of my identifier naming.
I don't understand the motivation for that. The formal Latex generation
of Isabelle works smoothly with things like @{text foo_bar}, @{thm
foo_bar}, even @{ML foo_bar}.
You can also redefine the default isabelle latex macros to get a slightly
different glyph for the underscore.
(I haven't figured out if the unicode characters in an email like this
show up correctly in other's email readers.)
I would say that should work out in practice, I am doing it myself all the
time now. Strictly speaking one cannot expect 100% reliability of unicode
transmission, but such mail threads are not for achiving of 100% correct
formal sources (unlike a repository which has to be more authentic).
Makarius
Email Gateway (Aug 19 2022 at 08:03):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Makarius,
First, I have been influenced by your emphatic insistence, spoken in
various ways, that we not use camelcase. Now I'm trying to come up with
a solution for long identifiers that doesn't use underscores. Here, I
resist the temptation to go into a lengthy discussion of my view of the
aesthetics of the underscore. There's a lot of freedom with Isabelle;
having figured that out, I now try to be flexible.
...a bigger issue is that I have to escape it [the underscore] in
Latex. Right now, I'm not using the Isabelle Latex processing.
The Isabelle document preparation system will solve these problems for
you. What are the reasons for not using it?
Last year, I worked on trying to use Isabelle to produce the PDF docs
from the .thy files. In looking through the source of the tutorial,
prog-prove.pdf, I can see the benefits of doing things your way, such as
being able to put in hidden "oops"s.
However, there's a problem, and there's a complete show-stopper. You
should keep in mind that I'm not willing to live without my Latex
macros, especially for sectioning commands, which I tweak to create
customized bookmarks. I think that in itself isn't/wasn't a problem, but
it complicates things a little. Last year, my solution was to only use
"text{...}", and none of the Isar sectioning commands.
PROBLEM: To be productive with Latex, you need to compile often, and be
able to compile fragments. I don't remember if compile speed for a small
theory was a problem, but to compile a theory fragment now, I'd have to
write scripts to create temporary .thy files for the fragment, and these
would have to import parts of the .thy that I'd be working on, so that
Isabelle wouldn't choke on a logic error. It's just the hassle of
switching over from what I use now, or, possibly, a big hassle.
SHOW-STOPPER: It's vaguely coming back to me, but I'm pretty sure that
the show-stopper was my need for the Verbatim environment. I had to put
it in a "text{...}" command, but "begin{Verbatim}" and "end{Verbatim}"
are picky about what can be on the same line with them. I couldn't get
rid of those errors, that I remember.
Anyway, I gave up and made the Isar subservient to the Latex in a tex
file. I'm now back to making the Latex subservient to the Isar in a thy
file by commenting out all the Latex, so that the file can be directly
loaded into jEdit.
Right now, I can't spend more time on trying to make things look nice,
at least done that way. The harder learning curve is Isabelle, and the
prerequisite knowledge required to use it.
Generally, camelCaseWasInventedByPeopleWhoDidNotHaveUnderscoreAvailable
InTheireCharacterSet, probably around 1960/1970, before ASCII became
universally accepted. Spacing between words improves readability,
this was observed first about 3000 years ago...
There is the issue that using the underscore for spacing makes a name
longer, but I'm seeing it your way, that spacing is important, and that
capital letters are best used sparingly. And with a little work, I can
probably come up with words that keep the name length down.
I'm kind of settling on a combination of limited camelcase use, and
using the single quote character, ( ' ), to separate words in an
identifier.For example, I have the identifer "emS'is'unique". Below, I include a
very fledgling theory where I don't know what I'm doing. It's to show
some of my identifier naming.I don't understand the motivation for that. The formal Latex
generation of Isabelle works smoothly with things like @{text
foo_bar}, @{thm foo_bar}, even @{ML foo_bar}.You can also redefine the default isabelle latex macros to get a
slightly different glyph for the underscore.
Here, I have to get into my opinions about mathematical writing, of
which I'm more of a critique than a producer.
For me, at this point, there are two important driving principles, among
others:
1) try to follow traditional, mathematical writing convention as
much as possible, and
2) keep a clear distinction between the syntax and language of
Isar, and the informal
language of mathematics used to discuss, prove, define, etc..
The good news is that you were thinking about Isar over 10 years ago.
Isar is sympathetic to tradition, with its structured proofs, the
ability to abbreviate structured proofs, and with its standard
mathematical symbols.
The breakdown, as I see it, comes with theorem names, function names,
and constant names; that is, names in general. Formal, compound-word,
long names, aren't a part of mathematical writing. So this requirement
by programming languages that everything have a name doesn't fit with
traditional-looking mathematical language in an unobtrusive way.
To describe the motivation for "emS'is'unique", consider this
hypothetical sentence in my hypothetical book:
My dear reader, please consider what happens when /A/ is bounded by
/b/.
Suppose formally that I've defined a function /is_bounded_by/. As a
quick advertisement, I mention Slawomir's IsarMathLib.
http://www.nongnu.org/isarmathlib/
By looking at his document, I saw his use of infix notation such as "A
{is disjoint with} B", which is shown on page 7. Okay. I like the idea,
but I don't like curley braces for non-set use any more than I like
underscores.
Here, I could stop writing and just say, "You know what, there is no
perfect solution to trying to create spacing between words without only
using spaces. Spaces look good when all you want is a simple space. All
these other characters don't".
Well, back to my pontificating.
Alright, so you tell me that I can delay the decision on how to
represent the underscore by using antiquotations such as @{text
foo_bar}, and that I can substitute glyphs, probably very nice looking
glyphs, for the underscore.
There are two problems. If I formally introduce /is_bounded_by/ into my
Isar code, then that's exactly how I want to refer to it anywhere else,
including in an informal discussion. As a total beginner, it was a
source of confusion for me to see identifiers which had hyphens
substituted for underscores. It's a non-issue now, but a 30-second
concept can be a 1-weeker when I'm on my own, especially if I'm only in
a discovery stage to try to determine if I want to go down a certain route.
The other problem is that I should make the "executive decision" now.
There are only a few non-alpha-numeric characters available to use in an
identifiers. Here's a list of me trying to name "is bounded by":
1) is_bounded_by
2) isBoundedBy
3) is'bounded'by
Really, if the phrase "is bounded by" was in a sentence in the middle of
a paragraph, anything done to it would mess it up and break the flow of
the sentence. Even italicizing it would mess it up.
The single ticks aren't looking so good to me at this moment. What I
need to do is put the different names in the middle of a big paragraph,
like in these sentences:
My dear reader, please consider what happens when /A is'bounded'by
b/, or
My dear reader, please consider what happens when /A is_bounded_by b/.
It's like recording music. You get up the next morning, and what you
thought sounded good the night before, doesn't sound so good anymore.
However, I think camelcase is out, for the most part.
Nothing's ever simple, though. What I see in jEdit, which is
emS'is'unique, looks better because jEdit is using a fixed-width font.
Thunderbird here is not using a fixed width font, so the ticks don't
create enough space.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:04):From: Gottfried Barrow <gottfried.barrow@gmx.com>
It 's becoming less vague. I could get rid of the compile errors, but
because one, or the other, or both \begin{Verbatim} and \end{Verbatim}
needed to be on a line with nothing else, I couldn't get rid of the
"}"s, or the "{"s, or the "("s, or the ")"s. How I was wrapping the
Verbatim begin and end, I don't remember, but stars and delimiters were
cluttering my document.
But that's to be expected, since I was trying to put all of the Isar
code in a verbatim environment, so maybe beginnings and endings on
lines by themselves were never a real issue. Ah, I was using the
Verbatim gobble feature to gobble up some of the stars and delimiters
that wrapped it, but I couldn't gobble them all up.
--GB
Email Gateway (Aug 19 2022 at 08:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gottfried,
SHOW-STOPPER: It's vaguely coming back to me, but I'm pretty sure that
the show-stopper was my need for the Verbatim environment. I had to put
it in a "text{...}" command, but "begin{Verbatim}" and "end{Verbatim}"
are picky about what can be on the same line with them. I couldn't get
rid of those errors, that I remember.
can you give a hint for which sake you are using verbatim? In LaTeX it
mixes up to purposes
a) interpret source more or less literally
b) present result in typewriter
For each of these, there are different possibilities; especially b) can
be achieved with Isabelle without relying on verbatim. a) is not so
simple, but there are ways to cope with involving ML (depending how
general it is supposed to be).
The single ticks aren't looking so good to me at this moment. What I
need to do is put the different names in the middle of a big paragraph,
like in these sentences:My dear reader, please consider what happens when /A is'bounded'by
b/, orMy dear reader, please consider what happens when /A is_bounded_by b/.
It's like recording music. You get up the next morning, and what you
thought sounded good the night before, doesn't sound so good anymore.
However, I think camelcase is out, for the most part.
If your primary concern is how identifiers appear in natural language,
you can consider using your specific set of antiquotations where you can
modify identifiers programatically, in the extreme case using an
explicit substitution table.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 08:05):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Florian,
Thanks for the interest, but first, please allow me to clarify why I
won't be able to use antiquotations such as @{text foo_bar} at the point
I start using Isabelle to create PDFs.
The limitation is that Acrobat's bookmarks can only predictably take
basic ASCII characters, which I constantly forget until I see "stuff" or
the "lack of stuff" in my PDF bookmarks. The bookmarks for chapter 4 of
functions.pdf demonstrates the problem.
http://isabelle.in.tum.de/dist/Isabelle2012/doc/functions.pdf
The antiquotation for section 4.2 resulted in numeric trash in the
bookmark. I use the hyperref package, so I know about the problem from
trying to use macros in section titles. My solution is to not get fancy
in section titles; to not have a bookmark made from a complicated Latex
macro, or use something like @{text foo_bar} in the title.
I heavily use PDF bookmarks. I have Latex macros which use the theorem
environment for Isabelle theorems, lemmas, definitions, etc.. These
macros also create a subsection entry into the
bookmarks/table_of_contents using the name of the theorem. Consequently,
I have to hard code the name so I don't get "stuff" or the "lack of
stuff" in the PDF bookmarks. It's not an option to use fancy characters
in the name, or to figure out later what character I want to use to
separate words.
Secondly, it's obvious to me that the Isabelle Latex document processing
is very powerful and should be the Latex tool of choice for most people
producing Isabelle documents. However, for my needs, without having
spent the time to get what I want through Isabelle, I have to stick with
what I'm doing.
SHOW-STOPPER: It's vaguely coming back to me, but I'm pretty sure that
the show-stopper was my need for the Verbatim environment...can you give a hint for which sake you are using verbatim? In LaTeX it
mixes up to purposesa) interpret source more or less literally
b) present result in typewriter
For each of these, there are different possibilities; especially b) can
be achieved with Isabelle without relying on verbatim. a) is not so
simple, but there are ways to cope with involving ML (depending how
general it is supposed to be).
In looking at functions.pdf, I can see that Alexander is using a
different font than other documentation PDFs. I guess this would be an
example of your "b)". The italicized roman font hasn't always been to my
liking for the Isar code, though typewriter font isn't all upside
either, but I could probably find out how to make basic font changes by
looking at the Isabelle Latex packages.
Bullet "a)" kind of represents why I want the Isar in a Verbatim
environment. I'll say a little more below.
If your primary concern is how identifiers appear in natural language,
you can consider using your specific set of antiquotations where you can
modify identifiers programatically, in the extreme case using an
explicit substitution table.Cheers,
Florian
This is an example of where, because of my multiple wants, in
emphasizing one want, I forget another want that has a higher priority.
It's true that I want Isar identifiers to look good when mixed into a
paragraph of natural language, but more importantly, I want Isar to look
extraordinarily mathematical even in its raw form in a Verbatim
environment, or on the jEdit screen. It happens to be that Isar gives me
a good start. Even Latex doesn't guarantee you a good looking document.
To get Latex looking really good, you have to make lots of artistic
decisions, and do lots of builds, and stare at the screen a lot.
As to natural language, using my example "is_bounded_by", I wouldn't
have to use that in an informal discussion, I could just say "is bounded
by" and let the reader make the connection if it was obvious. Function
over form, or form over function? It's always a compromise.
But back to why I want the Isar in a Verbatim environment. It's because,
being in the student mode right now, I'm sympathetic with a student's
needs. Code in a verbatim environment is basically saying, "This is what
the code really looks like in the editor. If you open the source file,
this is almost exactly what you will see. This is to make sure that you,
as a student, don't have any questions about what exactly the code is."
Replacing identifiers with something significantly different is not
something I would do. Clarity is more important to me than traditional
looking language. More levels of abstraction, or more words requiring
interpretation require more work from the reader, and more work to teach
them what the vocabulary means.
Someday I could decide that line numbers in a Verbatim environment are
just noise. What I'm doing will serve its purpose until I switch to
something else.
Learning a little Latex here and there helps out. There's this Latex
package for Fitch style diagrams:
http://www.mathstat.dal.ca/~selinger/fitch/
<http://www.mathstat.dal.ca/%7Eselinger/fitch/>
Like most array type environments, it doesn't break well over multiple
pages. I know just enough Latex to where I figured out how to modify it
so that it uses longtable. Now, I can use page after page after page to
do a natural deduction proof using a Fitch diagram.
Thanks for the suggestions.
Regards,
GB
Last updated: Apr 25 2024 at 01:08 UTC