Re: [isabelle] Isabelle/jEdit - default logic
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
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
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
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
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).
Illegal character "$" in path element specification "'$AFP"
The error(s) above occurred in "'$AFP/Kleene_Algebra'"
The error(s) above occurred in session catalog
On 1/22/14 10:42 AM, Makarius wrote:
On Mon, 20 Jan 2014, Christian Sternagel wrote:
isabelle jedit -d .
isabelle build -d . -b FOO
2) Now I was wondering about the following: For users that start
Isabelle/jEdit via clicking on an icon, which is I guess equivalent
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and