Re: [isabelle] Isabelle/jEdit - default logic



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 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 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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.