Aim

packages/core/src/Bundle.ts

@@ -17,6 +17,9 @@ export type Bundle = {
  spaces: Map<Id, Space>
  traits: Map<Id, Trait<Id>>
  theorems: Map<Id, Theorem>
+ lean?: {
+ properties: { id: string; module: string }[]
+ }
  version: Version
 }
 
@@ -26,6 +29,16 @@ export const serializedSchema = z.object({
  theorems: z.array(theoremSchema),
  traits: z.array(traitSchema(z.string())),
  version: z.object({ ref: z.string(), sha: z.string() }),
+ lean: z
+ .object({
+ properties: z.array(
+ z.object({
+ id: z.string(),
+ module: z.string(),
+ }),
+ ),
+ })
+ .optional(),
 })
 
 export type Serialized = z.infer<typeof serializedSchema>
@@ -41,14 +54,16 @@ export function serialize(bundle: Bundle): Serialized {
 }
 
 export function deserialize(data: unknown): Bundle {
- const serialized = serializedSchema.parse(data)
+ const { properties, spaces, theorems, traits, version, lean } =
+ serializedSchema.parse(data)
 
  return {
- properties: indexBy(serialized.properties, p => p.uid),
- spaces: indexBy(serialized.spaces, s => s.uid),
- theorems: indexBy(serialized.theorems, t => t.uid),
- traits: indexBy(serialized.traits, traitId),
- version: serialized.version,
+ properties: indexBy(properties, p => p.uid),
+ spaces: indexBy(spaces, s => s.uid),
+ theorems: indexBy(theorems, t => t.uid),
+ traits: indexBy(traits, traitId),
+ lean,
+ version,
  }
 }
 

packages/core/src/Property.ts

@@ -5,6 +5,7 @@ export const propertySchema = z.intersection(
  z.object({
  name: z.string(),
  aliases: z.array(z.string()),
+ mathlib: z.string().optional(),
  }),
  recordSchema,
 )

packages/viewer/package.json

@@ -20,12 +20,14 @@
  "@pi-base/core": "workspace:*",
  "@sentry/browser": "^7.75.1",
  "bootstrap": "^4.6.2",
+ "d3": "^7.8.5",
  "debug": "^4.3.4",
  "fromnow": "^3.0.1",
  "fuse.js": "^6.6.2",
  "hast-to-hyperscript": "^10.0.3",
  "hyperscript": "^2.0.2",
  "jquery": "1.12.4",
+ "katex": "^0.16.9",
  "rehype-katex": "^6.0.3",
  "remark-rehype": "^10.1.0",
  "unified": "^10.1.2",
@@ -37,6 +39,7 @@
  "@sveltejs/kit": "^1.27.1",
  "@sveltejs/vite-plugin-svelte": "^2.4.6",
  "@tsconfig/svelte": "^3.0.0",
+ "@types/d3": "^7.4.3",
  "@types/debug": "^4.1.10",
  "@types/hyperscript": "0.0.6",
  "@types/katex": "^0.16.5",

packages/viewer/public/global.css

@@ -46,3 +46,14 @@
 .description {
  margin-bottom: 1rem;
 }
+
+.links line {
+ stroke: #999;
+ stroke-opacity: 0.6;
+}
+
+.nodes circle {
+ stroke: #fff;
+ stroke-width: 1.5px;
+}
+

packages/viewer/src/app.html

@@ -4,25 +4,25 @@
  <meta charset="utf-8" />
  <meta name="viewport" content="width=device-width" />
 
-  <title>π-Base</title>
+ <title>π-Base</title>
 
-  <meta name="author" content="James Dabbs" />
-  <meta name="description"
-   content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
-  <meta property="og:type" content="website" />
-  <meta property="og:site_name" content="π-Base" />
-  <meta property="og:url" name="twitter:url" content="https://topology.pi-base.org" />
-  <meta property="og:title" name="twitter:title" content="π-Base" />
-  <meta property="og:description" name="twitter:description"
-   content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
-  <meta property="og:image" content="%sveltekit.assets%/pi-base.png" />
-  <meta name="twitter:site" content="π-Base" />
-  <meta name="twitter:creator" content="@jamesdabbs" />
+ <meta name="author" content="James Dabbs" />
+ <meta name="description"
+ content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
+ <meta property="og:type" content="website" />
+ <meta property="og:site_name" content="π-Base" />
+ <meta property="og:url" name="twitter:url" content="https://topology.pi-base.org" />
+ <meta property="og:title" name="twitter:title" content="π-Base" />
+ <meta property="og:description" name="twitter:description"
+ content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
+ <meta property="og:image" content="%sveltekit.assets%/pi-base.png" />
+ <meta name="twitter:site" content="π-Base" />
+ <meta name="twitter:creator" content="@jamesdabbs" />
 
  <link rel="icon" href="%sveltekit.assets%/favicon.ico" />
 
-  <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-Xi8rHCmBmhbuyyhbI88391ZKP2dmfnOl4rT9ZfRI7mLTdk1wblIUnrIq35nqwEvC" crossorigin="anonymous">
-  <link rel='stylesheet' href='/global.css'>
+ <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-Xi8rHCmBmhbuyyhbI88391ZKP2dmfnOl4rT9ZfRI7mLTdk1wblIUnrIq35nqwEvC" crossorigin="anonymous">
+ <link rel='stylesheet' href='/global.css'>
 
  %sveltekit.head%
  </head>

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

@@ -1,14 +1,28 @@
 <script lang="ts">
  import type { Property } from 'src/models'
- import { Aliases, References, Tabs, Title, Typeset } from '../Shared'
+ import {
+ Aliases,
+ Icons,
+ Link,
+ References,
+ Tabs,
+ Title,
+ Typeset,
+ } from '../Shared'
  import Spaces from './Spaces.svelte'
  import Theorems from './Theorems.svelte'
+ import Check from '../Shared/Icons/Check.svelte'
 
  export let property: Property
  export let tab: 'spaces' | 'theorems' | 'references'
  export let rel: string | undefined = undefined
 
  const tabs = ['spaces', 'theorems', 'references'] as const
+
+ function leanUrl({ id, module }: { id: string; module: string }) {
+ const path = module.replaceAll('.', '/')
+ return `https://leanprover-community.github.io/mathlib4_docs/${path}.html#${id}`
+ }
 </script>
 
 <Title title={property.name} />
@@ -21,6 +35,16 @@
 </h1>
 
 <section class="description">
+ {#if property?.lean}
+ <p>
+ <Icons.Robot />
+ <a href={leanUrl(property.lean)} target="_blank">
+ <code>{property.lean.id}</code>
+ in
+ <code>{property.lean.module}</code>
+ </a>
+ </p>
+ {/if}
  <Typeset body={property.description} />
 </section>
 

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

@@ -13,7 +13,7 @@
 <div class="text-center p-2">
  <small>
  Cite as:
- <span class="text-muted">
+ <span class="citation text-muted">
  The pi-Base Community.
  {#if title}
  <cite>{title}.</cite>
@@ -32,3 +32,13 @@
  <CopyButton text={markdown}>Markdown Link</CopyButton>
  </small>
 </div>
+
+<style>
+ .p-2 {
+ overflow: hidden;
+ }
+
+ .p-2:hover {
+ overflow: visible;
+ }
+</style>

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

@@ -1,11 +1,14 @@
 <script lang="ts">
- import type { Theorem } from '@/models'
+ import type { Property, Theorem } from '@/models'
  import { Formula, Link } from '../Shared'
+ import type { Readable } from 'svelte/store'
 
  export let theorems: Theorem[] = []
+ export let small = false
+ export let selected: Readable<Theorem | Property> | undefined = undefined
 </script>
 
-<table class="table">
+<table class="table" class:table-sm={small}>
  <thead>
  <tr>
  <th>Id</th>
@@ -15,7 +18,7 @@
  </thead>
  <tbody>
  {#each theorems as theorem (theorem.id)}
- <tr>
+ <tr class:table-warning={$selected === theorem}>
  <td>
  <Link.Theorem {theorem} />
  </td>