This is a paraphrasing of a mail by Christoph from 25 Sept 06:

When a prover exits, the broker will mark all processed atoms in source files loaded by that prover as "outdated", and will reject all attempts to bring these atoms up-to-date (giving an error message to the effect that the prover has exited). So users can't do anything with these source files any more excepting for saving them. It would be natural to allow a prover on restarting to reopen (without even needing to reparse) its source files. (Of course, all atoms are status "outdated" or "fresh parseley" then.)

Thinking this further, I wonder if displays actually want to refer to provers by their id as they currently do now. Maybe displays only want to refer to provers by their component id? I.e. I only want to load this file into Isabelle2005/HOL, not that precise running instance of Isabelle2005/HOL with session id very.long.and.complicated.and.lots.of.numbers:123457890. The broker could handle the starting of the prover, and the mapping of component id's to session id's behind the scene.

Of course, with this scenario, it would not be possible for a user to run two instances of the same prover. One might be tempted to think that this is a good thing.

The question here: is it sufficient that we tacitly replace the meaning of proverid in display messages such that where before it meant the session identifier of the prover (identifying one running instance) it now means the componentid of the prover (identifying the type of the prover, e.g. Isabelle 2005/HOL)?

-- ChristophLueth - 26 Sep 2006

Edit | Attach | Print version | History: r4 < r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r2 - 27 Sep 2006 - 10:52:34 - DavidAspinall
 
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