Email Gateway (Aug 19 2022 at 14:50): Email Gateway (Aug 19 2022 at 14:50):From: Makarius <makarius@sketis.net>
Now I understand what you mean. I will look at this again after next week
at Vienna, just before the Isabelle2014-RC1 snapshot.
Makarius
Email Gateway (Aug 19 2022 at 14:58):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Finally found some time to look at the jedit app launcher, first just downloading stable and latest versions of jedit.
The results weren’t encouraging:
- in neither, retina fonts worked
- in stable, I got the message that jedit is damaged and should be moved to the trash
- this could be fixed by relaxing security settings (so the problem was more a wrong error message)
- the latest version, I could not get to run at all, just got JRE load error (in non-retina fonts)
Summary: my appreciation of the work going into Isabelle releases has gone up another notch.
I might have a look at other macos/java launchers out there, but in light of the above, we’re already pretty good if we stick with what we have.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 14:58):From: Makarius <makarius@sketis.net>
After making a full round through major parts of the world wide web to
find out more about recent Java 7/8 app launchers, I am back to the
current one of Isabelle2014_RC0.
Lets try the following change to Isabelle2014-RC0.app/Contents/Info.plist:
<key>NSHighResolutionCapable</key>
<string>true</string>
That is for the outermost property list of that file. You can also use
the slightly odd GUI editor for that XML file, as provided by Apple.
Makarius
Email Gateway (Aug 19 2022 at 14:58):From: Joachim Breitner <breitner@kit.edu>
Hi,
very minor issue related to focus handling:
When I start jEdit and quickly open the menu (I usually first go to File
→ Recently used files), a moment later something happens that seems to
give focus to the main window, while the menu is still open. This means
that I cannot click on the open menu any more (and hover has no effect)
and I first have to close the menu and re-open it.
I can try to provide a screencast if required to reproduce.
Minor, but may indicate another problem somewhere.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:58):From: Lars Hupel <hupel@in.tum.de>
I can confirm that, using Linux (with KDE as desktop environment). It
doesn't happen with 2013-2.
Opening the menu right after jEdit opens also produces a stack trace:
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: Exception in
thread "AWT-EventQueue-0"
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:
java.lang.NullPointerException
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3414)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3405)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
org.gjt.sp.jedit.EditAction$Wrapper.actionPerformed(EditAction.java:212)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2018)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2341)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:402)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.AbstractButton.doClick(AbstractButton.java:376)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.AbstractButton.doClick(AbstractButton.java:356)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.plaf.basic.BasicPopupMenuUI$BasicMenuKeyListener.menuKeyPressed(BasicPopupMenuUI.java:358)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.JPopupMenu.fireMenuKeyPressed(JPopupMenu.java:1417)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.JPopupMenu.processMenuKeyEvent(JPopupMenu.java:1396)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.JPopupMenu.processKeyEvent(JPopupMenu.java:1380)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.MenuSelectionManager.processKeyEvent(MenuSelectionManager.java:455)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.plaf.basic.BasicPopupMenuUI$MenuKeyboardHelper.keyPressed(BasicPopupMenuUI.java:1200)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Component.processKeyEvent(Component.java:6474)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
javax.swing.JComponent.processKeyEvent(JComponent.java:2828)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Component.processEvent(Component.java:6293)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Container.processEvent(Container.java:2229)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Component.dispatchEventImpl(Component.java:4872)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Container.dispatchEventImpl(Container.java:2287)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Component.dispatchEvent(Component.java:4698)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1887)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:762)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1027)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:899)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:727)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Component.dispatchEventImpl(Component.java:4742)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Container.dispatchEventImpl(Container.java:2287)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Window.dispatchEventImpl(Window.java:2719)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.Component.dispatchEvent(Component.java:4698)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue.dispatchEventImpl(EventQueue.java:735)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue.access$200(EventQueue.java:103)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue$3.run(EventQueue.java:694)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue$3.run(EventQueue.java:692)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.security.AccessController.doPrivileged(Native Method)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:87)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue$4.run(EventQueue.java:708)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue$4.run(EventQueue.java:706)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.security.AccessController.doPrivileged(Native Method)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventQueue.dispatchEvent(EventQueue.java:705)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:242)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:161)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:150)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:146)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:138)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: at
java.awt.EventDispatchThread.run(EventDispatchThread.java:91)
Email Gateway (Aug 19 2022 at 14:58):From: Makarius <makarius@sketis.net>
Such focus problems are always annoying, and there are 3 main
possibilities / responsibilities for the cause: Java/Oracle, jEdit,
Isabelle/jEdit.
What precisely is your desktop environment (presumably on Linux)?
Makarius
Email Gateway (Aug 19 2022 at 14:59):From: Lars Hupel <hupel@in.tum.de>
It doesn't happen for me when I open a jEdit instance from the contrib
folder:
$ cd .isabelle/contrib/jedit_build-20140511/contrib/jedit-5.1.0-patched
$ java -jar jedit.jar
Email Gateway (Aug 19 2022 at 14:59):From: Joachim Breitner <breitner@kit.edu>
Hi,
ah, right: Linux with xmonad as the window manager.
(I guess the latter bit makes all problems not easily reproducible by
others my very own ones :-)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:59):From: Makarius <makarius@sketis.net>
Which version of Java is the "java" above?
Makarius
Email Gateway (Aug 19 2022 at 14:59):From: Lars Hupel <hupel@in.tum.de>
$ java -version
java version "1.7.0_60"
OpenJDK Runtime Environment (IcedTea 2.5.0) (Arch Linux build
7.u60_2.5.0-3-x86_64)
OpenJDK 64-Bit Server VM (build 24.60-b09, mixed mode)
Email Gateway (Aug 19 2022 at 14:59):From: Makarius <makarius@sketis.net>
Xmonad is known to be specifically Java-unfriendly, which is
understandable as a Haskell project. Not every version of xmonad is the
same, though, and there are concrete FAQ hints in
http://www.haskell.org/haskellwiki/Xmonad/Frequently_asked_questions#Problems_with_Java_applications.2C_Applet_java_console
Quoting the first part of the text:
There are two classes of problems: blank, grey windows and windows that
can't be focused for keyboard input. The latter should be fixed in the
newest xmonad, so follow the instructions on the website for getting a
copy of the darcs repository and build it.
Now it only depends on what they mean by "fixed" and "newest", and when
that FAQ entry was actually written.
Makarius
Email Gateway (Aug 19 2022 at 15:00):From: Joachim Breitner <breitner@kit.edu>
Hi,
I have had that particular problem many years ago (and that is how old
that entry is), and not any more since then. This does of course not
imply that there isn’t any fishiness left.
If others can’t reproduce it I’ll try again with a different window
manager.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:01):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Yup, that does it. I had to move the application bundle out of /Applications and back in, but after that it worked. It also correctly shows the non-low-resolution checkbox when you right-click and ask for info on the application.
Now the only step missing to MacOS bliss is passing in files to open.. ;-)
Cheers,
Gerwin
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 15:02):From: Makarius <makarius@sketis.net>
For that we would definitely have to give up the original Oracle
appbundler 1.0 that turned out so much better than anything else so far.
There might be a chance nonetheless, using the following fork of the
orignal project: https://bitbucket.org/infinitekind/appbundler
So far I did not manage to build it in a way that it actually works on our
official platforms: Lion, Mountain Lion, Mavericks.
If anyone else wants to try it and can provide some explanations how to do
it, including the all-important Info.plist, I will consider it for the
coming release candidates. There are about 1-2 weeks left for such
tinkering.
Makarius
Email Gateway (Aug 19 2022 at 15:04):From: Makarius <makarius@sketis.net>
VSL 2014 has ended today, and the special test version Isabelle2014-RC0 is
about to converge towards the first official release candidate
Isabelle2014-RC1 very soon.
As far as I can foresee now, it will be ready for general testing on
Sunday or Monday -- I am myself very busy in the week afterwards.
Stay tuned ...
Makarius
Email Gateway (Aug 19 2022 at 15:05):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the coming Isabelle2014 release is anticipated for August 2014. As an
early semi-official release candidate for general testing there is now
Isabelle2014-RC0 available from here:
http://isabelle.in.tum.de/website-Isabelle2014-RC0
This is an opportunity to look how things will presumably be in the
release, and to report problems, either on the isabelle-users mailing list
or via private mail.
The very same version will be used at the Isabelle tutorial at VSL 2014 in
Vienna next week: http://vsl2014.at/isabelle
The Vienna Summer of Logic is the largest convention of Logicians of known
human history (i.e. the last 15000 years) on this planet. Many of the
protagonists of this mailing list will be there. I am myself attending
the ITP week with two adjacent workshop days: 13..18-Jul-2014.
If there are any particular problems with the increasingly interactive
Isabelle computer-game, which is the Prover IDE, I would be happy to sort
this out personally. (Including the canonical question about remaining
uses of Proof General.)
After the conference -- more than 2 weeks from now -- there will be the
normal Isabelle2014-RC1, with more formal testing, reporting, polishing,
until final lift-off in August, when most Frenchmen are on vacation.
Makarius
Email Gateway (Aug 19 2022 at 15:07):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
At first sight, just a very tiny issue on Ubuntu 12.04: when running the
new Isabelle for the first time, before it started to build the heaps
images, I did not have a window immediately and instead a small white
empty square (about 100 px x 100 px), which for a few seconds, makes me
feel something crashed, then only later the window appeared.
Something funny: looks like jEdit changed a lot while it seems to be the
same version as with the prior Isabelle release (some plugins?). May be
the answer is in the NEWS log though, which I have not read yet.
Also, and sorry for the small talk, just wanted to say you did an even
bigger job than usual for this release.
Have an happy day!
Email Gateway (Aug 19 2022 at 15:08):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
So datatype_new will always be named the same? I though it will be
renamed to just datatype and replace the old one.
Email Gateway (Aug 19 2022 at 15:09):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hopefully not always. ;) For the 2014 release, our goal was to have "datatype_new" inside "Main" [*]. We've succeeded with that. For the following release (presumably 2015), I hope we can rename "datatype_new" to "datatype" and move the old command to "src/HOL/Library", but this is a delicate operation, and it may be that it takes more than one release cycle before we get there.
On the positive side, "list" and "option" are already defined using the new command, and the large IsaFoR library has been successfully ported. There's also more and more infrastructure that can deal with "datatype_new", including "fun", Lifting & Transfer, Nitpick -- and the "datatype_compat" command, which registers new-style datatypes as old-style ones, now works better than ever.
Jasmin
[*] This was, in fact, a goal for Isabelle2013-1 (cf. my 30 July 2013 email to the mailing list), but we ran out of time (moving "datatype_new" to "Main" required reducing its dependencies significantly, among other things), and the whole plan presented in that email got postponed by one release.
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
On Sun, 6 Jul 2014, Yannick Duchêne (Hibou57) wrote:
At first sight, just a very tiny issue on Ubuntu 12.04: when running the
new Isabelle for the first time, before it started to build the heaps
images, I did not have a window immediately and instead a small white
empty square (about 100 px x 100 px), which for a few seconds, makes me
feel something crashed, then only later the window appeared.
That should be a splash screen with the Isabelle logo, shown by the JVM on
startup. I will try to find out what happens here, but it might be one of
the many problems that Oracle has with the multitude of Linuxes.
Something funny: looks like jEdit changed a lot while it seems to be the
same version as with the prior Isabelle release (some plugins?).
jEdit did not change at all. What changed a lot is the Isabelle/PIDE
infrastructure and the modules that make Isabelle/jEdit.
May be the answer is in the NEWS log though, which I have not read yet.
You should read that, e.g. in Isabelle/jEdit via the Documentation panel.
There is also a SideKick tree view for that file.
Moreover the Isabelle/jEdit manual has changed a lot, now approaching 50
pages, with updated screenshots, new material etc.
Also, and sorry for the small talk, just wanted to say you did an even
bigger job than usual for this release.
We are not there yet. Many fine points need to be discovered, reported,
sorted out.
Makarius
Email Gateway (Aug 19 2022 at 15:11):From: Yannick <yannick_duchene@yahoo.fr>
The splash screen appeared the second time I launched this release. The
issue occurred only the first time, when it have to build the heap images.
This may be a short time bad user experience, but not a big issue.
Email Gateway (Aug 19 2022 at 15:12):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Two small things that might be worth looking at:
on my laptop, Isabelle 2014-RC0/jedit comes up with non-retina fonts, whereas 2013-2 does (different java version I guess)
on the Mac, by default the Isabelle app is not associated with .thy files (which is fine). If you do associate it manually, and either “open file.thy” on the command line, or double click a .thy file in Finder, Isabelle/jedit comes up, but loads Scratch.thy. This was already the case in 2013-2, I just forgot about it again. There is probably just some command line argument that needs to be passed to isabelle jedit in the Mac application magic.
Cheers,
Gerwin
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 15:13):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Further to that, current isabelle development at b8448367f9c7 with jdk-7u60 does come up fine with retina fonts.
Cheers,
Gerwin
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 15:13):From: Makarius <makarius@sketis.net>
That is exactly the same version. I guess that you have run
Isabelle2014-RC0 via the .app launcher, but the repository version via the
command-line "isabelle jedit". That makes a difference, but I don't
understand all what Oracle is doing here: both launchers are "official" in
some sense.
Can you try the launcher of jedit 5.2pre1 from http://www.jedit.org/ which
is the one of Java 7 JFX, instead of the old Java one?
The Prover IDE is a "filty rich client", but I am myself not filthy rich
to have access to a retina display for testing.
Makarius
Email Gateway (Aug 19 2022 at 15:13):From: Makarius <makarius@sketis.net>
Lack of file associations is a known and documented property of the 1.0
app launcher by Oracke that was used here. In that respect it should be
exactly the same behaviour as in Isabelle2013-2, which seems to be the
case.
Makarius
Email Gateway (Aug 19 2022 at 15:13):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 7 Jul 2014, at 1:36 pm, Makarius <makarius@sketis.net> wrote:
On Mon, 7 Jul 2014, Gerwin Klein wrote:
>
On 7 Jul 2014, at 12:59 pm, Gerwin Klein <Gerwin.Klein@nicta.com.au> wrote:
- on my laptop, Isabelle 2014-RC0/jedit comes up with non-retina fonts, whereas 2013-2 does (different java version I guess)
Further to that, current isabelle development at b8448367f9c7 with jdk-7u60 does come up fine with retina fonts.
That is exactly the same version. I guess that you have run Isabelle2014-RC0 via the .app launcher, but the repository version via the command-line "isabelle jedit”.
Correct. I just tried the command line for 2014-RC0 and that does come up fine with retina fonts, so it indeed seems to be something about the launcher.
Can you try the launcher of jedit 5.2pre1 from http://www.jedit.org/ which is the one of Java 7 JFX, instead of the old Java one?
Ok, happy to have a look. This might take a bit, I don’t have a good internet connection at the moment.
Cheers,
Gerwin
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 15:13):From: "C. Diekmann" <diekmann@in.tum.de>
I found some problems.
The following can be solved by isabelle 2013-2 but not by Isabelle 2014-RC0:
lemma "finite X ⟹ finite {(x1, x2) ∈ X. P x1 x2}" by simp
In Isabelle 2014-RC0, also try0 and sledgehammer fail.
I suppose it is because of the tuple notation?
When a proof fails, the output buffer displays: "... method⌂: ...".
Notice the triangle-like symbol. The same strange symbol is displayed
for an ML error.
Finally, when I try to sledgehammer something in one of my thys, the
prover crashes.
"Welcome to Isabelle/HOL (Isabelle2014-RC0: July 2014)
Malformed message:
bad chunk (unexpected EOF after 0 of 7314 bytes)
message_output terminated
/home/diekmann/Downloads/Isabelle2014-RC0/lib/scripts/run-polyml-5.5.2:
line 84: 15324 Segmentation fault (core dumped) "$POLY" -q -i
$ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl"
"$MLTEXT")" --error-exit < /dev/null
standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 139"
I will try to reproduce this in a minimal example
Cheers
Cornelius
Email Gateway (Aug 19 2022 at 15:13):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Indeed the tuple notation appears to be the issue here, with (simp add:
split_def) solving the lemma. Unfolding split_def breaks up the tuple
notation to use fst and snd.
It's not clear to me how this was being solved before and what might
have changed.
Hope that helps a little,
Thomas.
Email Gateway (Aug 19 2022 at 15:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Cornelius,
In Isabelle2013-2, the simproc finite_Collect has taken care of the tuples and solved your
goal. In Isabelle2014-RC0, this simproc has been disabled by default because it sometimes
complicates proofs or crashes. You can enable the simproc by declaring
[[simproc add: finite_Collect]]
either globally with "declare" or locally with "using".
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:15):From: Joachim Breitner <breitner@kit.edu>
Hi,
thanks for the RC!
I tried to collect my minor observations, but it turns out that all of
them have been reported before. Anyways, here are those collected today:
I just observed an error message in the output window:
Undefined constant: "list.size"⌂
And I wonder what the ⌂ is about.
The spellchecker doesn’t know about a few probably Isabelle specific
words such as “instantiation”. Maybe these should be added?
Messages like „Metis: Unused theorems:“ appear below the goal state
in the output panel, which is less convenient than the previous
order.
It is irritating that auto-completion does not work when there is a
letter following the cursor. But maybe I just need to get used to
that.
No select-to-clipboard in the output window under Linux.
And another thing worth noting, although already present in the 2013
release: When jumping to a file that is loaded as part of the loaded
heap (e.g. Set), there is an error at the theory command: “Cannot update
finished theory "Set"”. That makes sense to me, but I don’t plan to
update the theory, I just want to navigate it. Currently, this prevents
me from using Ctrl-Click on definitions in that file to navigate
further.
Greetings and thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:15):From: Alfio Martini <alfio.martini@acm.org>
(No email body)
Email Gateway (Aug 19 2022 at 15:15):From: Joachim Breitner <breitner@kit.edu>
Hi,
note that for me, this has always been the case. Maybe there is another
variable influencing this.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
This is a total failure of existance of the ML runtime system, which is
polyml-5.5.2 in Isabelle2014-R0.
In order to make some educated guesses what could be wrong, we need
precise information about the hardware (CPU model and memory size), apart
from the OS (which was Ubuntu 14.04 LTS here). Did you use x86 or x86_64
for Poly/ML? This depends on pre-installed C/C++ libraries.
If you know how to tinker with Isabelle components, you can also try with
polyml-5.5.1-1 from the Isabelle component repository, e.g. claiming it
via init_component in $ISABELLE_HOME_USER/etc/settings and using "isabelle
components -a" as described in the "system" manual.
Makarius
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
The strange symbol represents the position, i.e. you can hover-click to it
is for other formal divices in PIDE input/output.
Its Isabelle name is \<here> and its unicode rendering a "house" (or
"home") glyph.
Makarius
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
General PIDE principle: use C-hover to ask about what you see. Here it
will give you a visual clue that it is a hyperlink -- the one stemming
from a symbolic position.
IIRC, there is no explicit documentation of this new \<here> (or "house" /
"home") symbol, but the general principles are now quite explicit in the
Isabelle/jEdit manual.
Makarius
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
See also the Isabelle/jEdit manual. Users can choose their own
dictionaries, and include or exclude entries. There is also a nice context
menu for that.
What is missing in this release: proper support for non-English languages.
E.g. German with its treatment of capitalization will not quite work, even
if you give it a German word list via the documented settings and options.
French might work, but I did not try it.
Makarius
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
Did this change wrt. the last release?
Makarius
Email Gateway (Aug 19 2022 at 15:17):From: Makarius <makarius@sketis.net>
Can you say more explicitly what you mean? The output has its own very
simple selection and copy mechanism, unlike the main text area. But this
should not have changed wrt. the last release, IIRC.
Makarius
Email Gateway (Aug 19 2022 at 15:17):From: Makarius <makarius@sketis.net>
This is a very old omission in the PIDE document model: the relation to
persistent heap images is not really addressed. I think this is becoming
more anoying now, since so many other things work smoothly.
One reason why a substantial reforms in this department are difficult are
are the 4 different "modes" of Isabelle: Isar TTY, Proof General, batch
build, PIDE interaction.
The first two are obsolete, but still around to hinder progress. The
second two might need more reconsiderations, if there are chances to unify
them into just one.
Makarius
Email Gateway (Aug 19 2022 at 15:17):From: Makarius <makarius@sketis.net>
It has been like that all the time. It is now more explicitly documented
in the Isabelle/jEdit manual at least.
Makarius
Email Gateway (Aug 19 2022 at 15:17):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Joachim,
Could you give us more context about this error, e.g. a self-contained theory file that we can load to reproduce it (or at least a screenshot)? There have been some changes in the "size" function generation for lists between 2013-2 and 2014-RC0, but we were expecting the changes to be backward-compatible.
Thank you!
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 15:18):From: Joachim Breitner <breitner@kit.edu>
Dear Makarius,
sorry for not being clear. I wasn’t asking how to extend the dictionary
locally. My suggestion was to extend the dictionary, as shipped, with
uncommon, Isabelle-related words. Of course, a very minor suggestion.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:18):From: Joachim Breitner <breitner@kit.edu>
Dear Makarius,
yes: With 2013 I can put the cursor between a and b in abc and enter
\alp to get aαbc.With 2014, I get a\alpbc.
Greetings,
Joachi
signature.asc
Email Gateway (Aug 19 2022 at 15:18):From: Joachim Breitner <breitner@kit.edu>
Dear Makarius,
correct, no regression here. I mean that on Linux, when I select some
text, I expect that the middle mouse button pastes it; this does not
work in the output buffer.
The main text are support supports this interaction.
(It has been discussed on one of these two mailing lists before, so
nothing new here.)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:18):From: Joachim Breitner <breitner@kit.edu>
Dear Jasmin,
I found that I had to change my theories to refer to size_list instead
of list_size (but no substantial changes were required)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:18):From: Makarius <makarius@sketis.net>
There is a long story behind this. The author of the jortho module made
the largest possible dictionary on the planet, but that is useless for
spell-checking. He is very bad at spelling anyway, as can be seen in the
original Java sources.
So I spent a few days studying the situation a bit, to come up with an
imitation of aspell dictionaries according to SCOWL 7.1
http://wordlist.sourceforge.net with certain formal parameters that are
specified in $JORTHO_HOME/README. SCOWL is a very perfectionistic word
list project, and I don't want to deviate from it in informal ways.
If the parameters are somehow sub-optimal, or not really the aspell ones,
that can be revisited, of course.
Makarius
Email Gateway (Aug 19 2022 at 15:19):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Joachim,
Fair enough; this is documented in "NEWS" as follows:
* The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>
"case_prod").
INCOMPATIBILITY.
This is merely a cosmetic change. There were also more fundamental changes taking place under the hood.
(Incidentally, I don't quite understand how this connects to the unknown "list.size" constant error you reported, though. Please let us know If this is still an issue.)
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 15:19):From: Joachim Breitner <breitner@kit.edu>
Hi,
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC