Email Gateway (Aug 19 2022 at 13:52): Email Gateway (Aug 19 2022 at 13:52):From: Gergely Buday <gbuday@gmail.com>
This is how I see it: I have met an unexpected behaviour: looking up a
definition did not work. With my limited knowledge of the system, I
tried to identify the cause. I spot the difference as the definition
being in another file or in the same. This was incorrect. Makarius
changed the aspect: the difference is between processed and
unprocessed definitions. The former's data is in the heap so
Isabelle/Jedit can look it up.
But now a question comes to my mind: the mentioned file, Lambda.thy
was not itself processed but I use a precompiled heap image of Nominal
that includes Lambda.thy as well. I understand that I might change
Lambda.thy but _in theory_ the original definitions of Lambda.thy
_can_ be looked up in the precompiled heap. Of course I do not know
the internals of the Isabelle/JEdit implementation.
Makarius, what do you think, is this doable? Namely, to identify the
source files of a precompiled heap and to look up their definitions,
if the source files are unchanged? And, possibly, to make these files
read-only in Isabelle/JEdit?
Email Gateway (Aug 19 2022 at 13:52):From: Lars Noschinski <noschinl@in.tum.de>
This should work in practice, too (for example, clicking "TrueI" in "thm
TrueI" takes me to correct line in HOL.thy, which is part of the image).
Can you give a concrete example?
-- Lars
Email Gateway (Aug 19 2022 at 13:53):From: Makarius <makarius@sketis.net>
Indeed. What is still lacking on this thread is an elementary description
of the situation that lead to the initial surprise. So far there were
several educated guesses by Lars and myself what the perceived problem
actually is.
We don't need speculations about "bugs", "features", "intentions",
"designs" or whatever, but just some information about the empirical
observations. That is more difficult with the Prover IDE, since it is an
interactive game. So quite often, the problem is in timing and
reactivity, or lack thereof, but this is hard to phrase in prose text.
Makarius
Email Gateway (Aug 19 2022 at 13:53):From: Makarius <makarius@sketis.net>
On Wed, 26 Mar 2014, Gottfried Barrow wrote:
Gergely doesn't have any odd ideas about large-scale system
development at all. In fact, Gergely has the _right_ idea: in large
developments, there are _bound_ to be program behaviours that are not
expected, desirable, or intended."Unexpected, unintended, and undesirable" is a bogus definition of
"bug". That mainly describes what we as users want or don't want.If this was Microsoft, then you bash them because you can, because
they're some big, faceless corporation, and you use "bug" freely, and
don't worry about these things. Here, people aren't machines, and people
can be motivated or demotivated. If we demotivate people, then they
don't work as hard. No one here is dependent on me. I'm dependent on
others.
So far this is the most interesting contribution on the meta-discussion on
this thread.
The key problem that I see with the notions of "bugs + features + fixes"
is that the terminology suggests that you talk about a sufficiently small
and simple thing that you can manipulate arbitrarity (taking it into your
hands to do with it what you please). You might call that a "computer
program", but I prefer to call it a "plastic model of software reality".
So how about the real thing?
Alan Kay has given a nice lecture about "Programming and Scaling" some
years ago, which is interesting for various reasons, in particular:
(1) He as the inventor of the "object-oriented" movement repents after
all these decades, and sees more realistically the conceptual
mistakes they've made in the 1970/80-ies. I am not in a position to
blame him for mistakes of his youth, since I am much younger and
less experienced, while he has grown old and wise.
(2) A huge software system like Microsoft Windows 7 should be
visualized as Mexico City. Do you walk around there and to tell the
city administration about "bugs" that need to be "fixed"? The
people in charge won't take you seriously at all.
Isabelle is not as large and complex as Windows, not even the Linux
kernel, but it is definitely beyond the category of "computer program".
These are my opinions, expressed with the usual pedanticism. Most of my
emails are ignored.
I actually read more than half of your mails. Sometimes it takes time to
see the points behind the many words, but quite often I find useful hints
there. E.g. some months ago you have shared your observations about the
really ancient 'arities' command, which has no practical use today, but
can destroy a user's theory via uncontrolled axiomatization. So I've
sorted this out for the next release.
Makarius
Email Gateway (Aug 19 2022 at 13:53):From: Makarius <makarius@sketis.net>
On Thu, 27 Mar 2014, Gergely Buday wrote:
But now a question comes to my mind: the mentioned file, Lambda.thy was
not itself processed but I use a precompiled heap image of Nominal that
includes Lambda.thy as well. I understand that I might change Lambda.thy
but _in theory_ the original definitions of Lambda.thy _can_ be looked
up in the precompiled heap. Of course I do not know the internals of the
Isabelle/JEdit implementation.
This is actually the first time you mention Lambda.thy and Nominal on this
thread -- or I just overlooked it in the general noise.
When you open theory files from your base session (main HOL, HOL-Nominal,
whatever) you merely see the inactive source and an error in the theory
header that says "Cannot update finished theory".
So whatever you edit in that file, it is outside the formal document
model. And of course, there are no active links, as usual for unprocessed
text in that shade of pink. If the error is missing or the coloring of
the body is not there, that is a problem to be sorted out.
Makarius, what do you think, is this doable? Namely, to identify the
source files of a precompiled heap and to look up their definitions, if
the source files are unchanged? And, possibly, to make these files
read-only in Isabelle/JEdit?
I am trying for years to sort out the relation of precompiled heaps and
their sources wrt. the active editor session. This is not imminent --
users need to cope with a situation inherited from the past. What does
have a chance for the coming release is a reform that de-emphasizes heap
images, such that you can edit whatever theories you like without thinking
about batch sessions. Right now you still need the correct heap to be able
to process certain sources at all, for historic reasons of the theory name
space.
Makarius
Email Gateway (Aug 19 2022 at 14:05):From: Gergely Buday <gbuday@gmail.com>
Hi,
using ctrl-click to find the definition of an identifier is indeed
valuable. However, it fails to work sometimes. I cannot make bold claims
about the conditions, but one I have met is:
the definition is in the same file
Is this a feature, not a bug?
Email Gateway (Aug 19 2022 at 14:05):From: Lars Noschinski <noschinl@in.tum.de>
Normally this should work.
A situation where ctrl-click does not take me to the expected location
is if I am in a locale context (opened by context or implicitly via (in
locale)). Then (sometimes?) the click takes me to the opening of the
context, not to place where the lemma was defined.
Best regards,
Lars
Email Gateway (Aug 19 2022 at 14:05):From: Makarius <makarius@sketis.net>
Can you point to a definition of "feature" or "bug"? Both don't have any
meaning to me. I mean this seriously.
One of the key concepts of PIDE is that the prover can report some aspects
of its internal workings to the document source, via markup that is
positioned in the proper place. Aspects, not everything -- the prover is
doing many more things internally.
This restriction was the initial breakthrough of the Prover IDE approach.
Aefore the IDE guys would ask for everything and get nothing. Afterwards
it became feasible to reform the prover to support IDEs adequately.
I've spent the past 5 years or so providing more and more informative
markup from the bottom of the prover. This is a never-ending process, as
far as I can fortell.
Files are generally not very interesting in PIDE -- the prover does not
really know about them. It matters more if something has been loaded into
the underlying heap image in batch mode, or within the current editor
session.
Makarius
Email Gateway (Aug 19 2022 at 14:05):From: Makarius <makarius@sketis.net>
There is a conceptual problem here that was already known in 2008 when no
concrete PIDE markup was available yet. Contexts (class, locale etc.) are
like a second-order mechanism on top of plain declarations, and the
position reports should somehow take the relation of the two into account,
but don't do anything yet.
PIDE is like a high speed train that runs already at 550 km/h, while only
half of the railway lines are operative.
Makarius
Email Gateway (Aug 19 2022 at 14:05):From: Gergely Buday <gbuday@gmail.com>
On 26 March 2014 16:14, Makarius <makarius@sketis.net> wrote:
using ctrl-click to find the definition of an identifier is indeed valuable. However, it fails to work sometimes. I cannot make bold claims about the conditions, but one I have met is:
the definition is in the same file
Is this a feature, not a bug?
Can you point to a definition of "feature" or "bug"? Both don't have any meaning to me. I mean this seriously.
Yes I am afraid you are serious here. But ordinary language is not
"defined". People usually use the word feature when the behaviour is
expected by the software writer, and, possibly, by the users, while a
bug is something that is not expected and even unpleasant.
I've spent the past 5 years or so providing more and more informative markup from the bottom of the prover. This is a never-ending process, as far as I can fortell.
And we are all grateful for your efforts. I mean this seriously.
Files are generally not very interesting in PIDE -- the prover does not really know about them. It matters more if something has been loaded into the underlying heap image in batch mode, or within the current editor session.
Thanks, this explains what has happened. This is a good specification
of the expected behaviour. Now I know what to expect and my test with
the modified expectation ran through.
Email Gateway (Aug 19 2022 at 14:06):From: Makarius <makarius@sketis.net>
This is a slightly odd idea about system development at a large scale.
Quite often, the not so ideal behaviour is known and expected by the
people who did the job, but there were reasons why it could not be done
better in a certain situation, or forcing it would make things worse.
Equally often, users expect much less than could be done, either in
principle or in actuality after taking a fresh look at the bigger picture.
Above you say "it fails to work sometimes". What does that mean? Reading
between the lines I guess it might be any of the following behaviour in
Isabelle2013-2:
* An entity reference that points to a file from the base session (e.g.
from Isabelle/HOL) merely resolves to the file + line number, but not
the character precise offset.
* An entity reference that points to a file within Isabelle/Pure merely
points to the start of the file, not even the line number.
I could have put that in the manual, to make it an official "feature", but
that would be a bit silly. It does not really qualify as "bug" either,
because there is no real problem here: some entity references are more
precise than others, and better than no references. The hypersearch
facility of jEdit helps to finish the procedure to find something
somewhere.
For the coming release there will be more support for files of the base
session and bootstrap files of Pure. Due to other improvements in
external file handling within theories, the file + line reference suddenly
spoilt the game, so I invested more work to make the landing positions of
links more precise also in that case.
Does that "fix a bug" as many people would say? I say no, because there
was nothing "loose" and there is never an end of what else could be
improved, i.e. a "fixed situation". For example, after recent
improvements I could imagine a visual representation of "scope groups"
(binding position plus occurrences) that can be seen in other IDEs.
After that 5 more things that I don't dare to spell out yet.
Makarius
Email Gateway (Aug 19 2022 at 14:06):From: David Greenaway <david.greenaway@nicta.com.au>
On 27/03/14 05:08, Makarius wrote:
On Wed, 26 Mar 2014, Gergely Buday wrote:
On 26 March 2014 16:14, Makarius <makarius@sketis.net> wrote:
Can you point to a definition of "feature" or "bug"? Both don't have
any meaning to me. I mean this seriously.
I'll bite:
A bug is a behaviour of a computer program that is unexpected,
unintended and undesirable.
The behaviour reported was _unexpected_ by Gergely. The behaviour is
presumably _undesirable_ to Gergely. However, the behaviour was
_intended_ by the developer (you, I presume), so, in this case, the
behaviour is not a bug, but simply a design trade-off.
Gergely's original question "Is this a feature, not a bug?", was a query
to work out the last piece of the puzzle above, because trying to work
out the intention of the designer is _hard_.
Yes I am afraid you are serious here. But ordinary language is not
"defined". People usually use the word feature when the behaviour is
expected by the software writer, and, possibly, by the users, while
a bug is something that is not expected and even unpleasant.This is a slightly odd idea about system development at a large scale.
Quite often, the not so ideal behaviour is known and expected by the
people who did the job, but there were reasons why it could not be
done better in a certain situation, or forcing it would make things
worse. Equally often, users expect much less than could be done,
either in principle or in actuality after taking a fresh look at the
bigger picture.
Gergely doesn't have any odd ideas about large-scale system
development at all. In fact, Gergely has the _right_ idea: in large
developments, there are _bound_ to be program behaviours that are not
expected, desirable, or intended.
The fact that Gergely hit a design trade-off and asked publicly as to
whether it was intended or not is simply a sign that the behaviour is
either ill-document and/or the UI is insufficient.
Above you say "it fails to work sometimes". What does that mean?
Reading between the lines I guess it might be any of the following
behaviour in Isabelle2013-2:* An entity reference that points to a file from the base session
(e.g. from Isabelle/HOL) merely resolves to the file + line number,
but not the character precise offset.* An entity reference that points to a file within Isabelle/Pure
merely points to the start of the file, not even the line number.I could have put that in the manual, to make it an official "feature",
but that would be a bit silly. It does not really qualify as "bug"
either, because there is no real problem here: some entity references
are more precise than others, and better than no references.
Again, it is a design trade-off. And yes, you _should_ put it in the
manual, not because that would change the status of the behaviour from
"bug" to "not bug", but so that users understand what is going on.
Better still, if a design trade-off needs to be made, modify the UI so
that the user's expectations are met. A simple tooltip stating "Cannot
determine source location" when the user tries to Ctrl+Click such a term
gives the user a strong hint that they are hitting a design limitation,
and not a bug.
Cheers,
David
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 14:06):From: Gottfried Barrow <igbi@gmx.com>
On 14-03-26 16:33, David Greenaway wrote:
I'll bite:
A bug is a behaviour of a computer program that is unexpected,
unintended and undesirable.
I actually try to limit the amount of traffic I generate here, and
Makarius Wenzel doesn't really need me to help him out, so I'll check
out of this thread after this.
It's more general than that. A bug implies something is wrong, and to
know something is wrong, you have to have inside information, though at
times, it's fairly safe to claim there's a bug.
I exported functions that used functions of type 'prop', and the code
generator generated some totally bogus code for Scala and Haskell (or
did it?). On my end, it was unexpected and undesirable. On their end,
"unintended" would imply they even care about exporting 'prop' functions.
The issue at hand, that a link doesn't take you where you want, is not
even remotely a bug. It's a feature which doesn't meet our expectations,
because other features have fully met our expectations, which has made
us very unsatisfied, and downright ticked off, because the one feature
showed us how easy life could be if we lived in a more perfect world.
I could say it's wrong for people to complain about that kind of thing,
but it's not. Anything put out for public consumption is subject to
critique. People are free to produce, and we're free to complain.
Critiquing becomes a matter of perception. I myself understand there's
only one proof assistant in the whole world that has the features I
need, no exaggeration. It bares emphasizing, there's only one, and the
one there happens to be is extraordinarily powerful, and free, too. I
have a very bad attitude about many things involving proof assistants,
but I control myself, a little.
Gergely doesn't have any odd ideas about large-scale system
development at all. In fact, Gergely has the _right_ idea: in large
developments, there are _bound_ to be program behaviours that are not
expected, desirable, or intended.
"Unexpected, unintended, and undesirable" is a bogus definition of
"bug". That mainly describes what we as users want or don't want.
If this was Microsoft, then you bash them because you can, because
they're some big, faceless corporation, and you use "bug" freely, and
don't worry about these things. Here, people aren't machines, and people
can be motivated or demotivated. If we demotivate people, then they
don't work as hard. No one here is dependent on me. I'm dependent on others.
These are my opinions, expressed with the usual pedanticism. Most of my
emails are ignored. That would be good here, too.
Regards,
GB
Email Gateway (Aug 19 2022 at 14:06):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Some of the subsequent emails to this may have taken it too seriously.
Here are two possible definitions -)
(1) If the developers can't be bothered to fix it, it is a feature; if
they can, then it is a bug
(2) Something is a bug if it a program behaves differently from how the
documentation says it should behave. (This means that if there is no
documentation, then there are no bugs).
Regrettably, I can't claim originality in either of these approaches to
bug-avoidance.
Jeremy
Last updated: Apr 18 2024 at 16:19 UTC