KeYmaeraX-release icon indicating copy to clipboard operation
KeYmaeraX-release copied to clipboard

Published 20 hours ago • verified publisher icon LS-Lab

[UI] [enhancement] Not obvious to user why diRule breaks tactic editor goal-switching

Open rbohrer opened this issue 3 years ago • 6 comments

Version: 4.9.8 Reproduce:

  1. run attached archive's tactic
  2. open proof interface
  3. go to tactic editor
  4. try to navigate to the second TODO under "dC". It won't let you and the user won't know why

I'm assuming it's by-design that you can't navigate to these "todos" and that it's a result of the expandAllDefs and delayed USubst. However it may look like a bug to users without any added context.

Low priority, easy to explain to students

tactic-display-on-limited-editing-redo.kyx.txt

rbohrer avatar Jan 13 '22 15:01 rbohrer

The attached archive seems to not fit the bug description, please update.

smitsch avatar Jan 18 '22 19:01 smitsch

Updated file and description, my bad! I believe the same applies to issue #99, will check that now too

rbohrer avatar Jan 19 '22 14:01 rbohrer

Was unable to reproduce it, may have been fixed with some earlier improvement. Please check.

smitsch avatar Jan 21 '22 16:01 smitsch

I built the latest commit (6211d34d87) and reproduced the bug. To clarify: when I click on the second TODO, the mouse cursor will move, but the arrow symbol and green bar do not move, and the UI does not navigate to the second tab.

Additional info: OS: Windows 10 Enterprise Browser: Chrome Version 97.0.4692.71 (Official Build) (64-bit) JDK: Openjdk 11.0.13

Let me know if you need anything else, thanks!

rbohrer avatar Jan 24 '22 20:01 rbohrer

Still not able to reproduce. Is there anything useful in the View->Developer->JavaScript Console in Chrome?

smitsch avatar Feb 03 '22 21:02 smitsch

I don't think so from last time I checked but it may be after the next release when I get chance to debug again in depth so feel free to let it wait until after release

On Thu, Feb 3, 2022, 4:57 PM Stefan Mitsch @.***> wrote:

Still not able to reproduce. Is there anything useful in the View->Developer->JavaScript Console in Chrome?

— Reply to this email directly, view it on GitHub https://github.com/LS-Lab/KeYmaeraX-release/issues/98#issuecomment-1029439295, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAO6WYKV2OYP7MG5JLIRDJDUZL24PANCNFSM5L4C6JJQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you authored the thread.Message ID: @.***>

rbohrer avatar Feb 03 '22 22:02 rbohrer