Dynamic components/components with startup arguments

Isabelle is started with

isabelle logicname

where logicname is chosen from a list of heap images in the system/user's directory. The command

isatool findlogics

prints a list of the available heap images to the terminal. At the moment the existing interfaces each hard wire this command behind the scenes to refresh menus.

How can we do this kind of thing cleanly for PG Kit? Possibilities:

  1. secondary process updating component configurations for broker -- ugly/compilicated
  2. Isabelle itself doing same -- cleaner but a bit hacky
  3. custom handling of component arguments similar to object mechanism -- can of worms

Any others? Perhaps 2 is the best option, although other provers may also have usefully adjustable startup parameters.

-- DavidAspinall - 29 Sep 2006

The broker already supports the updating of component configurations, i.e. we can add new components to a running broker. This supports (1) above very cleanly: to start Isabelle, we would start a compont which in essence calls "isaool findlogics", and sends the result back as a list of new component configurations, each corresponding to one instance of Isabelle. Then user can select which Isabelle logic they want (they'd appear as different provers in the prover startup menu offered by the display).

Some displays like PGEmacs or PGWin2 do not allow a prover startup menu, and just ask for a fixed prover to be run. That's fine as well, you just have to specify which Isabelle logic you want.

-- ChristophLueth - 29 Sep 2006

Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r2 - 29 Sep 2006 - 13:59:45 - ChristophLueth
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies