Persist and restore deduction internal state

src/components/Dev/Explore.svelte

@@ -4,6 +4,11 @@
   import Log from './Log.svelte'
 
   const { spaces, properties, theorems, traits } = context()
+
+  function reset() {
+    localStorage.clear()
+    window.location.reload()
+  }
 </script>
 
 <table class="table">
@@ -25,15 +30,17 @@
       <td>{$traits.size}</td>
     </tr>
     <tr>
-      <th />
-      <td>
+      <td colspan="2">
         <Log>Log to Console</Log>
         <Link
           type="button"
           getProps={() => ({ class: 'btn btn-outline-dark' })}
           to="/dev/preview">
           Editor Preview
         </Link>
+        <button type="button" class="btn btn-outline-dark" on:click={reset}>
+          Reset
+        </button>
       </td>
     </tr>
   </tbody>

src/components/Status.svelte

@@ -13,7 +13,12 @@
     checked = state.checked.size
     total = state.all.size
 
-    progress = (checked * 100.0) / total
+    // Don't flicker a full bar if we're just hydrating a fully checked state
+    // from local storage.
+    const newProgress = (checked * 100.0) / total
+    if (progress || newProgress !== 100.0) {
+      progress = newProgress
+    }
 
     if (checked === total) {
       // Give the animation time to visually finish

src/stores/deduction.ts

@@ -1,4 +1,4 @@
-import { Readable, writable } from 'svelte/store'
+import { Readable, get, writable } from 'svelte/store'
 import { ImplicationIndex, Prover, disprove } from '@pi-base/core'
 import type { Proof } from '@pi-base/core/lib/Logic/Types'
 import * as F from '@pi-base/core/lib/Formula'
@@ -60,25 +60,41 @@ export function check(
   return proof.map((uid) => collection.find(uid)!)
 }
 
+function initialize(spaces: Collection<Space>): State {
+  return {
+    checked: new Set(),
+    all: new Set(spaces.all.map((s) => s.id)),
+  }
+}
+
 export function create(
+  initial: State | undefined,
   spaces: Readable<Collection<Space>>,
   traits: Readable<Traits>,
   theorems: Readable<Theorems>,
   addTraits: (traits: Trait[]) => void,
 ): Store {
-  const { set, subscribe, update } = writable<State>({
-    checked: new Set(),
-    all: new Set(read(spaces).all.map((s) => s.id)),
-  })
+  const store = writable<State>(initial || initialize(read(spaces)))
 
   function run() {
-    const ss = read(spaces).all
+    const allSpaces = read(spaces).all
     const implications = indexTheorems(read(theorems))
 
-    set({ checked: new Set(), all: new Set(ss.map((s) => s.id)) })
+    store.update((s) => ({
+      ...s,
+      all: new Set([...s.all, ...allSpaces.map((s) => s.id)]),
+    }))
+
+    const checked = read(store).checked
+    const unchecked: Space[] = []
+    allSpaces.forEach((s) => {
+      if (!checked.has(s.id)) {
+        unchecked.push(s)
+      }
+    })
 
-    eachTick(ss, (s: Space, halt: () => void) => {
-      update((state) => ({ ...state, checking: s.name }))
+    eachTick(unchecked, (s: Space, halt: () => void) => {
+      store.update((state) => ({ ...state, checking: s.name }))
 
       const map = new Map(
         read(traits)
@@ -89,7 +105,7 @@ export function create(
 
       const contradiction = prover.run()
       if (contradiction) {
-        update((s) => ({ ...s, contradiction }))
+        store.update((s) => ({ ...s, contradiction }))
         halt()
         return
       }
@@ -111,7 +127,7 @@ export function create(
 
       addTraits(newTraits)
 
-      update((state) => ({
+      store.update((state) => ({
         ...state,
         checked: new Set([...state.checked, s.id]),
       }))
@@ -121,11 +137,11 @@ export function create(
   theorems.subscribe(run)
 
   return {
-    subscribe,
+    subscribe: store.subscribe,
     run,
     checked(spaceId: number) {
       return subscribeUntil(
-        { subscribe },
+        store,
         (state) => state.checked.has(spaceId) || !!state.contradiction,
       )
     },

src/stores/index.ts

@@ -49,8 +49,13 @@ export function create(pre: Prestore, gateway: Gateway.Sync): Store {
   const traits = writable(new Traits())
   const source = Source.create()
   const sync = Sync.create(refresh, pre.sync)
-  const deduction = Deduction.create(spaces, traits, theorems, (added) =>
-    traits.update(($traits) => $traits.add(added)),
+
+  const deduction = Deduction.create(
+    pre.deduction,
+    spaces,
+    traits,
+    theorems,
+    (added) => traits.update(($traits) => $traits.add(added)),
   )
 
   function set(