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:
- secondary process updating component configurations for broker -- ugly/compilicated
- Isabelle itself doing same -- cleaner but a bit hacky
- 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
Aha, that's good. 1 is messy but maybe not so complicated. Probably this should be thought of as a non-problem for now.
Can we remove/replace components as well as add them?
--
DavidAspinall - 29 Sep 2006