Email Gateway (Aug 18 2022 at 14:49): Email Gateway (Aug 18 2022 at 14:49):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Is the Windows version ready? I tried to run it on windows, but I was
not able to
configure the Isabelle installation.
Viorel
Email Gateway (Aug 18 2022 at 14:50):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,
I've installed i3p and I've been using it for a few days, so it may be that
my appreciations are not that accurate, but just a few comments:
First I would like to emphasize the ease of use of the tool. It
took me no time to install it and in a couple of minutes I was already
writting code (from any point of view much easier than learning emacs
or xemacs for a newbie), and I could install the Isabelle fonts just
following the instructions.
I think it is quite fast starting and loading theories and images.
There are also a few things that i did not get to work and I missed from xemacs:
I do not know how to switch between the different windows from the
application. For instance, when I'm writting down a theory I would
like to move from the file to the "Result window" to copy the goals or
some of the premises and take them back to the "thy" file. I did not
manage to do it. This feature would ease faster development.
X-symbols are not displayed in my files (but they are in the
"Result prover" window). Whenever I write "\<And>" or any other symbol
i3p does not automatically convert it into its X-symbol version. Can
this option be turned on from any menu?
There is not keyboard shortcut for the "Isabelle" menu. By means of
"Alt + e" or "Alt + t" one can move to the Edit or Tools menu, but
there is no such option for the "Isabelle" menu.
I could not find any mail address inside of the application to
which one could send any congratulations :-)) comments, questions or
suggestions.
Alltogether, I found it really nice and very convenient for starters,
and with minor improvements better than the emacs or xemacs options.
Congratulations to Holger,
best wishes,
Jesus
Email Gateway (Aug 18 2022 at 14:54):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Dear Isabelle users,
It is my pleasure to announce the first public release
of I3P, an Interactive Interface for the Isabelle Prover.
It is available from
http://www-pu.informatik.uni-tuebingen.de/i3p
The two goals of the I3P development are interactivity
and extensibility: users should be able to interact with
an interactive theorem prover in more ways than executing
and undoing commands, and they should be able to add
in well-defined ways specific user-interface functionality to
support them in their specific projects.
Here are a few reasons why you might want to give I3P a try:
It offers the main functionality of the Emacs-based
ProofGeneral: as the main difference, the keyboard shortcuts
replace Ctrl-C by Ctrl-Shift.
It builds on the Netbeans/Swing frameworks and thus offers
standard UI features: your students might appreciate the
well-known environment.
It handles copy & paste with XSymbols correctly.
It is portable and has been used under Linux and MacOS.
(Windows/Cygwin support will be added shortly.)
It is fast: the design pays specific attention to handling
large numbers of trace messages and large messages efficiently:
there is no real need to wait while the UI is scanning your traces.
It offers command-local tracing: several posts to this list
have asked whether it is possible to turn on tracing for
single commands. I3P offers this capability (command-local options)
on the interface side, by having the prover driver issue option
changes before and after command execution.
It has small release cycles: due to test-driven development of
the developed infrastructure layer (with the number of test
cases approaching 400), I feel confident in releasing updates
in short periods. An AutoUpdate-Service is included to inform
you about new versions.
It is extensible: the existing modules provide general
and documented mechanisms for plugging in new views and
commands.
It provides a framework for driving Isabelle-2009/-1:
several posts to this list have asked how to use Isabelle
as a background prover. The test cases of the Isabelle
driver of I3P show how to achieve this in a simple manner.
The installation effort is minimal anyway: just download the
binary, unzip, and start i3p/bin/i3p.
At most, you may want to install the IsabelleMono.ttf from
Isabelle2009-1/lib/fonts on your system and choose it for the
display under Tool/Options/Fonts.
I would also like to thank Makarius Wenzel, Burkhart Wolff,
and Achim Brucker for discussions about the requirements
on user interfaces for Isabelle. Furthermore, they and
Alexander Krauss and Julia Trieflinger have courageously
agreed to act as beta-testers for I3P and have provided
invaluable feedback on shortcomings and usability issues.
I am very grateful for any feedback you might care to give.
Enjoy,
Holger
Email Gateway (Aug 18 2022 at 15:00):From: Makarius <makarius@sketis.net>
I would like to encourage users to try it out and give some feedback,
either on this mailing list or directly to Holger.
Makarius
Last updated: Apr 24 2024 at 04:17 UTC