Search code examples
isabelle

How to see all the active Isabelle sessions?

This question is connected with my other question How to export Isabelle session from the Windows installation? . Maybe that other question can be solved if I indicate the correct session name.

So - my question is - how to see all the active Isabelle sessions if jEdit if used for the editing of some custom theory file.

I can call jEdit plugin 'Plugins - Isabelle - Browse Session information' and I am getting the tree in left-side panel:

+ isabelle-session:
  - HOL

So - I guess - HOL is the parent session but the concrete session for the current theory file is something other, maybe default, maybe unnamed?

When I export HOL session, then current theory file is not among the exports. So - I have tried to export this unnamed default session, but without result:

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test1 -x *:**  Unsorted
*** Undefined session(s): "Unsorted"

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test1 -x *:**  isabelle-session
*** Undefined session(s): "isabelle-session"

So - if I could see all the active sessions, including the name of the most concrete, most low-level session (in which the current theory file is processed directly), then I would be able to export this concrete session and hence - my current theory file for the import into mmt.

Solution 
  • isabelle build -a -n -v

    is the exact answer to this question. E.g.:

    tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle build -a -n -v
Started at Sat Mar 27 01:28:30 GMT+2 2021 (polyml-5.8.2_x86_64_32-windows on DESKTOP)
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-windows"
ML_HOME="/cygdrive/c/Homes/Isabelle2021/Isabelle2021/contrib/polyml-test-f86ae3dc1686/x86_64_32-windows"
ML_SYSTEM="polyml-5.8.2"
ML_OPTIONS="--minheap 500"

Session Pure/Pure
Session CTT/CTT
Session Cube/Cube

    Although this command lists all the sessions, one can see that this list does not contain the currently opened custom theory file.

    The big issue with Isabelle presentation is the following issue: newbies are eager to start with creation of new theory files, that is why he or she opens jEdit, creates new file, imports parent theories and starts editing. One expects that all should be fine. But it is not fine. Such standalone theory file can be edited and checked, but it is orphaned, it does not belong to any sessions. E.g. this file has no its own sessions. This file does not belong to one parent session (e.g. HOL or Pure), because file is not exported as part of parent sessions.

    So - one should clearly document in Isabelle documentation that one is expected to create session at first (kind of project or solution folder/file like in industrial programming languages). This creation of session is quite tricky and unexpectedly confusing - one should create ROOT file, place it in some directory and then start jEdit from command line with special options that indicate that jEdit should be joined to this folder/session. And only after such setup the currently edited file belongs to session (I am trying to check this setup).

    Every IDE (like Visual Studio or Eclipse) provides IDE-in-build tools for managing solution/project infrastructure, so - maybe it could be good that jEdit have such session management plugins as well and maybe jEdit startup process can be made more intuitive that invites to use sessions explicitly as modern IDEs presses users to put all their work inside solutions or projects.

    E.g. I have created ROOT file (I hope it works. I have not managed to find ROOT example file for one-simple-theory-file project):

    chapter Algo

session Algo = Pure +
  description "
    Classical Higher-order Logic.
  "
  options [strict_facts]
  sessions Tools
  theories
    Main (global)
    Complex_Main (global)
  document_theories
    Tools.Code_Generator
  document_files
    "root.bib"
    "root.tex"

    And I have tried to start jEdit with - but it gave error (see trace):

    tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle jedit -d /cygdrive/c/Workspace-Isabelle2021 -l Algo
01:58:55 [AWT-EventQueue-0] [error] PluginJAR: Error while starting plugin isabelle.jedit.Plugin
01:58:55 [AWT-EventQueue-0] [error] PluginJAR: *** Duplicate global theory "Main" (line 3 of "/cygdrive/c/Homes/Isabelle2021/Isabelle2021/src/HOL/ROOT")
01:58:55 [AWT-EventQueue-0] [error] PluginJAR:  at isabelle.Exn$ERROR$.apply(exn.scala:28)
01:58:55 [AWT-EventQueue-0] [error] PluginJAR:  at isabelle.Exn$.error(exn.scala:32)

    After some experiments I shortened my ROOT to:

    chapter Algo

session Algo = Pure +
  description "
    Classical Higher-order Logic.
  "
  options [strict_facts]
  document_files
    "Max_Of_Two_Integers_Real.thy"

    I started jEdit with:

    tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle jedit -d /cygdrive/c/Workspace-Isabelle2021 -l Algo

    But there are 2 strange things:

    1. Draft/scratch document empty page is presented as the default document. When I am trying to load my theory file (Max_Of_Two_Integer_Real.thy) there is nothing in jEdit that would show that Workspace-Isabelle2021 is my default directory for this session.
    2. I tried to export sessions and again - without any success:

    e.g.

    tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test2 -x *:**  Unsorted
*** Undefined session(s): "Unsorted"

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test2 -x *:**  Algo
*** Undefined session(s): "Algo"

    This is really confusing. The first thing that I checked is Isabelle session plugin. I expected to see session Algo, but there was session Unsorted. However - none of these sessions could be exported - as seen by the Undefined sessions message.