feat: Lean linkage

packages/viewer/src/components/Dev/Explore.svelte

@@ -1,15 +1,10 @@
 <script lang="ts">
   import context from '@/context'
   import Log from './Log.svelte'
-  import { defaultStorage } from '@/repositories'
   import { reset } from '@/util'
+  import { showLeanLinks, showRedundancy } from '@/stores/settings'
 
   const { spaces, properties, theorems, traits } = context()
-
-  let showRedundancy = defaultStorage.getItem('showRedundancy') !== null
-  $: showRedundancy
-    ? defaultStorage.setItem('showRedundancy', 'show')
-    : defaultStorage.removeItem('showRedundancy')
 </script>
 
 <h4>Entities</h4>
@@ -47,10 +42,22 @@
         <input
           id="redundancyCheckbox"
           type="checkbox"
-          bind:checked={showRedundancy}
+          bind:checked={$showRedundancy}
         />
         <label for="redundancyCheckbox"> Show redundancies in tables </label>
       </td>
     </tr>
+    <tr>
+      <td colspan="2">
+        <input
+          id="leanLinksCheckbox"
+          type="checkbox"
+          bind:checked={$showLeanLinks}
+        />
+        <label for="leanLinksCheckbox">
+          Show Lean formalisation links (experimental)
+        </label>
+      </td>
+    </tr>
   </tbody>
 </table>

packages/viewer/src/components/Properties/Show.svelte

@@ -1,6 +1,14 @@
 <script lang="ts">
   import type { Property } from '@/models'
-  import { Aliases, Link, References, Source, Tabs, Typeset } from '../Shared'
+  import {
+    Aliases,
+    LeanLink,
+    Link,
+    References,
+    Source,
+    Tabs,
+    Typeset,
+  } from '../Shared'
   import Spaces from './Spaces.svelte'
   import Theorems from './Theorems.svelte'
 
@@ -11,7 +19,10 @@
   const tabs = ['theorems', 'spaces', 'references'] as const
 </script>
 
-<h3>Property <Link.Property {property} content="idLong" /></h3>
+<h3>
+  Property <Link.Property {property} content="idLong" />
+  <LeanLink kind="property" id={property.id} />
+</h3>
 
 <h1>
   <Typeset body={property.name} />

packages/viewer/src/components/Shared/Icons/Lean.svelte

@@ -0,0 +1,14 @@
+<svg
+  width="70"
+  height="20"
+  viewBox="0 0 486 169"
+  xmlns="http://www.w3.org/2000/svg"
+  stroke="#007bff"
+  fill="transparent"
+  stroke-width="10"
+  ><path
+    d="M206.333 5.67949H105.667M206.333 5.67949L243.25 84.5M206.333 5.67949V84.5M243.25 84.5H317.549M243.25 84.5L279.667 163.321L280.889 163.318L317.549 84.5M206.333 84.5V163.321H5V5M206.333 84.5H105.667M317.549 84.5L353 5.67949M353 5.67949V164M353 5.67949H353.667L480.333 163.454H481V5"
+    stroke-linecap="round"
+    stroke-linejoin="round"
+  /></svg
+>

packages/viewer/src/components/Shared/Icons/index.ts

@@ -1,6 +1,7 @@
 export { default as Branch } from './Branch.svelte'
 export { default as Check } from './Check.svelte'
 export { default as Dice } from './Dice.svelte'
+export { default as Lean } from './Lean.svelte'
 export { default as Question } from './Question.svelte'
 export { default as Repeat } from './Repeat.svelte'
 export { default as Search } from './Search.svelte'

packages/viewer/src/components/Shared/LeanLink.svelte

@@ -0,0 +1,80 @@
+<script context="module" lang="ts">
+  const repo = 'felixpernegger/pibase-lean'
+
+  const cache: Record<string, Promise<Set<string>>> = {}
+
+  function getDirectory(kind: 'property' | 'theorem'): Promise<Set<string>> {
+    const path =
+      kind === 'property' ? 'PiBaseLean/Properties' : 'PiBaseLean/Theorems'
+    if (!cache[kind]) {
+      cache[kind] = fetchDirectory(path)
+    }
+    return cache[kind]
+  }
+
+  async function fetchDirectory(path: string): Promise<Set<string>> {
+    try {
+      const res = await fetch(
+        `https://api.github.com/repos/${repo}/contents/${path}`,
+      )
+      if (!res.ok) return new Set()
+      const entries: { name: string }[] = await res.json()
+      return new Set(entries.map(e => e.name))
+    } catch {
+      return new Set()
+    }
+  }
+</script>
+
+<script lang="ts">
+  import { Icons } from '@/components/Shared'
+  import { showLeanLinks } from '@/stores/settings'
+
+  export let kind: 'property' | 'theorem'
+  export let id: number
+
+  let loaded = false
+  let available = false
+
+  $: folderName = kind === 'property' ? `P${id}` : `T${id}`
+  $: file = kind === 'property' ? 'Defs.lean' : 'Theorem.lean'
+  $: basePath =
+    kind === 'property' ? 'PiBaseLean/Properties' : 'PiBaseLean/Theorems'
+  $: href = `https://github.com/${repo}/blob/master/${basePath}/${folderName}/${file}`
+
+  $: if ($showLeanLinks && !loaded) {
+    getDirectory(kind).then(ids => {
+      available = ids.has(folderName)
+      loaded = true
+    })
+  }
+</script>
+
+{#if $showLeanLinks && loaded}
+  {#if available}
+    <div>
+      <a {href} target="_blank" rel="noopener noreferrer">
+        <Icons.Lean />
+      </a>
+    </div>
+  {/if}
+{/if}
+
+<style>
+  div {
+    display: inline-block;
+    border: 1px solid white;
+    padding: 2px;
+  }
+  div:hover {
+    background: #f6fafe;
+    border: 1px solid #e0edfb;
+    border-radius: 5px;
+  }
+  a {
+    padding: 5px;
+    display: flex;
+    align-items: center;
+    justify-content: center;
+  }
+</style>

packages/viewer/src/components/Shared/index.ts

@@ -5,6 +5,7 @@ export { default as Aliases } from './Aliases.svelte'
 export { default as Filter } from './Filter.svelte'
 export { default as Formula } from './Formula.svelte'
 export { default as Id } from './Id.svelte'
+export { default as LeanLink } from './LeanLink.svelte'
 export { default as Link } from './Link'
 export { default as Loading } from './Loading.svelte'
 export { default as NotFound } from './NotFound.svelte'

packages/viewer/src/components/Theorems/Show.svelte

@@ -1,6 +1,6 @@
 <script lang="ts">
   import type { Theorem } from '@/models'
-  import { Link, References, Tabs, Source, Typeset } from '../Shared'
+  import { LeanLink, Link, References, Tabs, Source, Typeset } from '../Shared'
   import Name from './Name.svelte'
   import Converse from './Converse.svelte'
 
@@ -11,7 +11,10 @@
   const tabs = ['converse', 'references'] as const
 </script>
 
-<h3>Theorem <Link.Theorem {theorem} content="idLong" /></h3>
+<h3>
+  Theorem <Link.Theorem {theorem} content="idLong" />
+  <LeanLink kind="theorem" id={theorem.id} />
+</h3>
 
 <h1>
   <Name {theorem} />

packages/viewer/src/components/Traits/Related.svelte

@@ -5,8 +5,8 @@
   import context from '@/context'
   import type { Property, Space, Trait, Traits } from '@/models'
   import FilterButtons from './FilterButtons.svelte'
-  import { defaultStorage } from '@/repositories'
   import { writable } from 'svelte/store'
+  import { showRedundancy } from '@/stores/settings'
   import urlSearchParam from '@/stores/urlSearchParam'
   import { checkIfRedundant } from '@/stores/deduction'
 
@@ -21,8 +21,6 @@
   let filterMode: 'all' | 'known' | 'asserted' | 'true' | 'false' | 'missing'
   filterMode = 'known'
 
-  let showRedundancy = defaultStorage.getItem('showRedundancy') != null
-
   $: all = related($traits)
   // all has type [Space, Property, Trait][]
   // we need to index names in different positions depending on which kind we
@@ -109,10 +107,9 @@
           <Link.Trait {space} {property}>
             <SourceIcon
               value={trait?.asserted}
-              redundant={showRedundancy &&
+              redundant={$showRedundancy &&
                 trait?.asserted &&
                 checkIfRedundant(space, property, $theorems, $traits).redundant}
-              icon="user"
             />
           </Link.Trait>
         </td>

packages/viewer/src/stores/settings.test.ts

@@ -0,0 +1,85 @@
+import { beforeEach, describe, expect, it } from 'vitest'
+import { get } from 'svelte/store'
+import { persistedBoolean, showLeanLinks, showRedundancy } from './settings'
+
+function mockStorage() {
+  const data: Record<string, string> = {}
+  return {
+    data,
+    getItem: (key: string) => data[key] ?? null,
+    setItem: (key: string, value: string) => {
+      data[key] = value
+    },
+    removeItem: (key: string) => {
+      delete data[key]
+    },
+  }
+}
+
+describe('persistedBoolean', () => {
+  it('defaults to the given default value when storage is empty', () => {
+    const storage = mockStorage()
+    const store = persistedBoolean('flag', false, storage)
+    expect(get(store)).toBe(false)
+  })
+
+  it('initializes to true when the key already exists in storage', () => {
+    const storage = mockStorage()
+    storage.data['flag'] = 'show'
+    const store = persistedBoolean('flag', false, storage)
+    expect(get(store)).toBe(true)
+  })
+
+  it('writes to storage when set to true', () => {
+    const storage = mockStorage()
+    const store = persistedBoolean('flag', false, storage)
+    store.set(true)
+    expect(storage.data['flag']).toBe('show')
+  })
+
+  it('removes from storage when set to false', () => {
+    const storage = mockStorage()
+    storage.data['flag'] = 'show'
+    const store = persistedBoolean('flag', true, storage)
+    store.set(false)
+    expect(storage.data['flag']).toBeUndefined()
+  })
+
+  it('reflects updates via subscribe', () => {
+    const storage = mockStorage()
+    const store = persistedBoolean('flag', false, storage)
+    const values: boolean[] = []
+    store.subscribe(v => values.push(v))
+
+    store.set(true)
+    store.set(false)
+
+    expect(values).toEqual([false, true, false])
+  })
+})
+
+describe('showLeanLinks', () => {
+  it('defaults to false', () => {
+    expect(get(showLeanLinks)).toBe(false)
+  })
+
+  it('can be toggled', () => {
+    showLeanLinks.set(true)
+    expect(get(showLeanLinks)).toBe(true)
+    showLeanLinks.set(false)
+    expect(get(showLeanLinks)).toBe(false)
+  })
+})
+
+describe('showRedundancy', () => {
+  it('defaults to false', () => {
+    expect(get(showRedundancy)).toBe(false)
+  })
+
+  it('can be toggled', () => {
+    showRedundancy.set(true)
+    expect(get(showRedundancy)).toBe(true)
+    showRedundancy.set(false)
+    expect(get(showRedundancy)).toBe(false)
+  })
+})

packages/viewer/src/stores/settings.ts

@@ -0,0 +1,25 @@
+import { writable } from 'svelte/store'
+import { defaultStorage } from '@/repositories'
+
+export function persistedBoolean(
+  key: string,
+  defaultValue: boolean,
+  storage: Pick<Storage, 'getItem' | 'setItem' | 'removeItem'> = defaultStorage,
+) {
+  const store = writable<boolean>(
+    storage.getItem(key) !== null ? true : defaultValue,
+  )
+
+  store.subscribe(v => {
+    if (v) {
+      storage.setItem(key, 'show')
+    } else {
+      storage.removeItem(key)
+    }
+  })
+
+  return store
+}
+
+export const showLeanLinks = persistedBoolean('showLeanLinks', false)
+export const showRedundancy = persistedBoolean('showRedundancy', false)