Re: [isabelle] Isabelle/jEdit - default logic



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.