Subject: Fragments

Keywords: ::usage
          ::clean
          ::recipe

Title: fragment table maintainence recipes

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

show replay failures

show grind failures : ie invalidate grind with forreals false

replay with update to update any proofs modified to resolve grind failures
 - may oprhan source records of modified proofs.

? better to invalidate and clean from alpha to source or vice versa
 - affects orphans
 - frag_invalidate_dekreitz invalidates dekreitz siblings
     - frag_invalidate_thins invalidates thins of invalid dekreitz
       thus if invalidate_thins done after invalidate dekreitz
            and before clean dekreitz
        then more thins would be considered invalid.
 - frag invalidate dekreitz grind/orphans
     - if done prior to invaidate thins, then would cause a working thin
       to be invalid if orig dekreitz is invalid.
     should be few in invalid grind/orphan and very few valid thins originating
     from invalid deks. 
Thus in general probably better to invalidate/clean bottom up.

better to invalidate source prior to dekrietz?
  - invalid source results in orphaned dekreitz

replay alpha
replay thin
replay dekreitz
replay source
 
invalidate alpha grind failures 
invalidate alpha hrank inconsistency 
invalidate thin grind failures
invalidate thin hrank inconsistency 
invalidate alpha
invalidate thin
clean thin/alpha
invalidate source grind failures
invalidate source orphans
invalidate dekreitz grind failures
invalidate dekreitz orphans
invalidate dekreitz
clean source/dekreitz 

remove source orphans?
 
replay theories in update mode


NB: source_keys_of_stm will not include orphaned records as keys of `source` property.
    frag_stms_records will include orphaned.

Have Source records with grind fail from TNF,
 modified proofs to be more palatable to TNF
No relevant Dekreitz, Thin or generalized fragments.
  - invalidate_grind_failures
  - clean source
  - replay relevant source in update mode

Will Source update remove stale records?  

General strategy : identify/annotate/clean/redo
 annotate as invalid, ie non cc prop `invalid`
   - grind failures
       cc or not cc? 
       replays are cc.
       other grind operations annotate main properties!
   - replay failures 
       * fail exit of replay dialog will annotate with replay grind_fail
         thus annotating grind failures is sufficient. 
   - orphans : at least source orphans.
 rm invalid records and links to them.
 deal with orphans
 recreate  

`invalid` is crucial property. This is only true marker for bad records.
Other properties may identify issues of concern and unresolved issues should cause
records to eventually be annotated as invalid.  

Should thins of invalid Dekreitzed be invalid ?

Maybe add consistent check for each table.
 - genning and genning exists and are not invalid and point to record.
   immediate completion exists
   not grind failures or other problemmatical annotations.

Bad
  - grind_fail
      * grinder annotates main prop list at failure exit of dialog
        don't see how these are removed if later replay works.
        presumption is if dialog fail exit, you are committed to making it invalid.
        but could clear at clean
  - replay fail :
      * cc replay property show bad replay after replay : not necessarily bad? use grind_fail.
      * failure exit of dialog annotates grind_fail on cc prop list 
  - orphan : when orig/source
      * orphaned thin and alpha records are maintained as long as they are not otherwise bad.
      * replayable orphaned records could possibly be adopted.
        But fttb orphans are routinely rm'd,
        since (unlikely genned record replays if genning does not).
        But looks like we're leaving dek orphans? And their genned. FTTB leave as is.
        Timing issue in that we may be delete source, and thus making deks orphans, but
          Ie if run invalidate_dekreitz_orphans prior to source_clean then deks of invalid
          source not orphans, but if after they are.
        But do invalidate siblings of invalidate siblings of invalid dek? ???

    ancestors of bad or has bad descendent.

replay/grind

verify :
 orig
 derivations : down pointers
 completions :
 index order
 index orphans : keys with no record
 


should not exist bad replay failure that are not also replay grind_fails
 - if didn't dialog fail exit then could happen

frag_invalidate_grind_failures finds grind_fails on both cc and main prop lists.

frag_invalidate_dekreitz_orphans
frag_invalidate_dekreitz : invalidates siblings of invalid dekreitzs.
frag_invalidate_thins : invalidates alphas of invalid thins +  thin ancestors
frag_invalidate_alpha : invalidates thins of invalid dekreitz + alpha ancestors
frag_source_clean : removes source records and source props of deks.
frag_dekreitz_clean : removes deks and cleans props in source the refd deks.
frag_thin_clean : removes thins from index and thin table
                  removes Thin cc props from Dekreitz records 

 cc `grind_fail` : invalid{grind:t,Top_replay,<obid>}
 `invalid` orphan:t
 `source` !Void()

  replay of source
    - update mode may orphan source records
    - may overwrite source records and orphan deks?
  replay of source table
    - replay can fail
  grind tnf/dekreitz failure
    - might prompt one to modify source proof which 
      then replay orphans/overwrites 

Cleanup orphaned source records after TNF fails.
  invalidate orphans
  remove invalids 
    - clean orig pointers of dekreitz records if they point at source.

 view_show ilist (frag_invalidate_source_orphans false `Standard_2_9`)
 view_show ilist (frag_source_clean false `Standard_2_9`)


Cleanup alpha grind fails :
 make grind_fail invalid then clean as usual
 ??

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

Authors: 

Contributors: RICH:t
              NUPRL:t

⋅

Home