Email Gateway (Aug 22 2022 at 18:18): Email Gateway (Aug 22 2022 at 18:18):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I use Isabelle 2018 in Debian. ~~/src/Cube/Cube.thy contains symbol \<^bold>\<lambda> a. k. a. "❙λ" a. k. a "U+2759 U+03BB". This symbol consists of two Unicode code points. When I try to copy this symbol from Isabelle IDE (jEdit), it is very easy to copy second symbol without first, i. e. \<lambda> alone. This symbol looks very like \<^bold>\<lambda> , but has other meaning.
I copy-pasted this symbol to my own theory file and spent a lot of time trying to debug a formula, until I finally saw that \<^bold>\<lambda> and \<lambda> are different symbols.
Currently jEdit works with the symbol \<^bold>\<lambda> badly. When I select this symbol using mouse, only \<lambda> is selected. When I traverse a line containing this symbol using keyboard arrow "Right", I need two key presses to pass this symbol. So, overall support for this symbol in jEdit is bad.
Also, I noticed that other programs deal with this symbol even worse. I write this letter using Chromium on Debian. This Chromium doesn't recognize this symbol at all! I threats it as two symbols. I repeat the symbol as is here: "❙λ". My Chromium renders it as two symbols. So, I wonder whether Unicode standard really says that this symbol should be viewed as one symbol.
So, there is two variants.
1A. It should handle this symbol as one symbol. This is best variant. (Same applies to other such symbols, of course.)
1B. If you disagree with 1A, i. e. don't want to add proper support to Isabelle, well, then remove such symbols from Cube.thy and other places.
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:18):From: Makarius <makarius@sketis.net>
Unicode has many problems and will probably require 3 more decades to
get it sorted out. On this way the website https://utf8everywhere.org is
of great help: it puts old documents about Unicode into proper
perspective to avoid its many misunderstandings.
Right now, I don't know any program that implements the Unicode
standards correctly.
Isabelle actually does not use Unicode internally, but its own scheme of
infinitely many named symbols: it is is simpler, better defined, and
more flexible. It is closer to LaTeX than to Unicode.
For the front-ends, e.g. Isabelle/jEdit or HTML rendering, finitely many
Isabelle symbols are displayed via Unicode codepoints pointing to our
own Isabelle font. Thus it mostly works most of the time. There are also
some input methods in the Isabelle/jEdit Prover IDE.
See also the documentation in the manuals "jedit", "isar-ref",
"implementation", searching for "symbols" or "isabelle symbols".
Makarius
Email Gateway (Aug 22 2022 at 18:18):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I will repeat: I get bugs when I try to copy-paste this symbol from one Isabelle document opened in Isabelle/jEdit to other. I select \<^bold>\<lambda>, copy it, paste it to other document and get \<lambda> only. Also I see bugs when I put cursor to line containing this symbol and press Left and Right multiple times. This is bugs. Fix them or stop to use this symbol in Cube.thy.
I can send you screenshots or video, if you want.
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:18):From: Makarius <makarius@sketis.net>
Did you read the documentation so quickly? Some exercises with the input
methods also require some time.
Makarius
Email Gateway (Aug 22 2022 at 18:18):From: Lars Hupel <hupel@in.tum.de>
There is no need to repeat your previous message, particularly not after
such short time.
Please refrain from using such aggressive language here, it won't help
anyone.
And by the way: the source code of Isabelle is public
(<https://isabelle.in.tum.de/repos/isabelle>), and you are encouraged to
fix bugs yourself if they are urgent.
Email Gateway (Aug 22 2022 at 18:19):From: Dominique Unruh <unruh@ut.ee>
While the question of unicode support or not is a larger issue, I think the
issue pointed out by Askar (which I also ran into and had trouble with in
another context with a bold g) could have a simpler solution. The problem
is that select-copy-and-paste in jEdit will easily copy the lambda, but not
the bold. I don't know if fixing that is easy or hard, either, but at least
it would not necessitate changing the whole philosophy of Isabelle's
encoding.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:19):From: Makarius <makarius@sketis.net>
I know what you mean, but readers of this mailing list also know that
"bug" and "fix" is not part of my vocabulary: it leads to a wrong idea
about the actual problems.
Over the decades, Isabelle has become quite ambitious, motivated by
sophisticated applications. The Isabelle control symbols for sub- and
superscript and bold are part of that.
In particular, bold is often an escape-route for unusual syntax, but it
poses challenges to the editor. In the old Emacs days it was almost
unusable. In current Isabelle/jEdit it works quite smoothly.
So instead of forking Isabelle and removing the results of 10-15 years
of efforts to make bold notation work most of the time, here is another
suggestion:
Join the fine jEdit project on SourceForge, and help in maintaining this
great editor platform. It is a solid Java/Swing application, but that
has got out of fashion for social reasons, not technological ones.
Makarius
Email Gateway (Aug 22 2022 at 18:19):From: Makarius <makarius@sketis.net>
There is the "implementation" manual and the Isabelle/jEdit Prover IDE
for Isabelle/Pure/ML development and interactive exploration.
Some weeks ago you ignored both of that, and I see indeed little chance
to understand Isabelle in 2018 without it.
Hopefully that is the end of another potential junk thread on this fine
mailing list.
Makarius
Email Gateway (Aug 22 2022 at 18:19):From: Dominique Unruh <unruh@ut.ee>
I know what you mean, but readers of this mailing list also know that
OK, then "fix" in my mail should be read as "possible nice improvement".
With the understanding that I don't expect anyone to produce that
improvement because I understand that time is limited...
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:19):From: Makarius <makarius@sketis.net>
Such improvements of the jEdit rendering and editing model are feasible,
but the jEdit project has become a bit static in the past 5 years.
I should be easy to revitalize this relatively simple text editor
project. It is just plain Java done in a very sane way.
Makarius
Email Gateway (Aug 22 2022 at 18:20):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
I'm not aware of any instance of my having ignored the "implementation"
manual - sometimes I find it contains useful information, sometimes not.
What, precisely, are you referring to?
As for the Isabelle/jEdit Prover IDE - how does it help in finding an
explanation of the Isabelle source code?
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 18:20):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi. I have read "2.2. Isabelle symbols" in jedit.pdf and also I have read all mentions of symbols in isar-ref.pdf and implementation.pdf. And I still didn't find anything which can change current (wrong) behavior.
It seems you have no issue tracker. Why? Yes, I clearly see you don't want to solve this \<^bold> issue right now. Yes, you probably have something more important to do now, I understand you. And I understand that this is free software and you ought nothing to me. But this still would be very nice if you will write such issues into issue tracker. So you will not forget about them and will solve them when you complete some more urgent things. Even if you don't want to solve the issue at all, still write it to issue tracker with resolution "won't fix" or "not a bug", so users will see that there is no point to report the issue again.
Also, there is nothing wrong with terms "bug" and "fix". Entire free software world uses them. They are used by, say, Linux kernel developers. Go web search for "top 100 free software projects", look at mailing lists of this projects, and I pretty sure that all them use terms "bug" and "fix", this is just standard terminology in our industry.
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:20):From: Makarius <makarius@sketis.net>
That is just street language. Isabelle is a more elite project, where
people express themselves more accurately.
There is nothing wrong with Isabelle, jEdit, or Isabelle/jEdit the
Prover IDE. If you want to contribute to improve the jEdit text editor
beyond its basic Unicode support, you can add tickets to its many
trackers on SourceForge.
Makarius
Email Gateway (Aug 22 2022 at 18:20):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I just installed jEdit from Debian repo. Then I copied whole \<^bold>\<lambda> from Cube.thy (opened in Isabelle/jEdit) and pasted it into plain jEdit installed from the repo. And I saw two separate symbols. This means that jEdit itself (in default configuration) doesn't have support for \<^bold>\<lambda>. This symbol has special handling in Isabelle/jEdit. So, the issue I report here is related to Isabelle, not to jEdit itself.
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:20):From: Makarius <makarius@sketis.net>
I have explained it on this thread already: Isabelle uses symbols that
are closer to LaTeX than to Unicode. There is some approximative
rendering of the these Isabelle symbols as plain Unicode in jEdit,
spiced up with font styles. Further improvements need to happen on that
side: to make the jEdit editing and rendering model a bit more like
"rich text editor". That is in principle feasible, but the jEdit project
has become a bit static in recent years.
That is not a technical problem, but a social one: most people do what
most other people do, and Java/Swing is no longer part of that for no
particular reason.
Makarius
Email Gateway (Aug 22 2022 at 18:20):From: Makarius <makarius@sketis.net>
On 23/09/18 10:51, Jeremy Dawson wrote:
I'm not aware of any instance of my having ignored the "implementation"
manual - sometimes I find it contains useful information, sometimes not.
What, precisely, are you referring to?
I refer to its general explanation how Isabelle works, notably
Isabelle/ML inside the formal theory context, and the concepts of
contexts in the first place. Isar is just a corollary from that. All of
these advanced concepts after 1998 are integral to Isabelle in 2018.
As for the Isabelle/jEdit Prover IDE - how does it help in finding an
explanation of the Isabelle source code?
It provides a lot of formal annotations to help browsing the sources as
a one huge document written in ML -- not "code". There is also a
SideKick tree view for the all-important section structure of
Isabelle/ML sources, to keep an overview.
I've recently been exposed myself to a huge code-base (in Scala) that I
did not know nor understand beforehand. Thanks to the great IntelliJ
IDEA, I could explore it easily. That IDE is even more heavy-weight than
Isabelle/jEdit for Isabelle/ML, but I will see how to re-use some its
advanced IDE concepts eventually. Thus Isabelle/jEdit will become even
more useful, but also more "sluggish" and less acceptable to TTY users.
As a first step, I might try to set up an IntelliJ IDEA project for the
Isabelle/Scala sources, to shed some IDE light on these, too.
Makarius
Email Gateway (Aug 22 2022 at 18:21):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
Well, what - in your view - is the more accurate way of expressing the
concepts for which the standard terminology in the software industry is
"bug" and "fix"?
Then, once everyone else learns the right language to use in connection
with this "elite" project, it might be possible for effective
communication to occur.
Jeremy
Email Gateway (Aug 22 2022 at 18:21):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 09/24/2018 06:41 AM, Makarius wrote:
On 23/09/18 10:51, Jeremy Dawson wrote:
I'm not aware of any instance of my having ignored the "implementation"
manual - sometimes I find it contains useful information, sometimes not.
What, precisely, are you referring to?I refer to its general explanation how Isabelle works, notably
Isabelle/ML inside the formal theory context, and the concepts of
contexts in the first place. Isar is just a corollary from that. All of
these advanced concepts after 1998 are integral to Isabelle in 2018.Hi Makarius,
Well, I've had another look at these parts, and I can't recall any
question I've asked to which they're relevant. Except that I think I've
on occasions wanted to know exactly what information is contained in a
proof context (as distinct from a theory or a proof state), and on this
point the manual is even less informative than I had remembered.
As for the Isabelle/jEdit Prover IDE - how does it help in finding an
explanation of the Isabelle source code?It provides a lot of formal annotations to help browsing the sources as
a one huge document written in ML -- not "code". There is also a
SideKick tree view for the all-important section structure of
Isabelle/ML sources, to keep an overview.So how does one get these annotations? I've tried opening jedit, and I
can't find how to access the source code through it, let alone the
annotations. Incidentally, what to you mean by "not "code""? Is this
another word with a different meaning when we're discussing Isabelle?
Jeremy
Email Gateway (Aug 22 2022 at 18:21):From: Makarius <makarius@sketis.net>
See the Isabelle/jEdit manual (60 pages), e.g. from the Documentation
panel in Isabelle/jEdit. That panel also provides a one-click entry for
src/Pure/ROOT.ML -- if you go there, it contains some explanations in
the top of the file.
A "document" is something you study carefully, read and write it like a
good novel, poetry, or epic. (Examples: well-written Isabelle/ML or the
Isar proof language.)
"Code" is not necessarily readable, it is interpreted by the machine.
(E.g. machine language or old-style tactic scripts.)
"Source code" is an oxymoron often used today, e.g. in "Source Code
Management System" (like Mercurial). It more often means "document
sources in a formal language" than anything with "code" for the machine.
Makarius
Email Gateway (Aug 22 2022 at 18:21):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Well, that entry src/Pure/ROOT.ML enables me to load a particular file
from the source code (you haven't said what you want to call it
instead), and what I see in the output panel is the usual response of an
ML system to the declarations in the file. But where are the
annotations you refer to?
Jeremy
Email Gateway (Aug 22 2022 at 18:22):From: Makarius <makarius@sketis.net>
See the Isabelle/jEdit manual (60 pages), it also contains many screenshots.
Maybe I write English in a way that you don't understand, and that might
be the mystery behind decades of misunderstandings.
Makarius
Email Gateway (Aug 22 2022 at 18:22):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
I can't see any screenshots showing annotated source code, and a quick
glance through the manual doesn't show me which part of it, if any,
describes how I get them. How about you just tell me where the
information is in the manual to which you are referring?
What you perhaps don't understand is that it's totally unreasonable to
suggest someone reads a 60 page manual when you could easily say which
bit of it is relevant.
Jeremy
Email Gateway (Aug 22 2022 at 18:22):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Click "Documentation" at the right, this will open "Documentation" panel
Click "Examples > src/Pure/ROOT.ML" in this panel, this will open file ROOT.ML
Then click "Sidekick" at the right, you will see this document in tree form
Then press down "Ctrl" button (on PC) and while holding it, move the mouse to any file name listed in ROOT.ML (say, ML/ml_name_space.ML) (3.5. Tools and hyperlinks in Isabelle/jEdit manual) (I mean to file name in ROOT.ML itself, not in Sidekick)
Attention: you should first hold "Ctrl" and then move mouse to file name, not the other way. Also, you should keep "Ctrl" holding when you hover file name
Then you will see file name became gray. Precisely at this moment click file name. You should still keep holding Ctrl. Note: be hurry, file name will restore its normal color in one second, you should be hurry to click file name immediately the file name became gray.
Then this file will open in editor.
Same way you can move to files where given identifier is defined.
Also same way you can see (possible recursive) tooltips for identifiers. See 3.5.
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:22):From: Makarius <makarius@sketis.net>
E.g. Fig. 1.1 -- the very first screenshot with its explanations section
1.2.
It is worth reading that manual carefully experimenting with its various
hints and suggestions.
Makarius
Email Gateway (Aug 22 2022 at 18:22):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Well, Fig 1.1 is an Isabelle theory file, if I'm not mistaken, and there
aren't any annotations explaining the functions defined. (Arguably
these functions are simple enough that they don't need annotations
explaining them, but my point is that the screenshot doesn't show how I
get to see the annotations you are talking about).
And I take it that "its explanations section 1.2." means that section
1.2 explains what is shown in the screenshot, is that so?
This email thread is about the "annotations" which help explain the
Isabelle source code.
Jeremy
Email Gateway (Aug 22 2022 at 18:22):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Askar,
Thanks for your help. Actually it doesn't seem to work the same here, I
don't get the file names changing colour, and when I click on a file
name, I get, in the output window, what looks like the result of
processing that file.
Anyway, thanks for your help
Jeremy
Email Gateway (Aug 22 2022 at 18:22):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
I've been given an explanation of how to view a source file in jedit,
and it doesn't seem to work for me here.
Could you just point me to where these annotations are located, in the
distribution? Presumably they are moderately legible. Anyway, I'll
have a look at them in whatever their "source code" form is.
Jeremy
Email Gateway (Aug 22 2022 at 18:22):From: Makarius <makarius@sketis.net>
Please read section 1.1 as well.
Anyway, I am giving up on this hopeless thread.
Makarius
Email Gateway (Aug 22 2022 at 18:23):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Section 1.1 contains nothing that seems to answer my questions.
If you're simply not prepared to help someone who has questions, you
shouldn't waste their time. Thankfully in this case the irrelevant
material you tell me to read is only a couple of pages.
Not to mention the time of other people who have actually tried to help me.
As things stand we have a large body of source code of which only a
small proportion is documented at all, and that often in a vague and
imprecise style. There are said to be annotations available - for which
some helpful person tried to explain how I get to see them in jedit, but
it doesn't work on my computer here. And you won't tell me where they
are. Do they really exist?
As a matter of fact - regarding this hopeless thread - can I suggest
giving a short simple answer to two short simple questions: (1) do these
annotations really exist? (2) if so, where are they (ie, path/to/file,
or, if they are scattered around, just a sample).
If you won't answer these, don't bother making this thread even more
hopeless.
Jeremy
Email Gateway (Aug 22 2022 at 18:23):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
(1) do these
annotations really exist?
I'm not expert, but it seems for me that there is no any actual annotations. When we say "annotations" we simply mean that jEdit can display some info about identifier when we hover mouse over it with Ctrl. I mean that jEdit displays type of particular variable and place where it is defined.
Also, I recommend trying to follow my instructions again. I tried lot of times until I finally got hyperlinks to work. I will say again that this instructions will not show you any "annotations", they just will enable you to easily switch from one file to another, to open file which a particular identifier is defined in and to see types of identifiers.
What OS you use? What computer? Mac or PC? What Isabelle version you use?
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:23):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 09/26/2018 06:14 PM, Askar Safin wrote:
(1) do these
annotations really exist?
I'm not expert, but it seems for me that there is no any actual annotations. When we say "annotations" we simply mean that jEdit can display some info about identifier when we hover mouse over it with Ctrl. I mean that jEdit displays type of particular variable and place where it is defined.Hi Askar,
Thanks - in fact I was beginning to wonder if that might be the case.
But since the whole thread started with the topic of the almost totally
undocumented Isabelle source code, these "annotations" are pretty much a
red herring.
Also, I recommend trying to follow my instructions again. I tried lot of times until I finally got hyperlinks to work. I will say again that this instructions will not show you any "annotations", they just will enable you to easily switch from one file to another, to open file which a particular identifier is defined in and to see types of identifiers.
What OS you use? What computer? Mac or PC? What Isabelle version you use?
Right now it's Isabelle2018-RC0. PC running Linux, uname -a gives
Linux hp2017 4.13.9-300.fc27.x86_64 #1 SMP Mon Oct 23 13:41:58 UTC 2017
x86_64 x86_64 x86_64 GNU/Linux
CPU is Intel(R) Core(TM)2 Quad CPU Q9400 @ 2.66GHz
But I'll try at work tomorrow, see if it makes a difference.
Cheers,
Jeremy
Askar Safin
http://vk.com/safinaskar
Last updated: Apr 25 2024 at 16:19 UTC