Subject: Fragments

Keywords: ::clean

Title: Clean up bad replay

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


Grind Fail : first make invalid, then clean as usual.

Dekreitz : replay

 annotate as orphaned source with !void for source property.

 invalidate
   - unreplayable dekreitzes 
     siblings of unreplayable dekreitzes
   - unreplayable thins
   - thins of invalid dekreitzes
   - ancestors of invalid thins.
   - alphas of invalid thins.
   - unreplayable alphas (fttb: not replaying alphas), 
      assuming thin unreplayable if alpha wouuld be
   - ancestors of invalid alphas.
  
 clean
   - for all source if there exist an invalid dekreitz  
     remove tnf and dekreitz properties
   - delete invalid dekreitzes
   - for all dekreitz if thin is invalid
     remove Thin property
   - delete invalid thins
   - delete invalid alphas

 repair
   - replay all stms with a source without dekreitz/tnf properties 
   - tnf/dekreitz
   - thin

  frag_invalidate_unreplayable_dekreitz :
    - ? invalidate orphaned dekreitz ? 
    - invalidates unreplayable dekreitz
    - foreach source containing invalid dekreitz:
        * invalidate all dekreitz

  frag_invalidate_thins :
    - invalidate union 
        * unreplayble thins
        * thins of invalid dekreitzes
        * ancestors of invalid thins

  frag_invalidate_alphas :
    - invalidate union 
        * unreplayble alpha
        * alphas of invalid thins
        * ancestors of invalid alphas

 it is possible for a dekreitz record to have a link to an invalid Thin.
 Thin is invalid due to Thin replay or Alpha grind failure,
  but dekreitz replay still succeeds.
  thus after cleaning thin need to check for stale links in dek recds?
 "down" pointers are removed but not "up"? One reason is that most if not
 all records with bad up pointer will themselves be removed.
 EG, thin_clean clears pointers in deks to invalid thins but no check is 
  made of orig pointers in alphas to deleted thins.
  After deleting records should check down table origs
  and clear any bad pointers.
 Prob ok to just do separately.  

  frag_dekreitz_clean :
     -remove tnf/dek properties from source
    - delete invalid dekreitz

  frag_thin_clean :
    - foreach dekreitz with invalid thin remove Thin property
    - delete invalid thins.

  frag_alpha_clean :
    - foreach thin with invalid alpha remove Alpha property
    - delete invalid alphas.

  stms_to_replay : stms for which there exists a source record with no dekreitz prop

 
 Annotate : 
  - Annotate dekreitz replay fails as invalid  
  - Remove tnf and dekreitz props of orig of invalid dekreitz.
      * may orphan other dekreitz
  - Annotate thins of invalid dekretiz as invalid
      * other dekreitz may point to thin
        then their replays should have failed as well?
          - possible they had some extra hyp that allowed replay even 
            though that hyp was unneeded in the past.
  - Annotate ancestors of invalid thins as invalid % having missing_descendant%
    Or invalidate them and let thin redo. 
      * may want to keep working but orphaned alpha but no need for thins 
      * thin may change ancestors since hyps may differ

 Clean :
  - Remove invalid thins and their ancestors in completion tree 
  - Remove invalid and orphaned dekreitzes
  - Remove keys to deleted dekreitzes from source
  - Remove keys to deleted    
  - Remove invalid thin prop from dekreitzs
      * irrespective of whether Thin orig is dekreitz.
  - Remove orphaned orig prop from thins

 Invariants after clean :
  - No source with invalid dekreitz exists.
  - No orphaned dekreitz (includes invalid) exist.
  - No dekreitz has dead Thin property
  - No thin which was derived from invalid dekreitz exists.
  - Orphaned thins exist.
  - MissingDescendant thins exist.
      * May(must?) Exist completions with key of removed invalid thin!
        ? could remove and rely on MissingDescendant to prompt repair ?
        ? could replace with dummy key like with invalid as table name ?

 Repair :
  - replay and update source without tnf/dekreitz
  - tnf and dekreitz source 
  - thin dekreitz
      * may adopt orphans  
  - fixup missing descendants.
    Find least missing descendant and look for completion.
    There could exists missinng descendants that can not be repaired:
      For example: might exists a hyp previously thinned which is now needed to
                   complete proof. ancestors of least thin needing that hyp may 
                   have thinned it and now they can not be completed.
    If after repair missing descendants still exist, then those thins should be
    made invalid and be removed and associated deks cleaned and rethinned.
    Would be sufficient to just invalidate missing descenent leaves, then retry repair.
      - may result in many passes.
      thus maybe best to invalidate back to root. 
     
frag_dekreitz_replay_failures_wsrc    
frag_dekreitz_replay_failures_wthin    

annotate_dekreitz_replay_fails (ioid InfoReplay) `replay` <dek_table> 

Alpha : ?

Thin : 
  Annotate bad replay as invalid.
  Remove pointers, to the invalid records, from dekreitz.

  Annotate associated alpha as invalid (or check w replay)
 
  Annotate associated dekreitz records and replay (should fail replay)
   or just assume they're bad and annotate as invalid.

  Thin makes a initial check if a matching thinned record exists for same
   stm and adopts if so.


  
Source

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

Authors: 

Contributors: NUPRL:t
              RICH:t

⋅

Home