Email Gateway (Aug 19 2022 at 10:55): Email Gateway (Aug 19 2022 at 10:55):From: Andrius Velykis <andrius.velykis@newcastle.ac.uk>
Dear Isabelle users,
I am pleased to announce the first _official_ release of Isabelle/Eclipse!
Isabelle/Eclipse provides an Eclipse integration for Isabelle, based on
Isabelle/Scala. It started as a port of Isabelle/jEdit to integrate with
Eclipse IDE. Today Isabelle/Eclipse is available as a standalone prover
IDE, as well as plug-ins for integration with Eclipse IDE of your choice.
Learn more about Isabelle/Eclipse and download it from its website:
http://andriusvelykis.github.io/isabelle-eclipse/
In many ways Isabelle/Eclipse mirrors Isabelle/jEdit, but aims to provide
Eclipse-native functionality to use Isabelle. The integration uses common
Eclipse components to provide theory editing, correct symbols, completion
assistance, prover output and other features. By building on Eclipse it
inherits various IDE goodies out of the box. Learn more about
Isabelle/Eclipse features on the website. Check out the list of closed
issues to see what has been implemented and fixed in this release:
http://github.com/andriusvelykis/isabelle-eclipse/issues?state=closed
Before you start Isabelle/Eclipse, I advise reading the "Getting started"
page on the website. Also make sure you are using Java 7 and Isabelle 2013.
Note that Isabelle/Eclipse still has several known issues, notably no
support for sub/super-script, bold and other control symbols, as well as
lack of nice UI to configure certain Isabelle options. You can view all
open issues for Isabelle/Eclipse here:
http://github.com/andriusvelykis/isabelle-eclipse/issues?state=open
Please report any bugs, feature requests, questions and other issues you
encounter using the link above - I will appreciate your input!
Isabelle/Eclipse is open-source and the source code is available on GitHub:
http://github.com/andriusvelykis/isabelle-eclipse
I welcome all contributions and help - if you see an open issue that you
want to hack at, feel free to!
Isabelle/Eclipse started as an attempt to get Isabelle working from within
Eclipse IDE. There are a number of formal methods tools building on the
Eclipse platform and I hope that Isabelle/Eclipse will be useful to
integrate them with the Isabelle theorem prover.
Great thanks to Makarius for his assistance, input and all the work on
Isabelle and Isabelle/Scala.
Let me know what you think!
Best regards,
Andrius Velykis
Newcastle University / AI4FM project
http://andrius.velykis.lt
Email Gateway (Aug 19 2022 at 10:55):From: Alfio Martini <alfio.martini@acm.org>
Hi Andrius,
Thank you very much for your work. I have installed used the update manager
and it works well (see
isa-eclipse-session image).
I am working in windows 8 laptop with 6GB of ram memory. My only complain
is that it took
too (ooo) long to process the thy file (if compared to jedit/isabelle or
isabelle/proofgeneral).
I have used ecplise update manager as explained in the help file. But one
thing caught my attention.
If you click in the link for the windows 64-bit version you will see that
actually it points to the
32 bit version (see second image). So I wonder if that could be the problem
for the very slow file processing.
Thanks for any help
isa-eclipse-session.PNG
eclipse-64-download..PNG
Email Gateway (Aug 19 2022 at 10:55):From: Andrius Velykis <andrius.velykis@newcastle.ac.uk>
Hi Alfio,
Thanks for trying it out. Glad to see you got everything running without
problems!
On Wed, Apr 17, 2013 at 1:06 PM, Alfio Martini <alfio.martini@acm.org>wrote:
I am working in windows 8 laptop with 6GB of ram memory. My only
complain is that it took
too (ooo) long to process the thy file (if compared to jedit/isabelle or
isabelle/proofgeneral).
I have not done any side-by-side performance testing yet with
Isabelle/jEdit, so it may be true. If you feel it is much slower, can you
file this as a bug at
http://github.com/andriusvelykis/isabelle-eclipse/issues ?
I have used ecplise update manager as explained in the help file. But one
thing caught my attention.
If you click in the link for the windows 64-bit version you will see that
actually it points to the
32 bit version (see second image). So I wonder if that could be the
problem for the very slow file processing.
The win32 bit in the file name is just standard Eclipse's way of
packaging to indicate that Win-API is used for UI widgets. The 32/64 bit
difference is at the end of the file name, see:
isabelle-eclipse-ide-1.2.0-win32.win32.x86_64.zip. The x86_64 part
indicates that this is indeed a 64-bit package.
I'll have to see what can be the causes of performance issues you are
experiencing.
Thanks for any help
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
Thanks for the comments!
Andrius
Email Gateway (Aug 19 2022 at 10:56):From: René Neumann <rene.neumann@in.tum.de>
Thanks for your work! Having a sane SWT-Interface alone is worth using
it (at least compared to using Swing...).
I have a couple of suggestions -- as I have never really used jEdit
(still don't like its way of user-interaction [1]), some of these might
be impossible to implement because of the underlying PIDE framework.
1.) Print some error-message if Java7 could not be found, instead of
failing silently. It took quite a while to figure this out, when the
Isabelle-View seemed to not exist.
2.) Add a view to show the 'informational' messages like "thm
list.induct". It is shown for a short moment in "prover output" but then
gone when the prover decides to proof something different. Perhaps a
view "line_number : message". This would even allow to show "term foo;
term bar" at the same time, something I really miss in PG.
2a.) As an alternative (or addition): Add a default shortcut to show the
info/error in the current line (this is the 'Show Ruler Annotation
Tooltip', as I just learned).
3.) 'export_code term in SML file -' does not produce any
output/popup/... Please add this.
4.) Sessions: If I add an external directory, how is determined, whether
there is a session?
4a.) Allow to use the logics in ~/.isabelle/Isabelle-yyyy/heaps, so that
I can use them directly without 'session dirs'.
5.) Is it somehow possible to state the logic to use via the cmdline on
startup?
So, thanks again. This really looks promising.
[1] And the look'n'feel of jEdit (the editor itself) is really bad imho
-- but this is a non-technical point.
smime.p7s
Email Gateway (Aug 19 2022 at 10:56):From: Andrius Velykis <andrius.velykis@newcastle.ac.uk>
Dear René,
Thanks for the comments and reports!
On Wed, Apr 17, 2013 at 5:12 PM, René Neumann <rene.neumann@in.tum.de>wrote:
1.) Print some error-message if Java7 could not be found, instead of
failing silently. It took quite a while to figure this out, when the
Isabelle-View seemed to not exist.
The silent non-load is being done by Eclipse if plug-in's execution
environment is not satisfied. A possible workaround would be to include a
plug-in with lower requirements that pops up a dialog message if Java 7 is
not available.
Tracking the issue in
http://github.com/andriusvelykis/isabelle-eclipse/issues/69
2.) Add a view to show the 'informational' messages like "thm
list.induct". It is shown for a short moment in "prover output" but then
gone when the prover decides to proof something different. Perhaps a
view "line_number : message". This would even allow to show "term foo;
term bar" at the same time, something I really miss in PG.
Do you mean like a duplicate Prover Output view that is "sticky" on some
prover command? Could you file this as an issue and elaborate more in
http://github.com/andriusvelykis/isabelle-eclipse/issues (you can use the
tracker to record feature requests as well as bugs!)? I am not too familiar
with PG (never got used to Emacs..) so would appreciate more details :)
2a.) As an alternative (or addition): Add a default shortcut to show the
info/error in the current line (this is the 'Show Ruler Annotation
Tooltip', as I just learned).
Will look into it:
http://github.com/andriusvelykis/isabelle-eclipse/issues/70
3.) 'export_code term in SML file -' does not produce any
output/popup/... Please add this.
Could file an issue and elaborate further? Thanks!
4.) Sessions: If I add an external directory, how is determined, whether
there is a session?
The session dir must have an appropriate ROOT or ROOTs file at the top (see
Chapter 3 in Isabelle System Manual).
4a.) Allow to use the logics in ~/.isabelle/Isabelle-yyyy/heaps, so that
I can use them directly without 'session dirs'.
You can build sessions into your home directory by selecting "Build
sessions to user home directory" in Build tab of Isabelle launch
configuration. Or do you mean that the dialog should look for additional
heaps already pre-built there and list them in the session selection? I am
not sure how much Isabelle.Build tool covers this (Isabelle/Eclipse just
provides a UI for it).
5.) Is it somehow possible to state the logic to use via the cmdline on
startup?
No, not at the moment. It is not possible to auto-start Isabelle, you have
to start it manually via the configured launch dialog. In Isabelle/Eclipse
I am still investigating the best way of interacting with Isabelle
distribution, since it is not bundled with a specific Isabelle like
Isabelle/jEdit (see
http://github.com/andriusvelykis/isabelle-eclipse/issues/71).
What is your use case to indicate the logic via cmdline?
So, thanks again. This really looks promising.
- René
Thanks for the input and good words! I would really suggest also filing all
such feature requests (as well as bugs or just discussions) in the GitHub
issue tracker. Things get lost in e-mails.. :)
Thanks,
Andrius
Email Gateway (Aug 19 2022 at 10:56):From: René Neumann <rene.neumann@in.tum.de>
Am 17.04.2013 19:28, schrieb Andrius Velykis:
2.) Add a view to show the 'informational' messages like "thm
list.induct". It is shown for a short moment in "prover output" but
then
gone when the prover decides to proof something different. Perhaps a
view "line_number : message". This would even allow to show "term
foo;
term bar" at the same time, something I really miss in PG.
Do you mean like a duplicate Prover Output view that is "sticky" on
some
prover command?
Yes. Perhaps exactly those commands, that already produce the
(i)-bubble to the left of the text.
Could you file this as an issue and elaborate more in
http://github.com/andriusvelykis/isabelle-eclipse/issues (you can use
the
tracker to record feature requests as well as bugs!)? I am not too
familiar
with PG (never got used to Emacs..) so would appreciate more details
:)
http://github.com/andriusvelykis/isabelle-eclipse/issues/72
3.) 'export_code term in SML file -' does not produce any
output/popup/... Please add this.
Could file an issue and elaborate further? Thanks!
4.) Sessions: If I add an external directory, how is determined,
whether
there is a session?
The session dir must have an appropriate ROOT or ROOTs file at the top
(see
Chapter 3 in Isabelle System Manual).
Ah, will look into it. Never had to use this -- having a ROOT.ML and a
./build.sh did the thing for me until now.
4a.) Allow to use the logics in ~/.isabelle/Isabelle-yyyy/heaps, so
that
I can use them directly without 'session dirs'.
You can build sessions into your home directory by selecting "Build
sessions to user home directory" in Build tab of Isabelle launch
configuration. Or do you mean that the dialog should look for
additional
heaps already pre-built there and list them in the session selection?
The latter. Because then, my current setup (ROOT.ML + build.sh) would
still work, and I wouldn't need any session directories.
I am
not sure how much Isabelle.Build tool covers this (Isabelle/Eclipse
just
provides a UI for it).
Well ... there still is isabelle findlogics. But I don't know, how
this is implemented.
5.) Is it somehow possible to state the logic to use via the cmdline
on
startup?
No, not at the moment. It is not possible to auto-start Isabelle, you
have
to start it manually via the configured launch dialog. In
Isabelle/Eclipse
I am still investigating the best way of interacting with Isabelle
distribution, since it is not bundled with a specific Isabelle like
Isabelle/jEdit (see
http://github.com/andriusvelykis/isabelle-eclipse/issues/71).What is your use case to indicate the logic via cmdline?
With some project-oriented environment like Eclipse, there probably is
none. For PG I used to have ".isabelle-logic" files all over the place,
which specify the logic image to use, and then a wrapper around
'isabelle {emacs,jedit}' that interprets them (cf.
http://git.necoro.eu/dotfiles.git/tree/.zsh/functions/IE ). So the
question was more or less inspired by current habits :).
Email Gateway (Aug 19 2022 at 10:56):From: Makarius <makarius@sketis.net>
This sounds all very ancient, even before the IsaMakefile/usedir setup
that was used between 1997 and 2012. Isabelle2013 still has some remains
of the old stuff, but there is no point to go back to it. (Files that
happen to lie around in some directory are not a proper session.)
Andrius was rather quick to pick up the isabelle.Build Scala module, which
is standard session management component of Isabelle2013. Quite
impressive work what he did in Isabelle/Eclipse.
I feel motivated to trash the old IsaMakefile/usedir scripting stuff
rather soon. Then users merely have to spend 15min reading the Isabelle
system manual, and then save a lot of everyday build time.
Makarius
Email Gateway (Aug 19 2022 at 10:57):From: René Neumann <rene.neumann@in.tum.de>
If it's afterwards still possible to pass an image to PG, I won't
object. Also it would be nice to still have a "isabelle findlogics"
equivalent to allow passing sessions/images by script. Whether this is
implemented by looking into a directory or by using XML-RPC in
combination with the "iSabelle Session Server (iSS) in the Cloud(tm)" is
not my concern.
Last updated: Apr 26 2024 at 20:16 UTC