Email Gateway (Aug 19 2022 at 13:18): Email Gateway (Aug 19 2022 at 13:18):From: Makarius <makarius@sketis.net>
On Mon, 20 Jan 2014, Christian Sternagel wrote:
isabelle jedit -d .
isabelle build -d . -b FOO2) Now I was wondering about the following: For users that start
Isabelle/jEdit via clicking on an icon, which is I guess equivalent to doing$ISABELLE_HOME/Isabelle2013-2
on a console. How are they expected to access FOO as default logic?
The command lines of "isabelle jedit" and "isabelle build" coincide on
some options to manage the session name space and select logic images.
See also the description of "isabelle build" in the system manual. It has
the following additional explanation of option -d:
Any session root directory may refer recursively to further directories
of the same kind, by listing them in a catalog file ROOTS line-by-line.
This helps to organize large collections of session specifications, or
to make -d command line options persistent (say within
$ISABELLE_HOME_USER/ROOTS).
Maybe the logic selector should provide all images that are present in
ISABELLE_PATH ?
The ISABELLE_PATH does not account for the session name space, it is
merely a way to find potential heap images in the file-system. Note that
this is in contrast to very ancient modes of operation of
isabelle-process, isabelle findlogics, and Proof General.
But then again, how are GUI-only users expected to build FOO in the
first place?
By using $ISABELLE_HOME_USER/ROOTS mentioned above. In principle the
Prover IDE should provide more direct access to ROOTS at some point, but
this is not implemented yet.
I get myself occasionally confused about the new toplevel application
wrappers, which are available on all platforms in Isabelle2013-2. Since I
am rarely in the privileged situation to use Isabelle as regular user, I
usually have old-fashioned "isabelle jedit" invocations on the
command-line, with slightly different semantics.
Maybe it would be good to have something like the former "build_dialog"
that can be started from within Isabelle/jEdit?
The build_dialog was just an intermediate thing, to help a hypothecial
Proof General maintainer to do what Isabelle/jEdit also does by itself via
isabelle.Build in Isabelle/Scala. Since no Proof General maintainer
showed up in such a long time, I have removed the "build_dialog" shell
script wrapper for Isabelle2013-2.
Makarius
Email Gateway (Aug 19 2022 at 13:34):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
1) First a trivial observation: When I start Isabelle/jEdit via
isabelle jedit -d .
and the current directory contains a ROOT file with a session FOO, then
the logic selector in the theory panel will contain the session FOO.
If I do the same via
isabelle jedit
FOO is not there, which is expected.
Now, after doing
isabelle build -d . -b FOO
there is the heap image FOO in my ~/.isabelle/Isabelle2013-2/heaps/...
but nevertheless the logic selector will not contain FOO when starting
jEdit via
isabelle jedit
Again, this is as expected.
2) Now I was wondering about the following: For users that start
Isabelle/jEdit via clicking on an icon, which is I guess equivalent to doing
$ISABELLE_HOME/Isabelle2013-2
on a console. How are they expected to access FOO as default logic?
Maybe the logic selector should provide all images that are present in
ISABELLE_PATH ? But then again, how are GUI-only users expected to build
FOO in the first place? Maybe it would be good to have something like
the former "build_dialog" that can be started from within Isabelle/jEdit?
cheers
chris
Email Gateway (Aug 19 2022 at 16:44):From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Makarius,
Basic question: in Isabelle2014 (GUI), how do I start with a heap I
have built, instead of HOL?
In Isabelle2014, if I build a heap with say
isabelle build -d '$AFP/Kleene_Algebra' -b Kleene_Algebra
or
isabelle build -s -d '$AFP/Kleene_Algebra' -b Kleene_Algebra
this puts a heap in the expected place(s). However, I am clueless as to
how to start Isabelle/jEdit with such a heap. If I start up the
Isabelle/jEdit GUI,
Kleene_Algebra does not appear as a choice for logic in the pull-down
menu in the Theories panell (although I believe it use to in an older
version). If I try
isabelle jedit -l Kleene_Algebra
I get a box with
Undefined session(s): "Kleene_Algebra"
This is despite having /Users/elsa/svn/AFP in my
~/.isabelle/Isabelle2014/etc/components
file. Below you quote a paragraph from system.pdf suggesting that
using ROOTS in the $ISABELLE_HOME_USER directory will somehow address
this. I'm not at all sure what this has to do with the -d flag for the
isabelle executable, which allows the user to specify a directory for
finding the ROOT file for a session. More to the point, I do not know
how to use ROOTS. The ROOTS file in $ISABELLE_HOME contains a
collection of path fragments. I gather the sessions described in the
ROOT files in those directories are made available as the choices of
starting logic (?) for an Isabelle session. But there are way more
"logics" than heaps, so I'm not even sure if this is particularly
relevant Are these paths interpreted relative to the location of ROOTS,
$ISABELLE_HOME, the $ISABELLE_PATH, or what? If I put
'$AFP/Kleene_Algebra' in ROOTS, I get
Illegal character "$" in path element specification "'$AFP"
The error(s) above occurred in "'$AFP/Kleene_Algebra'"
The error(s) above occurred in session catalog
"/Users/elsa/.isabelle/Isabelle2014/ROOTS"
If I put an absolute path into ROOTS in $ISABELLE_HOME_USER, then it
offers it to me as a choice of Kleene_Algebra in the logics, but
choosing it seems to have no real effect; it still loads the theories in
Kleene_Algebra over again, apparently from Main. For Kleene_Algebra, we
are only talking about a few theories of relatively modest size.
However, I have need of half a dozen or so theories from AFP, including
JinjaThreads, as well as a few home-grown libraries and I really need
not to have to rebuild all that every time I try to get some work done
in Isabelle (or even just try to continue the very painful fight to
bring my work up to date with Isabelle 2014).
---Elsa
On 1/22/14 10:42 AM, Makarius wrote:
On Mon, 20 Jan 2014, Christian Sternagel wrote:
isabelle jedit -d .
isabelle build -d . -b FOO2) Now I was wondering about the following: For users that start
Isabelle/jEdit via clicking on an icon, which is I guess equivalent
to doing$ISABELLE_HOME/Isabelle2013-2
on a console. How are they expected to access FOO as default logic?
The command lines of "isabelle jedit" and "isabelle build" coincide on
some options to manage the session name space and select logic images.
See also the description of "isabelle build" in the system manual. It
has the following additional explanation of option -d:Any session root directory may refer recursively to further directories
of the same kind, by listing them in a catalog file ROOTS line-by-line.
This helps to organize large collections of session specifications, or
to make -d command line options persistent (say within
$ISABELLE_HOME_USER/ROOTS).Maybe the logic selector should provide all images that are present
in ISABELLE_PATH ?The ISABELLE_PATH does not account for the session name space, it is
merely a way to find potential heap images in the file-system. Note
that this is in contrast to very ancient modes of operation of
isabelle-process, isabelle findlogics, and Proof General.But then again, how are GUI-only users expected to build FOO in the
first place?By using $ISABELLE_HOME_USER/ROOTS mentioned above. In principle the
Prover IDE should provide more direct access to ROOTS at some point,
but this is not implemented yet.I get myself occasionally confused about the new toplevel application
wrappers, which are available on all platforms in Isabelle2013-2.
Since I am rarely in the privileged situation to use Isabelle as
regular user, I usually have old-fashioned "isabelle jedit"
invocations on the command-line, with slightly different semantics.Maybe it would be good to have something like the former
"build_dialog" that can be started from within Isabelle/jEdit?The build_dialog was just an intermediate thing, to help a hypothecial
Proof General maintainer to do what Isabelle/jEdit also does by itself
via isabelle.Build in Isabelle/Scala. Since no Proof General
maintainer showed up in such a long time, I have removed the
"build_dialog" shell script wrapper for Isabelle2013-2.Makarius
Email Gateway (Aug 19 2022 at 16:54):From: Makarius <makarius@sketis.net>
On Wed, 31 Dec 2014, Elsa L. Gunter wrote:
Basic question: in Isabelle2014 (GUI), how do I start with a heap I have
built, instead of HOL? However, I am clueless as to how to start
Isabelle/jEdit with such a heap.
Building heaps (or "logics") yourself is sometimes needed in batch mode,
but normally you don't do it manually when working with PIDE. You just
tell Isabelle/jEdit where to find ROOT or ROOTS files via option "-d DIR",
and it will allow you to select additional sessions in the GUI or via
option "-l SESSION".
Below you quote a paragraph from system.pdf suggesting that using ROOTS
in the $ISABELLE_HOME_USER directory will somehow address this.
The ROOTS files allow to make -d options (of isabelle build or isabelle
jedit) persistent. The shortest answer to all your questions is to have
$ISABELLE_HOME_USER/ROOTS with a line like this
$AFP
without any extra quotes or spaces -- this is not a bash script, just a
text file with lines to be taken literally.
I principle, AFP as a "component" could do this for you, but it refrains
from it by default, since its session name space is quite large, and would
affect important maintenance operations like "isabelle build -a".
Makarius
Last updated: Apr 19 2024 at 04:17 UTC