feat: Lean linkage

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

@@ -10,6 +10,11 @@
   $: showRedundancy
     ? defaultStorage.setItem('showRedundancy', 'show')
     : defaultStorage.removeItem('showRedundancy')
+
+  let showLeanLinks = defaultStorage.getItem('showLeanLinks') !== null
+  $: showLeanLinks
+    ? defaultStorage.setItem('showLeanLinks', 'show')
+    : defaultStorage.removeItem('showLeanLinks')
 </script>
 
 <h4>Entities</h4>
@@ -52,5 +57,17 @@
         <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,79 @@
+<script context="module" lang="ts">
+  const repo = 'felixpernegger/pibase-lean'
+
+  const directories: Record<string, Promise<Set<string>>> = {
+    property: fetchDirectory('PiBaseLean/Properties'),
+    theorem: fetchDirectory('PiBaseLean/Theorems'),
+  }
+
+  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 { onMount } from 'svelte'
+  import { Icons } from '@/components/Shared'
+  import { defaultStorage } from '@/repositories'
+
+  export let kind: 'property' | 'theorem'
+  export let id: number
+
+  let enabled = defaultStorage.getItem('showLeanLinks') !== null
+  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}`
+
+  onMount(async () => {
+    if (!enabled) {
+      loaded = true
+      return
+    }
+    const ids = await directories[kind]
+    available = ids.has(folderName)
+    loaded = true
+  })
+</script>
+
+{#if enabled && 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} />