[isabelle] Bug report. \<^bold>\<lambda> in Cube.thy

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.

Did you read the documentation so quickly? Some exercises with the input
methods also require some time.

Makarius

Dominique Unruh

2018-09-21 06:31:04 UTC

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.

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.
Did you read the documentation so quickly? Some exercises with the input
methods also require some time.
Makarius

Makarius

2018-09-21 11:37:23 UTC

Post by Dominique Unruh
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.

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

Dominique Unruh

2018-09-21 11:42:13 UTC

I know what you mean, but readers of this mailing list also know that

Post by Makarius
"bug" and "fix" is not part of my vocabulary: it leads to a wrong idea
about the actual problems.

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.

Makarius

2018-09-21 11:47:32 UTC

Post by Dominique Unruh
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...

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

Makarius

2018-09-23 16:09:12 UTC

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

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

Makarius

2018-09-23 20:29:30 UTC

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.

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

Jeremy Dawson

2018-09-24 01:42:46 UTC

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

Post by Makarius
That is just street language. Isabelle is a more elite project, where
people express themselves more accurately.

Lars Hupel

2018-09-20 21:27:17 UTC

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.

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.

Jeremy Dawson

2018-09-21 03:49:33 UTC

Post by Lars Hupel
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.

I don't think this is really a practical suggestion. I have found the
Isabelle source code extraordinarily difficult to figure out. Much of
it is completely lacking any sort of explanation (certainly within the
body of the source files, and so far as I have seen, anywhere else).
Certainly it has led me to advise that I'd rather be unemployed than to
have to work with (recent) Isabelle.

It's reminiscent of the sort of code one tells students
(1) if your programs are like this you should be shot
(2) if you succeed in getting away with this without being shot, you'll
have a job for life, since no-one else will be able to figure out what
you have done

As for the extraordinary complexity of the whole setup, one supposes it
must have seemed like a good idea to someone, sometime.

So, quite reasonably, one expects the developers to do the bug-fixing

Jeremy

Post by Lars Hupel
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.

Makarius

2018-09-21 11:40:49 UTC

Post by Jeremy Dawson
I have found the
Isabelle source code extraordinarily difficult to figure out. Much of
it is completely lacking any sort of explanation

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

Jeremy Dawson

2018-09-23 08:51:30 UTC

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

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

Makarius

2018-09-23 20:41:37 UTC

Post by Jeremy Dawson
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.

Post by Jeremy Dawson
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

Jeremy Dawson

2018-09-24 02:45:00 UTC

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.

Post by Jeremy Dawson
As for the Isabelle/jEdit Prover IDE - how does it help in finding an
explanation of the Isabelle source code?

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

Makarius

2018-09-25 12:19:25 UTC

Post by Jeremy Dawson
As for the Isabelle/jEdit Prover IDE - how does it help in finding an
explanation of the Isabelle source code?

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

Jeremy Dawson

2018-09-25 14:16:18 UTC

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

Makarius

2018-09-25 14:18:42 UTC

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

Jeremy Dawson

2018-09-25 14:29:53 UTC

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

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

Makarius

2018-09-25 14:46:24 UTC

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

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

Jeremy Dawson

2018-09-25 15:21:22 UTC

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

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

Jeremy Dawson

2018-09-25 15:42:20 UTC

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

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

Makarius

2018-09-25 17:04:03 UTC

Post by Jeremy Dawson
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.

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

Please read section 1.1 as well.

Anyway, I am giving up on this hopeless thread.

Makarius

Jeremy Dawson

2018-09-26 00:49:01 UTC

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

Please read section 1.1 as well.
Anyway, I am giving up on this hopeless thread.
Makarius

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

Jeremy Dawson

2018-09-26 09:20:16 UTC

Post by Jeremy Dawson
(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

Jeremy Dawson

2018-09-25 15:38:37 UTC