Email Gateway (Feb 06 2025 at 07:05): Email Gateway (Feb 06 2025 at 07:05):From: Ian Hayes <cl-isabelle-users@lists.cam.ac.uk>
I'm using MacOS Sequoia 15.3.
Issue 1:
For the attached theory file,
a Command click on the reference to lemma subset in locale test2, it
takes one to the lemma in locale test1, however,
a Command click on the reference to HT_def in locale test2 it takes one
to the head of locale test2.
A Command click on the reference to HT_def in locale test1 it takes one
to the definition (in test1) as expected.
A Command click on the reference to XX_def in locale test2 it takes one
to the definition (outside the locales) as expected.
The difference is that XX is defined outside the locale but HT is
defined inside.
I think same behaviour occurs in Isabelle-2024.
Issue 2: Again this is not a new issue.
A slight movement of the mouse when Command clicking through to a
lemma/definition means it fails and selects the character under the
cursor. I'm guessing this is something to do with the fact that the
Command click occurs, not on pressing the mouse, but when it is then
released. For example, if you Command press and move the mouse a little
and then release, it won't go through to the definition but rather
selects the text under the cursor. And the behaviour is worse when I use
an Apple magic mouse in place of an old mouse -- I suspect because the
Magic mouse will generate a small movement more easily.
A similar issue occurs when clicking on a the output of sledgehammer to
get it to copy the suggested proof into the theory file.
Another issue is double-clicking the name of a theory in the theories
menu is also flaky if the mouse moves slightly between the two clicks,
even if one remains within the same menu item.
Many thanks in advance
Ian
On 4/2/2025 05:22, Makarius wrote:
Dear Isabelle users,
we are now ready to start the release process for Isabelle2025 (March
2025). See also the continuously updated blog entry
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025The current release candidate is available from
https://isabelle.in.tum.de/website-Isabelle2025-RC1A corresponding version of the Archive of Formal Proofs is
https://isabelle.sketis.net/repos/afp-devel/rev/634f3bc5f94bThe NEWS and ANNOUNCE files are already up-to-date, but some
documentation still requires update.The rules of the game are the same as in the past few decades: NOW is
the window of opportunity to discuss observations and problems, in
order to get changes into the code-base. The final release remains
unchangeable, until the next one (8-10 months later).Any feedback about Isabelle release candidates should be posted with a
meaningful Subject, not just a clone of this announcement.Makarius
Email Gateway (Feb 06 2025 at 19:48):From: Makarius <makarius@sketis.net>
On 06/02/2025 08:04, Ian Hayes (via cl-isabelle-users Mailing List) wrote:
Issue 1:
For the attached theory file,
a Command click on the reference to lemma subset in locale test2, it takes one
to the lemma in locale test1, however,
a Command click on the reference to HT_def in locale test2 it takes one to the
head of locale test2.
A Command click on the reference to HT_def in locale test1 it takes one to the
definition (in test1) as expected.
A Command click on the reference to XX_def in locale test2 it takes one to the
definition (outside the locales) as expected.
The difference is that XX is defined outside the locale but HT is defined inside.
I think same behaviour occurs in Isabelle-2024.
This refers to the attached test2.thy which imports test1, but I did not see
test1.thy: using "imports Main" instead works, but maybe you intended to show
something else in test1.thy?
Anyway, I have clicked through the formal entities as sketched above, and
don't see anything suspicious. Note that "locale test2 = test1 ..." in is not
just a plain import, but a new locale based on existing locale(s) via locale
expressions that are internally turned into morphisms. Formal entities of the
new locale then get the position of the morphism that was applied to the old
entities, instead of the old entities, or both the morphism and entity. That
could be certainly improved at some point, but it is not a regression from
Isabelle versions in the past decade.
Side-remark: mixing up theory names (test1, test2) and local names (test1,
test2) is generally a bad idea: the name-space policies have been specifically
designed some decades ago under the assumption that both kinds are disjoint.
This is easy to achieve by following ancient naming conventions: theory names
capitalized, almost everything inside a theory lower-case (including types,
classes, locales). A rare use of capitalized names inside a theory is OK.
Issue 2: Again this is not a new issue.
A slight movement of the mouse when Command clicking through to a lemma/
definition means it fails and selects the character under the cursor. I'm
guessing this is something to do with the fact that the Command click occurs,
not on pressing the mouse, but when it is then released. For example, if you
Command press and move the mouse a little and then release, it won't go
through to the definition but rather selects the text under the cursor. And
the behaviour is worse when I use an Apple magic mouse in place of an old
mouse -- I suspect because the Magic mouse will generate a small movement more
easily.
It sounds like input device problems. I don't have an Apple mouse nor a
touchpad to test it: I always use an old Logitech wheel-mouse with my test
machine Mac Mini for testing.
I do have macOS Sequoia 15.3 available.
A similar issue occurs when clicking on a the output of sledgehammer to get it
to copy the suggested proof into the theory file.Another issue is double-clicking the name of a theory in the theories menu is
also flaky if the mouse moves slightly between the two clicks, even if one
remains within the same menu item.
I cannot reproduce that with my Apple test equipment.
Can seasoned Apple user confirm any of these problems? Is there anything new
in macOS Sequoia and/or Isabelle2025-RC1?
Makarius
Email Gateway (Feb 07 2025 at 15:10):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Issue 2: Again this is not a new issue.
A slight movement of the mouse when Command clicking through to a lemma/ definition means it fails and selects the character under the cursor. I'm guessing this is something to do with the fact that the Command click occurs, not on pressing the mouse, but when it is then released. For example, if you Command press and move the mouse a little and then release, it won't go through to the definition but rather selects the text under the cursor. And the behaviour is worse when I use an Apple magic mouse in place of an old mouse -- I suspect because the Magic mouse will generate a small movement more easily.It sounds like input device problems. I don't have an Apple mouse nor a touchpad to test it: I always use an old Logitech wheel-mouse with my test machine Mac Mini for testing.
I do have macOS Sequoia 15.3 available.
A similar issue occurs when clicking on a the output of sledgehammer to get it to copy the suggested proof into the theory file.
Another issue is double-clicking the name of a theory in the theories menu is also flaky if the mouse moves slightly between the two clicks, even if one remains within the same menu item.I cannot reproduce that with my Apple test equipment.
Can seasoned Apple user confirm any of these problems? Is there anything new in macOS Sequoia and/or Isabelle2025-RC1?
I can confirm the behaviour: if you move the mouse-pointer between click-and-release or between a double-click, then this
is interpreted differently than a standard click and double-click without movement when running Isabelle 2025-RC1 and Seqouia 15.3.
However, neither with my laptop touchpad nor with a classical (non-magic) mouse I a have a problem that there actually
is movement between click-release or double-click, if I do not (on purpose) move my finger on the touchpad, or move the mouse
during these actions.
Best,
René
Email Gateway (Feb 10 2025 at 01:50):From: Ian Hayes <cl-isabelle-users@lists.cam.ac.uk>
Hi Makarius,
Issue 1: Apologies test2 should just include Main (I was experimenting
with references across theory files and found that it was just across
locales so copied test1.thy into test2.thy so there was just a single
file but forgot to replace the import). I agree it is not a regression
and look forward to improvement at some point in the future.
Side-remark: The naming was me being lazy in building a minimal test file.
Issue2: For MacOS for a left mouse click there are the following mouse
events:
* Press down the button: NSLeftMouseDown which invokes mouseDown
* Move the mouse while pressing the button: NSLeftMouseDragged which
invokes mouseDragged
* Release the button:|NSLeftMouseUp which invokesmouseUp|
* ||Move the mouse without pressing any button: NSMouseMoved which
invokes mouseMoved
A combination of mouseDown-mouseDragged-mouseUp selects the text between
the coordinates of the mouseDown and mouseUp. The problem with
Command-click would appear to be that the text selection behaviour is
happening when the Command key is held down (for a click through) and
the selection behaviour is taking precedence over the Command click*. If
the selection behaviour was disabled while the Command key is held down
that might fix the problem. Alternatively, the Command click behaviour
should take precedence over selection of text.
*In practice, sometimes it recognises the Command-click and other it
recognises a selection, so this looks like a classic (concurrency) race
between the two actions. With the Command key held down, mouseDown-move
a few characters-mouseUp always selects the text, even if it is in the
one name.
An alternative scenario is the following.
The mouseDown-mouseUp combination (*without *Command key held) moves the
cursor to the location of the mouse. With the Command key held down, it
non-deterministically either moves the cursor or clicks through to the
definition. Again this looks like a race between the two actions. If the
cursor movement action was disabled while the Command key is held down
or the Command-click given precedence that may work.
From my experimentation, it appears the Command-click does not happen
until the mouse is released (mouseUp). If the Command click action was
invoked on mouseDown, the issue might be resolved.
Using the track-pad rather than the mouse is more reliable but can still
exhibit the same behaviour. The detailed behaviour is that with Command
held down, mouseDown moves the cursor to the mouse location and on
mouseUp it moves it to the definition of the item. On some occasions it
just moves the cursor to the mouse location and does not go to the
definition, and on other occasions it moves the cursor to the mouse
position and removes the highlight from the item under the mouse, where
by highlight, I mean the highlighting that occurs when one presses the
Command key.
Another symptom is that if the cursor is on name and the Command key
held, the name is not highlighted, but if one leaves the Command key
held and moves the cursor a little, the name is then highlighted.
A related symptom is that when the Command key is held and the name
highlighted for a couple of seconds, a pop-up window appears and the
highlight is removed from the name until one moves the cursor again.
An old Dell wheel mouse is more reliable than the track-pad, which is in
turn more reliable than a magic mouse. But note that even with the old
Dell mouse a small mouse movement between down and up gives a cursor
move or select text action, and not a click-through to definition
action. The symptoms occur on both my old M1 laptop and a new mini with
a fresh install of everything.
Probably not relevant here but in the Finder under MacOS, if wants to
select multiple files, one holds down the Command key while clicking on
each file.
Disclaimer: I'm not a mouse event handling expert.
Thanks in advance
Ian
On 7/2/2025 05:47, Makarius wrote:
On 06/02/2025 08:04, Ian Hayes (via cl-isabelle-users Mailing List)
wrote:Issue 1:
For the attached theory file,
a Command click on the reference to lemma subset in locale test2, it
takes one to the lemma in locale test1, however,
a Command click on the reference to HT_def in locale test2 it takes
one to the head of locale test2.
A Command click on the reference to HT_def in locale test1 it takes
one to the definition (in test1) as expected.
A Command click on the reference to XX_def in locale test2 it takes
one to the definition (outside the locales) as expected.
The difference is that XX is defined outside the locale but HT is
defined inside.
I think same behaviour occurs in Isabelle-2024.This refers to the attached test2.thy which imports test1, but I did
not see test1.thy: using "imports Main" instead works, but maybe you
intended to show something else in test1.thy?Anyway, I have clicked through the formal entities as sketched above,
and don't see anything suspicious. Note that "locale test2 = test1
..." in is not just a plain import, but a new locale based on existing
locale(s) via locale expressions that are internally turned into
morphisms. Formal entities of the new locale then get the position of
the morphism that was applied to the old entities, instead of the old
entities, or both the morphism and entity. That could be certainly
improved at some point, but it is not a regression from Isabelle
versions in the past decade.Side-remark: mixing up theory names (test1, test2) and local names
(test1, test2) is generally a bad idea: the name-space policies have
been specifically designed some decades ago under the assumption that
both kinds are disjoint. This is easy to achieve by following ancient
naming conventions: theory names capitalized, almost everything inside
a theory lower-case (including types, classes, locales). A rare use of
capitalized names inside a theory is OK.Issue 2: Again this is not a new issue.
A slight movement of the mouse when Command clicking through to a
lemma/ definition means it fails and selects the character under the
cursor. I'm guessing this is something to do with the fact that the
Command click occurs, not on pressing the mouse, but when it is then
released. For example, if you Command press and move the mouse a
little and then release, it won't go through to the definition but
rather selects the text under the cursor. And the behaviour is worse
when I use an Apple magic mouse in place of an old mouse -- I suspect
because the Magic mouse will generate a small movement more easily.It sounds like input device problems. I don't have an Apple mouse nor
a touchpad to test it: I always use an old Logitech wheel-mouse with
my test machine Mac Mini for testing.I do have macOS Sequoia 15.3 available.
A similar issue occurs when clicking on a the output of sledgehammer
to get it to copy the suggested proof into the theory file.Another issue is double-clicking the name of a theory in the theories
menu is also flaky if the mouse moves slightly between the two
clicks, even if one remains within the same menu item.I cannot reproduce that with my Apple test equipment.
Can seasoned Apple user confirm any of these problems? Is there
anything new in macOS Sequoia and/or Isabelle2025-RC1?Makarius
Last updated: Mar 09 2025 at 12:28 UTC