Subject: Fragments

Keywords: ::recipe
          ::bot
          ::implementation
          ::usage

Title: Interactive Fragment recipes 

--------------------------------------------------
  
See Interactive Fragment Pipeline


new_source_table (iobid InfoReplay) `All` true (3,0) (iobid theories)
new_dekreitz_table `All` true (3,0) <interactive-source-obid>
 - must activate proxy object

launch_interactive_fragment_generator `Mathematics`
  - doesn't automatically join the editor, thus view replay object and join
launch_interactive_dekreitz (iobid <source table obid>) <edit-environment-stamp>
  - edit-environment-stamp
      * launches from lib so can not use (current_environment_stamp())
      * eval current_environment_stamp() in EDD then cut and paste resulting term 
  - activate InteractiveSource_<vers>_dbbot_dekreitz_... proxy object

add and set UpdateProvisonal property of replay bot to be T:b
  - this is included in parms somehow and not props thus probably don't need to add to props

update INTERACTIVE_DEKREITZ of InteractiveFragmentReplay bot to be obid 
of interactive dekreitz dbbot

maybe clear : properties_hashtable_clear frag_interactive_inf_cache
or restore  : frag_table_inf_obids false `Interactive_Source_3_0`

launch_interactive_thin (iobid <dekreitz-table-obid>) <edit-environment-stamp>
  - must activate proxy_object 

launch_interactive_alpha  <thin-obid> <edit-environment-stamp>
  - activate
  - thin obid is irrelevant? put Interactive thin dbbot?
  - does not populate bot table from Thin tables
    for each thin table, run query using pattern in bot proxy to find 
    thin records with Interactive prop and no alpha and queue them to bot.
    see frag_interactive_thin_todo

launch_interactive_fragment_generator <theory-group>
  - !! interactive_fragment_replay is the generator and here we launch it with some new props !!  
  - reuses props from interactive_fragment_replay
    but updates ``DISPATCH APPENDP DB FragmentInteractive``
  - theory group : `Analysis` | `Mathematics`
      * avoids inserting source fragments for STMs not in theories for which
        fragments are being maintained.
      * interactive_fragment_replay has `FragmentInteractive` property 
        which also specifies a theory group
          - this theory group limits whats added to Interactive_Source table 
            how is correct version of Interactive_Source table found?
              * launch function's hardcoded dbargs prop points to Interactive_Source table
  - maybe_update_provisional_replay_fragments uses frag_is_theory_active 
    and so on until frag_active_theory_p has hard coded reference to  
    interactive_fragment_replay where its `FragmentInteractive` property is 
    used to judge where theory of STM is active. 
  - instead should somehow find `FragmentInteractive` property of ?generator?

Starts silently must Join* from button in body of interactive_fragment_replay
The frag bots can be resumed from proxy object menu.
  - what is proxy object menu? probably the object menu of the interactive bot  

The replay_bot
 - adds to source table found as first string of dbargs of DB prop of replay bot.
 - queues new source fragments to bot found in INTERACTIVE_DEKREITZ prop of replay bot
   INTERACTIVE_DEKREITZ property should be set appropriately in the replay bots object term.
   ie INTERACTIVE_DEKREITZ: Interactive_Source_3_0_dbbot_dekreitz_3791567537
 

when interactive dekreitz fragments created how to they get added to interactive thin bot? 

How do partial subproofs get added to InteractiveReplay???
  - after each refine, walk tree and look for complete subproofs?
  - replay bot finds maximal complete subproofs when pobid queue to interactive replay.
      * how to prevent redoing unaffect subtrees any time some other subtree completed?
          - remember inf obids and maintain cache
            see: fragment_interactive_inf_obids, but local to refiner, should do in lib.
          - dups not harmful except waste cpu/time 

 ? not sure this is correct:
   Must run Interactive replay bot until Source table has a record 
   before you can start dekreitz bot since bogus failure if try to start bot with no
   records!
   If so, a bit of a conumdrum since interactive replay expects dekreitzer to be running
   as it needs to queue replayed sources to dekeritzer.

⋅
--------------------------------------------------

Authors: 

Contributors: NUPRL:t
              RICH:t

⋅

Home