Email Gateway (Aug 19 2022 at 13:31): Email Gateway (Aug 19 2022 at 13:31):From: Christian Maeder <Christian.Maeder@dfki.de>
Hi,
whenever a new Isabelle version comes out, I need some time to find out
how to build a heap image i.e. for HOLCF.
After unpacking Isabelle2013-2_linux.tar.gz and extending my PATH I now
called:
isabelle build -b -s HOLCF
(I'm no friend of the installation "when Isabelle is started for the
first time".)
Could this piece of information be put on a more prominent place. i.e.
into an INSTALL file, the FAQ or on the installation web page?
In fact, I only post this in order to improve the chance to find this
command faster next time.
Cheers Christian
Email Gateway (Aug 19 2022 at 13:31):From: John Wickerson <johnwickerson@cantab.net>
Hi Christian,
Could this piece of information be put on a more prominent place. i.e. into an INSTALL file, the FAQ or on the installation web page?
You might consider posting this on stackoverflow. There are a growing number of isabelle questions there, and the site is extremely googlable.
John
Email Gateway (Aug 19 2022 at 13:31):From: Makarius <makarius@sketis.net>
Have you tried starting the top-level "Isabelle" executable instead?
Going to Plugin Options / Isabelle there, you can select a different logic
session name. After restart, the required heap image will be built
automatically. There is no need for any command line invocation.
In the past 2 year I've spent a lot of efforts to make such things work
without further ado. At the same time I have stopped maintaining Isabelle
Proof General, and nobody has jumped in, so that is legacy since October
2011.
Makarius
Email Gateway (Aug 19 2022 at 13:31):From: Christian Maeder <Christian.Maeder@dfki.de>
Am 13.01.2014 16:30, schrieb Makarius:
On Mon, 13 Jan 2014, Christian Maeder wrote:
whenever a new Isabelle version comes out, I need some time to find
out how to build a heap image i.e. for HOLCF.After unpacking Isabelle2013-2_linux.tar.gz and extending my PATH I
now called:isabelle build -b -s HOLCF
Have you tried starting the top-level "Isabelle" executable instead?
Well, I called
Isabelle2013-2/Isabelle2013-2
as described at http://isabelle.in.tum.de/installation.html
This made the Pure and HOL heaps (only). I ignored/closed all pop-ups as
I only wanted to use isabelle-process in batch mode to see if old .thy
files still go through.
In fact, I've not tried yet if
isabelle tty -l HOLCF
works like older versions did.
And yes, I still prefer Proof General for my (limited) uses, although I
once tried the jedit interface because of a Proof General / emacs
problem. (Also our hets tool still uses "isabelle emacs".)
http://trac.informatik.uni-bremen.de:8080/hets/ticket/1042
Cheers Christian
Going to Plugin Options / Isabelle there, you can select a different
logic session name. After restart, the required heap image will be
built automatically. There is no need for any command line invocation.In the past 2 year I've spent a lot of efforts to make such things work
without further ado. At the same time I have stopped maintaining
Isabelle Proof General, and nobody has jumped in, so that is legacy
since October 2011.Makarius
Email Gateway (Aug 19 2022 at 13:31):From: Makarius <makarius@sketis.net>
On Mon, 13 Jan 2014, Christian Maeder wrote:
Well, I called
Isabelle2013-2/Isabelle2013-2
as described at http://isabelle.in.tum.de/installation.html
This made the Pure and HOL heaps (only). I ignored/closed all pop-ups as
I only wanted to use isabelle-process in batch mode to see if old .thy
files still go through.
We have a bit too many manuals, and getting attention of users into the
right corner is difficult.
For Isabelle2013-2 all defaults are for Isabelle/jEdit, there is also the
new "jedit" manual (accessible in the Documentation panel of
Isabelle/jEdit), which has near the start the following item:
The logic image of the prover session may be specified within
Isabelle/jEdit. The new image is provided automatically by the Isabelle
build tool after restart of the application.
Anything beyond selecting a logic image in Plugin Options / Isabelle (or
the Theories) panel is subsumed by the "system" manual, which is linked at
http://isabelle.in.tum.de/installation.html for "further technical
background information".
The assumption (and the hope) is that users invest time in getting
acqainted with the current generation of the Prover IDE, instead of
finding quick-paths to do it like in old times.
In fact, I've not tried yet if
isabelle tty -l HOLCF
works like older versions did.
No change here in recent releases. The "isabelle build -b" requirement
was the same in Isabelle2012 and Isabelle2013, if you really want to
bypass Isabelle/jEdit. Note that isabelle-process is really low-level,
normally you have your session ROOT files and use "isabelle build" as
explained in the "system" manual.
And yes, I still prefer Proof General for my (limited) uses, although I
once tried the jedit interface because of a Proof General / emacs
problem. (Also our hets tool still uses "isabelle emacs".)
The basic assumption is that people who are still using Proof General have
some extra time to tinker with shell scripts etc. I used to maintain
special tricks to get Proof General / Emacs run for most people out of the
box, but that is long past.
Now the remaining tricks are for the Java Runtime Environment on various
platforms, and Linux is not the best right now, especially various recent
forks of desktop environments. Windows and Mac OS X are more friendly to
users of Java. Hopefully Linux recovers eventually, when more and more
"free people" realize that there is a problem
http://linuxfonts.narod.ru/why.linux.is.not.ready.for.the.desktop.current.html
Makarius
Email Gateway (Aug 19 2022 at 13:31):From: Makarius <makarius@sketis.net>
I see the old "COMP" attribute on that tracker item. The NEWS file for
Isabelle2013 (February 2013) has the following entry on it:
In current Isabelle2013-2 (December 2013) the Documentation panel provides
quick access to this important file, which documents user-relevant
changes. Morever, the Sidekick plugin provides some basic tree view for
it, to get an overview of the long history of NEWS.
Makarius
Email Gateway (Aug 19 2022 at 13:31):From: Christian Maeder <Christian.Maeder@dfki.de>
Am 13.01.2014 21:11, schrieb Makarius:
On Mon, 13 Jan 2014, Christian Maeder wrote:
I see the old "COMP" attribute on that tracker item. The NEWS file for
Isabelle2013 (February 2013) has the following entry on it:
- Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY,
use regular rule composition via "OF" / "THEN", or explicit proof
structure instead. Note that Isabelle/ML provides a variety of
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
with some care where this is really required.
Right, I saw that entry, but still was not able to adjust our old proof.
Thanks Christian
In current Isabelle2013-2 (December 2013) the Documentation panel
provides quick access to this important file, which documents
user-relevant changes. Morever, the Sidekick plugin provides some basic
tree view for it, to get an overview of the long history of NEWS.Makarius
Email Gateway (Aug 19 2022 at 13:32):From: Makarius <makarius@sketis.net>
It depends what you a trying to do with COMP, which became out of use many
years ago. A more current approach is to use the Pure "prop" marker (a
special constant) to indicate the intended rule structure, and then use
regular OF or THEN. This is for tools that do some low-level tinkering of
rule; normal end-user applications use high-level infrastructure like
locales and interpretation.
To ease the initial transition to the current Isabelle2013-2 release, here
is a definition of the old attribute for your own theory context:
attribute_setup COMP = {*
Attrib.thm >> (fn B => Thm.rule_attribute (fn _ => fn A => A COMP B))
*}
The 'attribute_setup' command is described with some basic examples that
can be combined with the above NEWS to produce that Isabelle/ML snipped.
What is still missing in the Prover IDE is some hyperlink from formal
entities like 'attribute_setup' to the corresponding documentation. The
manual has that markup already, but the connection in the user interface
is not yet there.
Makarius
Email Gateway (Aug 19 2022 at 13:32):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
If that's to PDF documentations, there is no easy way to achieve this, as
not all PDF readers support anchor on the command line like the Adobe PDF
reader do.
Last updated: Apr 19 2024 at 08:19 UTC