Email Gateway (Aug 19 2022 at 09:36): Email Gateway (Aug 19 2022 at 09:36):From: Makarius <makarius@sketis.net>
On Sun, 20 Jan 2013, Alfio Martini wrote:
I had no problem in installing and using the leaked version from January
the 11th.
IIRC, that version was bypassing the Cygwin init script accidentally.
But I could not successfully install this RC. After the unpacking of
files, it opens the command prompt windows and stays forever
"initializing Cygwin".
See Isabelle2013-RC1\contrib\cygwin\isabelle\init.bat what is happening
here. You should be able to see where it hangs by editing the two shell
invocations in that file like this:
...
"bin\dash" -x /isabelle/rebaseall
"bin\bash" -x /isabelle/postinstall
The -x option produces a trace. If you show me the result we can continue
guessing.
You can try again by opening a Windows command interpreter (cmd.com) and
execute the batch file Isabelle2013-RC1\contrib\cygwin\isabelle\init.bat
Makarius
Email Gateway (Aug 19 2022 at 09:37):From: Serguei Mokhov <serguei@gmail.com>
Makarius,
On Sun, Jan 20, 2013 at 2:38 PM, Makarius <makarius@sketis.net> wrote:
Dear all,
the Isabelle2013 release is anticipated for February 2013. Before actual
lift-off we have approx. 3 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 main Isabelle2013-RC1 download page is
http://isabelle.in.tum.de/website-Isabelle2013-RC1 -- although some parts of
the text of the webpage is still missing.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. The time to sort out
issues is now.
On my MacOS X, I am getting on start up when it crashes:
------8<------
dyld: unknown required load command 0x80000022
/Applications/Isabelle2013-RC1.app/Contents/Resources/Isabelle2013-RC1/lib/Tools/java:
line 1: 2095 Trace/BPT trap "$ISABELLE_JDK_HOME/bin/$PRG"
"$@"
Return code: 133
------8<------
Admittedly, I am still running 10.5.x on this particular laptop, which
is technically no longer supported by Apple, but I saw no mention in
the docs that officially Isabelle community no longer supports it. If
this is the case please mention it somewhere. I still happened to have
2011-1 and 2012-RC2 on it, and both work. All use jEdit.
Makarius
Email Gateway (Aug 19 2022 at 09:37):From: Makarius <makarius@sketis.net>
It is mentioned on
http://isabelle.in.tum.de/website-Isabelle2013-RC1/installation.html where
it says "(10.8, 10.7, partly 10.6)". There is little chance left for 10.5
(Leopard) and 10.6 (Snow Leopard) is working only to the extent that I can
myself use it every in the office, but there can be surprises with the JDK
1.7.x that is used for Isabelle2013.
I recommend to invest the nominal fee for Mountain Lion to upgrade. (There
are websites and private blogs explaining how to do that for very old
systems, despite what Apple says officially.)
Makarius
Email Gateway (Aug 19 2022 at 09:37):From: Serguei Mokhov <serguei@gmail.com>
On Mon, Jan 21, 2013 at 2:34 PM, Makarius <makarius@sketis.net> wrote:
On Mon, 21 Jan 2013, Serguei Mokhov wrote:
On my MacOS X, I am getting on start up when it crashes:
------8<------
dyld: unknown required load command 0x80000022/Applications/Isabelle2013-RC1.app/Contents/Resources/Isabelle2013-RC1/lib/Tools/java:
line 1: 2095 Trace/BPT trap "$ISABELLE_JDK_HOME/bin/$PRG"
"$@"Return code: 133
------8<------Admittedly, I am still running 10.5.x on this particular laptop, which
is technically no longer supported by Apple, but I saw no mention in
the docs that officially Isabelle community no longer supports it.It is mentioned on
http://isabelle.in.tum.de/website-Isabelle2013-RC1/installation.html where
it says "(10.8, 10.7, partly 10.6)".
Doh... I am sure I searched prior posting; obviously not very rigorously. :/
There is little chance left for 10.5
(Leopard) and 10.6 (Snow Leopard) is working only to the extent that I can
myself use it every in the office, but there can be surprises with the JDK
1.7.x that is used for Isabelle2013.
Thanks for confirming that.
I recommend to invest the nominal fee for Mountain Lion to upgrade. (There
are websites and private blogs explaining how to do that for very old
systems, despite what Apple says officially.)
Right; I just seem to never being able to get around to do that yet
with all the backups and re-configurations to be done... but I agree
with you totally as there are no security patches among other things.
-s
Email Gateway (Aug 19 2022 at 09:38):From: Slawomir Kolodynski <skokodyn@yahoo.com>
The hints in jedit are less convenient in Isabelle2013, I don't know if this is intentional. For example, if I type \<ta I get the only hint for the greek letter \<tau>.
It used to be that if I pressed enter at this point it was interpreted as selection and the text \<ta was replaced by the full text \<tau>in the source. Now jedit just puts the cursor in the new line. To select \<tau> I have to point and click the mouse.
Similarly, if I type \<in I get a couple of possibilities. If I point the cursor (with arrows on the keyboard) to the symbol \<in> and press enter, again this just puts me in the new line instead of selecting \<in>. I would prefer not to have to switch between keyboard and mouse every time I want to select a symbol from the hints. Can it be configured in options somehow?
I am on (L)Ubuntu 12.10.
Thanks,
Slawekk
Email Gateway (Aug 19 2022 at 09:38):From: Alfio Martini <alfio.martini@acm.org>
Hi Slawomir,
This might help you (from the News List in Isabelle 2013-RC1)
Email Gateway (Aug 19 2022 at 09:39):From: Lars Noschinski <noschinl@in.tum.de>
As far as I know, the completion key was changed from \n (Enter) to \t
(Tab).
-- Lars
Email Gateway (Aug 19 2022 at 09:39):From: Christian Sternagel <c.sternagel@gmail.com>
And of course, you can change it back to your desired behavior. As follows:
1) Utilities -> Options (or C-F12)
2) Tab: Plugin Options
3) Sidekick -> General
4) "Accept characters for completion popup"
this is currently set to "\t" and you can just change it to "\t\n" (or
maybe "\n")
cheers
chris
Email Gateway (Aug 19 2022 at 09:41):From: Makarius <makarius@sketis.net>
I recommend to practice a little with \t first. In the past it just did
not work for technical reasons of Java/Swing. So \n had to be used as a
workaround, but it gets more often in the way of normal editing. E.g.
when you type "fix x :: nat" or "foo:" and then press RETURN.
Moreover the popup passes almost all key strokes back to the main editor
window, so it should get in the way much less than before.
Since the timing is also much more aggressive by default, it could break
down, loosing focus or whatever. So frequent users should keep an eye on
it, to see if it behaves badly. Often the problem is one of the
underlying platform or the platform look-and-feel of Java/Swing. Gtk on
Linux is particularly bad, because it has many themes on its own that may
change the behaviour as well.
I was trying many of these things already 1-2 years ago, but it was
causing so much trouble that it did not make it as default in the two
earlier official releases of Isabelle/jEdit.
Makarius
Email Gateway (Aug 19 2022 at 10:00):From: Makarius <makarius@sketis.net>
Dear all,
the Isabelle2013 release is anticipated for February 2013. Before actual
lift-off we have approx. 3 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 main Isabelle2013-RC1 download page is
http://isabelle.in.tum.de/website-Isabelle2013-RC1 -- although some parts
of the text of the webpage is still missing.
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. The time to
sort out issues is now.
Makarius
Email Gateway (Aug 19 2022 at 10:00):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,
I had no problem in installing and using the leaked version from January
the11th. But I could
not successfully install this RC. After the unpacking of files, it opens
the
command prompt windows and stays forever "initializing Cygwin". See image
attached.
I repeated this installation three times.
Even though, I continue the installation process executing Isabelle, after
killing the
command prompt window. The build process
(now presented in more detail) was successful.
Anyway, Avast AutoSandbox complain systematically about the following
processes:
C:\Isabelle2013-RC1\Isabelle2013.exe
C:\Isabelle2013-RC1\contrib\polyml-5.5.0\x86-cygwin\poly.exe
However, it gives permission to continue execution after 15 seconds or so
for
each file.
Then I went to a final test: configuring a session for document
preparation. After executing the
cygwin terminal I got a message that somethings did not go well (group
identification),
telling that some files should be rebuilt. See attached image. Probably
this is related to that faulty
initialization mentioned above
I stop here and wait from some feedback of you.
Best!
installation-stuck.PNG
cygwin-group-problem.PNG
Last updated: Apr 30 2024 at 16:19 UTC