Email Gateway (Aug 19 2022 at 12:03): Email Gateway (Aug 19 2022 at 12:03):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the Isabelle2013-1 release is scheduled for November 2013. Before actual
lift-off we have approx. 5 weeks of public testing of release candidates.
See https://bitbucket.org/isabelle_project/isabelle-release for the main
website where this is organized. There is also a link to an issue tracker on
the same Bitbucket site.
The website with downloads etc. is
http://isabelle.in.tum.de/website-Isabelle2013-1-RC1
Observations from testing release candidates may be discussed here on
isabelle-users (not isabelle-dev), on the bitbucket tracker, or via private
mail.
Active participation in testing is important to iron out small problems,
and raise the overall quality of the system for everybody. There is a
particular challenge to make all platforms work smoothly: Linux, Windows,
Mac OS X. The Isabelle quality standards and user expectations have
continously increased in recent years, while all major operating system
vendors and distributors are on a slight downwards curve.
The time to sort out issues is now. Note that I will myself be on
vacation from 17-Oct to 04-Nov and make the final launch afterwards. In
the meantime we have time for 2-3 release candidates.
Makarius
Email Gateway (Aug 19 2022 at 12:13):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
Something I noticed after switching my brain to beginners mode and
starting Isabelle "for the first time".
It might be helpful if Isabelle/jEdit would provide some more tool tips.
I'm talking especially about the following buttons (with some very crude
suggestions attached):
- Find (e.g., "Search for existing facts")
- Output (e.g., "Isabelle's reply to the command at the cursor position")
- Sledgehammer (e.g., "Apply external provers to the current proof goal")
- Symbols (e.g., "A collection of available mathematical symbols")
- Documentation (e.g., "Documents describing all things Isabelle and
examples")
- Sidekick (I have no clue... I never use it myself; could somebody
enlighten me about its use cases?)
- Theories (e.g., "Collection of all loaded theories (a red(?) bar
indicates how much of each theory has still to be processed)")
cheers
chris
Email Gateway (Aug 19 2022 at 12:17):From: Makarius <makarius@sketis.net>
This is a regular jEdit plugin. The Plugin Manager provides the following
blurb:
The SideKick plugin provides a dockable window in which other plugins
can display buffer structure in a tree view.
Thus it becomes the default tree view of various jEdit "modes". It is
very easy to set up programmatically, but difficult to get further beyond
its basic operations.
Did you notice already that the Isabelle NEWS file now has that as well?
Just a few lines of Scala with some regexps to reconstruct a tree
structure of our traditional text file layout.
In the longer run, I would like to see a specific tree (or graph) view on
Isabelle theories -- all of them, not just one buffer.
Makarius
Email Gateway (Aug 19 2022 at 12:18):From: Makarius <makarius@sketis.net>
Another application are session ROOT files. E.g. IsaFoR/IsaFor/ROOT now
gets a general overview in Sidekick.
I am adding the following to NEWS to make this more explicit:
* Improved support of various "minor modes" for Isabelle NEWS,
options, session ROOT etc., with completion and SideKick tree view.
Makarius
Email Gateway (Aug 19 2022 at 12:19):From: "C. Diekmann" <diekmann@in.tum.de>
Dear all,
I encountered the following when testing Isabelle2013-1-RC1.
When using code_modulename, the buffer displays a Warning:
"Legacy feature! prefer "code_identifier" over "code_modulename""
However, the warning is not visualized by jEdit (I expected a yellow
marking at the left border)
Say I have my mathematical definitions in X.thy and an executable
implementation in X_impl.thy. I used
code_modulename Scala X_impl X
to export the code in the module X, not X_impl. How do I translate
this using the suggested code_identifier?
On a German keyboard layout, the "Go to Recent Buffer" does (still) not work.
Cheers
Cornelius
Email Gateway (Aug 19 2022 at 12:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Cornelius,
The former "code_modulename Scala Theory Module" is now
code_identifer code_module Theory => (Scala) Module
You can now use code_identifier also with other kinds of code generator data. For example,
the following moves a single constant foo to module M and renames it to bar:
code_identifier constant c => (Scala) "M.bar"
Best,
Andreas
Email Gateway (Aug 19 2022 at 12:19):From: Makarius <makarius@sketis.net>
Is this Linux / Windows or Mac OS X?
jEdit defines many shortcuts, but not all of them are reachable on all
keyboards. Recent jEdit releases have improved this a little bit, at the
cost of introducing further confusion due to alternative keymaps. In
current Isabelle/jEdit I have tried to pick up a few alternatives and make
them the default in jEdit.props -- this will end up in your "imported"
keymap after the first start of the application.
For "Go to Recent Buffer" there is C-CIRCUMFLEX as alternative shortcut --
I am using this routinely on German Linux keyboard.
Note that the jEdit menus usually only show the primary shortcut. You can
browse through "Golbal Options / Shortcuts" to see what is there.
Makarius
Email Gateway (Aug 19 2022 at 12:19):From: Makarius <makarius@sketis.net>
Florian Haftman is emitting a warning in the parser of the command, so it
ends up in slightly different slots than messages produced at actual
run-time. Since some related legacy warnings already happen at runtime, I
have now adapted code_modulename accordingly -- for the next release
candidate that is anticipated during this week.
Warning, tracing, error messages are notoriously difficult to get right in
all respects, since they only happen in special situations. Legacy
message are particularly bad, since they are to disappear anyway together
with the old feature that they inform about. This is called in Isabelle
jargon "renovation before demolition".
Makarius
Email Gateway (Aug 19 2022 at 12:20):From: Makarius <makarius@sketis.net>
On Mon, 7 Oct 2013, C. Diekmann wrote:
Is this Linux / Windows or Mac OS X?
Linux, Ubuntu
Which of its many versions?
For "Go to Recent Buffer" there is C-CIRCUMFLEX as alternative shortcut
-- I am using this routinely on German Linux keyboard.I see that C+` and C+^ are both defined but they don't work. I can't
even press C+^ or C+´ to install these shortcuts in jEdit. xev emits
events for these keys.
xev represents only one of many layers of X11 where keystrokes have to
pass through to get eventually to the application. All this keyboard
handling is a bit messed up on modern operating systems, and Linux is
particularly critical.
The guy who still tries to get rid of decades of X11 legacy and turn it
into better use as "Wayland" got a lot of resistance from traditionalists,
and it still remains to be seen if this promising project will ever get to
the point where Oracle might support it.
What counts for Java / Swing applications like Isabelle/jEdit can be seen
in the KeyEventDemo from
http://docs.oracle.com/javase/tutorial/uiswing/events/keylistener.html
This little Java application is easy to compile with javac and run with
"isabelle java" -- just to make sure you have exactly the same JRE.
jEdit then has its own filters (workarounds and "fixes" for odd and
historic behaviour) that might cause extra problems.
I've just tried myself again as a freshly created test user on Xbuntu
13.04 and Isabelle2013-1-RC1 with factory default: C-CIRCUMFLEX and
A-CIRCUMFLEX both work on my German Sony Vaio.
Makarius
Email Gateway (Aug 19 2022 at 12:20):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
I find that on my machine (running the notorious 64bit Fedora 19 with
Gnome) when using the Sledgehammer panel, very often (it feels like the
majority of cases) after clicking "Apply", "Cancel" has no effect (the
whole buffer is grayish highlighted). In such cases sometimes clicking
"Apply" again actually cancels the ATPs, but sometimes only restarting
Isabelle/jEdit helps (or maybe I would have to wait longer than 1 minute).
cheers
chris
Email Gateway (Aug 19 2022 at 12:21):From: "C. Diekmann" <diekmann@in.tum.de>
Same here, Ubuntu 12.04.3 LTS, 64Bit, Unity (shame on me!)
Email Gateway (Aug 19 2022 at 12:21):From: "C. Diekmann" <diekmann@in.tum.de>
2013/10/7 Makarius <makarius@sketis.net>:
Linux, Ubuntu
Which of its many versions?
Ubuntu 12.04.3 LTS, 64Bit, Unity
For "Go to Recent Buffer" there is C-CIRCUMFLEX as alternative shortcut
-- I am using this routinely on German Linux keyboard.
I see that C+` and C+^ are both defined but they don't work. I can't
even press C+^ or C+´ to install these shortcuts in jEdit.What counts for Java / Swing applications like Isabelle/jEdit can be seen in
the KeyEventDemo from
http://docs.oracle.com/javase/tutorial/uiswing/events/keylistener.htmlThis little Java application is easy to compile with javac and run with
"isabelle java" -- just to make sure you have exactly the same JRE.
ctrl+´ produces
KEY PRESSED:
key code = 17 (Ctrl)
extended modifiers = 128 (Ctrl)
action key? NO
key location: left
KEY RELEASED:
key code = 129 (Dead Acute)
extended modifiers = 128 (Ctrl)
action key? NO
key location: standard
KEY RELEASED:
key code = 17 (Ctrl)
extended modifiers = 0 (no extended modifiers)
action key? NO
key location: left
ctrl+^ produces
KEY PRESSED:
key code = 17 (Ctrl)
extended modifiers = 128 (Ctrl)
action key? NO
key location: left
KEY RELEASED:
key code = 130 (Dead Circumflex)
extended modifiers = 128 (Ctrl)
action key? NO
key location: standard
KEY RELEASED:
key code = 17 (Ctrl)
extended modifiers = 0 (no extended modifiers)
action key? NO
key location: left
jEdit tested with
Swing look&feel: Nimbus, GTK+, CDE/Motif, Metal
Cornelius
Email Gateway (Aug 19 2022 at 12:21):From: Makarius <makarius@sketis.net>
These keys are treated as "dead" here, so it is understandable that they
behave slightly differently than normal ones.
I have myself developed this reflex to choose "German no-dead keys" as
Linux keymap already 15 years ago, so I could not imagine that the normal
default with dead keys is actually active. My current Sony Vaio
actually requires further bending and stretching of keyboard defaults via
.Xmodmap to make it usable for me -- normally I try to avoid that.
Anyway, this might be a topic for the general jEdit mailing list at
Sourceforge. Better international keyboard support has been started about
one year ago, but it is still not quite finished.
Makarius
Email Gateway (Aug 19 2022 at 12:22):From: Makarius <makarius@sketis.net>
On Tue, 8 Oct 2013, Christian Sternagel wrote:
I find that on my machine (running the notorious 64bit Fedora 19 with
Gnome) when using the Sledgehammer panel, very often (it feels like the
majority of cases) after clicking "Apply", "Cancel" has no effect (the
whole buffer is grayish highlighted).
This should be different in Isabelle2013-1-RC2, and hopefully better.
In such cases sometimes clicking "Apply" again actually cancels the
ATPs, but sometimes only restarting Isabelle/jEdit helps (or maybe I
would have to wait longer than 1 minute).
In such cases of uncertainty I merely reload the current buffer (F5),
which is normallly sufficient. This operation is somehow reminiscent of
proof-tract-buffer in Proof General :-)
For sledgehammer in particular, the "interaction state" is tied to the
syntactic command span in the text. So if that is edited or removed any
associated operations on the prover side should be canceled. The "Locate"
button reveals the command that is associated with the current query
process.
Makarius
Email Gateway (Aug 19 2022 at 12:23):From: Makarius <makarius@sketis.net>
I don't see a reason for being ashamed of Ubuntu classic. At least at
12.04 LTS it is still a fine system, but I've got many problems with
13.04, and 13.10 beta totally bombed my test installation. Right now I am
glad to have Xubuntu 13.04 in a mostly stable state on my main machine.
All the social pressure against recent moves of Canonical have lead to
further steps towards the degradation of major Linux distributions. The
Linux Mint fork of Ubuntu is particularly bad -- first they claim to
support Java better out of the box, then they make it all very weak, with
standard problems of X11 window managers against Java AWT that Open JDK
insiders already know for years.
Makarius
Email Gateway (Aug 19 2022 at 12:39):From: Makarius <makarius@sketis.net>
These buttons are managed by the "dockable window manager" of jEdit. I
can't tell if that supports tooltips here.
That subsystem of jEdit is generally quite useful, but it has some snags
that are worse than missing tooltips: windows don't necessarily stay on
top of the main view. This is particularly bad, if the view is in
"full-screen" mode, which now works more than 50% of the time of various
platforms.
People who feel like getting engaged in general jEdit improvements, should
look around at http://www.jedit.org/ and
http://sourceforge.net/projects/jedit/
There has been quite some fluctation (and also loss) of brain power of the
project in recent years, but it is definitely possible to move forward
reasonably fast. (Faster than Oracle does.) I've recently started an
initiative to get jEdit on Mac OS X and Java 7 back into shape, and it is
expected to be all there in the next jEdit release. (Isabelle/jEdit in
Isabelle2013-1 has its own adjustments for that right now.)
Makarius
Last updated: Nov 21 2024 at 12:39 UTC