Subject: Fragments

Keywords: ::policies
          ::overview

Title: Interactive Fragment Pipeline

--------------------------------------------------

Sourced from
  - refine results 
     * add new working source node as fodder for fragments
  - failing subtrees of replay failures
     * presuming that subtrees of failing node may work and be helpful in fixing proof. 
  Question as to whether to use only known working complete subtrees or cast a wider net

AOGT : proof address # Inf obid # goal # tactic

Overview:
  - queue aogts to replay bot
  - replay aogt
    if successful add do Interactive Dekreitz table and queue to interactive_dekreitz bot
  - dekreitz : adds to which Thin table?
      * uses thin_tables in fragdb table groups to find appropriate table for theory
  - Thin/Alpha do inherit `inf_obid` and `Interactive` properties
    Eventually want Interactive to be Provisional, but at the moment 
    provisional_fragment_propname = `Interactive`

How to clean uncompletable and failing ?
    
see also Interactive Fragment recipes

Interactive Fragments are in some sense ephemeral: 
  - scratch proofs
  - orphaned subproofs
  - orphaned proofs, ie new proof 
  - goal modification
  - STM movement

STM deletion/deactivation
  - reference environment unusable
      * repair re :
        try choosing first hie obj in theory following lastest refd hie object
        if occurs in proof successfully then that proof could make refenve
      * invalidate fragments using that reference enviroment
      * if inactive then somehow "deactivate" fragment

Incrementally adds fragments as subtrees of proofs are completed.
  - Also add fragments from replay failures, by finding maximal replayable
    subtree of failure address.

Harvest top down or bottom up?
  - top down
     * if sequent changes but tactics still work then successful
     * failure stops recursion
         - no, since can still recurse on children as new tops
           requires goals from source tree and not just tactics, 
             * aogt, address, obid, goal, tactic
Do not want some transient experimental partial proof to overwrite persistent
record derived from a complete proof.

Source addresses of provisional are less stable since proof is not complete and thus
will be modified. 

Provisional have special props:
  - `inf_obid` : obid of inf, 
      * since addresses unreliable includes INF obid. Might make sense for all source fragments
  - `Interactive` : !bool term
      * identifies as provisional, would need to be removed if inherited to become persistent
      * should change this to `Provisional`

Duplicates : provisional
  - Provisional fragments are more likely to become invalid;
     * fail due to STM deletion
     * not replayable due to STM movement, tactic or definition change.
  - what qualifies as duplicate?
    step is same, same goal, same tactic, and same subogals including number of subgoals,
    thin use lex_equal on sequents, alpha does test alpha equal.
      * if refenv same then identical.
        one should have not been produced but instead inherited the other.
      * otherwise the earlier (lower hrank) RefEnv is considered better.
          - but if one is ephemeral, then want to keep other as backup
            ie the ephemeral is provisional
      * other possible definitions of better 
          - fewer subgoals
          - faster, lower resource usage
          - different subgoals with more efficient completions
  - provisional validity
     * refenv valid, ie fragment should work as expected
  - provisonal maintenance:
     * want to maintain provisional fragments that are valid
       even if no longer used in proof.
         - generated from extant step
         - used when building fragment proof.
     * source addresses unreliable

Allow Duplicates ?
  Currently dups only detect if hranks and steps same and both provisional (have `inf_obids`)
  so all good except need GC to clean out provisional when better or as good non-provisional exists.
  - avoid building fragments from proof steps generated from fragments
      * how to identify
          - could be generated then modified.
          - look for name_ap or any tactic description obid
  FTTB : should not allow modification of generated steps
    ? eventually have transformation of generated to native 
      such that step must be transfomed prior to modification
    ? recoginize fragment instance in dekreitz and either
      invalidate if no longer conforms or ignore if conforms.
      or for now just fail dekreitz.

   ? hpf utility functions cause missing func description failures at dekreitz
       - skip/fail if exists an hpf utility func.
  

all things being equal prefer fragments that are not provisional
when adding complete proof, inherit the identical provisional fragments.


hrank   (position in hierarchy) 
  - earlier : usable by more lemmas. 
  - later : maybe better since has more to refer to. 

better  (fewer hyps, faster)

At insert
new is better -> overwrite - ie use old key with new record.
  - prevents garbage accumulation since old record is implicitly deleted
    and do not have to update referencers.
  - if new value is provisional then do not overwrite a non-provisional
  - provisional should come later than non-provisional

unreplayable provisional fragments when refenv is still ok means
tactic or def mod.
  - has no replayable source step: unlikely that source succeeds when some 
    derived fragment fails.

policy : preserve persistent keys.
  - referenced by completion ancestors
  - referenced by origin/source
  - referenced by proofs, not needed to replay proof but
    preferable that all keys in proofs reference valid fragment.

Ok for completion of provisional to reference other provisional
 but if possible should prefer persistent in completions of persistent

policy: cleaning shouldn't remove replayable orphans?
  Until have some metric for preferability probably best to limit orphans.
  - replays, but some completion descendent does not, expect if 
    usable then regenerate from source?

policy: all references to fragments in fragments and proofs
  should be valid.

policy: no identical records (identical where on is persistent and one is provisional ok)
        no equivalent persistent records.
  
if we insert better provisional without overwriting and thereby shadow old :
  - if provisional becomes persistent ie included in main complete proof
      * shadowed should be overwritten
          - but key is not in proper spot thus needs to be moved.
      * provisional should be orphaned
    essentialy want to keep the key of the old persistent, move it to provisional
    position, and remove provisional key
  or  * provisional gets overwritten,
      * old persistent gets removed
    easier but harder to maintain consistent referencees

  could remove key from index but keep record, no new references would be made but old
  would continue to work, eventually rebuilding completions/proofs will loose ref

              
%---%
 fttb maybe just treat interactive as though persistent and fixup as normal when they 
 go bad or get orphaned.
  
 paddrs made in queueing complete refinements to interactive generator
  are somewhat nonsensical since paddr arg maybe from partial proof
  and yet we combine that with stm obid where addrs are relative to whole proof.
  should avoid adding such addrs to fragments, but to prevent breakage in case there is a
  code dependency on the address existing, used the fudged one fttb. At some point fix.

as addresses are unreliable we use inf-obid to detect if step has been seen.
  - too expensive to query for obid occurrence at each potential update
  - lib can keep list of recently added.
      * could init list with a query to find all obids in provisional fragments 
        of source tables
      * maintain segregation of provisional in special table then just need
        to extract obids from special
      * when proof is completed, same steps may be added to persistent tables.
          - should result in identical general fragments and thus provisional
            should be overwritten with persistent.
  - could add `Fragment`, <FKey> substantive property to INF obid             

Any Source step that refines can be dekreitzed
Some descendent may not refine, resulting in dekreitzed steps that
can not be thinned as no completion exists.
  - leave since hole may be filled later.
  - clean since should be added again when hole is filled.
      * depends on methodology of updating Source_Interactive from refine bot.
  - could be significant quantity

how are source fragments added from failing/incomplete prfs
ancestors of failing nodes not good
complete subtrees are good
  - how to find working complete subtrees
      * siblings of failed addresses
      * subtrees of failed, 
        recheck subtrees or pass goals 



  clear frag_interactive_inf_cache
  delete Interactive Source and Dekreitz tables

  clean orig of Interactive Thin fragments : frag_clean_interactive_orig
  init frag_interactive_inf_cache with frag_table_inf_obids 
  
 
update can be done simultaneously by replay in update mode with UpdateProvisional
 replay and update db
 replay and UpdateProvisional

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

Authors: RICH:t

Contributors: NUPRL:t

⋅

Home