From c96fe2d171f1d3c9b59992f7d0fb00775cae9243 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 27 Mar 2026 11:26:37 +0100 Subject: [PATCH 1/7] commit --- .../src/components/Properties/Show.svelte | 12 +++- .../src/components/Shared/LeanLink.svelte | 55 +++++++++++++++++++ .../viewer/src/components/Shared/index.ts | 1 + .../src/components/Theorems/Show.svelte | 4 +- 4 files changed, 70 insertions(+), 2 deletions(-) create mode 100644 packages/viewer/src/components/Shared/LeanLink.svelte diff --git a/packages/viewer/src/components/Properties/Show.svelte b/packages/viewer/src/components/Properties/Show.svelte index cc4eb43b..ddce9a9a 100644 --- a/packages/viewer/src/components/Properties/Show.svelte +++ b/packages/viewer/src/components/Properties/Show.svelte @@ -1,6 +1,14 @@ + + + +{#if loaded} +

+ {#if available} + + Formalisation available. + + {:else} + No formalisation available. + {/if} +

+{/if} diff --git a/packages/viewer/src/components/Shared/index.ts b/packages/viewer/src/components/Shared/index.ts index f7d893de..80d4cd27 100644 --- a/packages/viewer/src/components/Shared/index.ts +++ b/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' diff --git a/packages/viewer/src/components/Theorems/Show.svelte b/packages/viewer/src/components/Theorems/Show.svelte index 8f469ca8..21438e32 100644 --- a/packages/viewer/src/components/Theorems/Show.svelte +++ b/packages/viewer/src/components/Theorems/Show.svelte @@ -1,6 +1,6 @@ -

Property

+

+ Property + +

@@ -39,8 +42,6 @@ - - {#if tab === 'spaces'} diff --git a/packages/viewer/src/components/Shared/Icons/Lean.svelte b/packages/viewer/src/components/Shared/Icons/Lean.svelte new file mode 100644 index 00000000..4b501de4 --- /dev/null +++ b/packages/viewer/src/components/Shared/Icons/Lean.svelte @@ -0,0 +1,14 @@ + diff --git a/packages/viewer/src/components/Shared/Icons/index.ts b/packages/viewer/src/components/Shared/Icons/index.ts index 15267334..a56627a0 100644 --- a/packages/viewer/src/components/Shared/Icons/index.ts +++ b/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' diff --git a/packages/viewer/src/components/Shared/LeanLink.svelte b/packages/viewer/src/components/Shared/LeanLink.svelte index af8b42bb..6bcebc92 100644 --- a/packages/viewer/src/components/Shared/LeanLink.svelte +++ b/packages/viewer/src/components/Shared/LeanLink.svelte @@ -22,6 +22,7 @@ {#if loaded} -

- {#if available} + {#if available} +

- Formalisation available. + - {:else} - No formalisation available. - {/if} -

+
+ {/if} {/if} + + diff --git a/packages/viewer/src/components/Theorems/Show.svelte b/packages/viewer/src/components/Theorems/Show.svelte index 21438e32..9ddf4692 100644 --- a/packages/viewer/src/components/Theorems/Show.svelte +++ b/packages/viewer/src/components/Theorems/Show.svelte @@ -11,7 +11,10 @@ const tabs = ['converse', 'references'] as const -

Theorem

+

+ Theorem + +

@@ -25,8 +28,6 @@ - - {#if tab === 'converse'} From 3c8138212a09d5389a5de73d3c6c9101eb8dd205 Mon Sep 17 00:00:00 2001 From: Steven Clontz Date: Wed, 1 Apr 2026 15:04:45 -0500 Subject: [PATCH 3/7] Apply suggestion from @StevenClontz --- packages/viewer/src/components/Shared/Icons/Lean.svelte | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packages/viewer/src/components/Shared/Icons/Lean.svelte b/packages/viewer/src/components/Shared/Icons/Lean.svelte index 4b501de4..ab214268 100644 --- a/packages/viewer/src/components/Shared/Icons/Lean.svelte +++ b/packages/viewer/src/components/Shared/Icons/Lean.svelte @@ -3,7 +3,7 @@ height="20" viewBox="0 0 486 169" xmlns="http://www.w3.org/2000/svg" - stroke="auto" + stroke="#007bff" fill="transparent" stroke-width="10" > Date: Sun, 5 Apr 2026 05:14:21 +0200 Subject: [PATCH 4/7] small edit --- .../viewer/src/components/Dev/Explore.svelte | 17 +++++++++++++++++ .../src/components/Shared/LeanLink.svelte | 8 +++++++- 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/packages/viewer/src/components/Dev/Explore.svelte b/packages/viewer/src/components/Dev/Explore.svelte index ba6487a8..a88d7413 100644 --- a/packages/viewer/src/components/Dev/Explore.svelte +++ b/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')

Entities

@@ -52,5 +57,17 @@ + + + + + + diff --git a/packages/viewer/src/components/Shared/LeanLink.svelte b/packages/viewer/src/components/Shared/LeanLink.svelte index 6bcebc92..7b267781 100644 --- a/packages/viewer/src/components/Shared/LeanLink.svelte +++ b/packages/viewer/src/components/Shared/LeanLink.svelte @@ -23,10 +23,12 @@ -{#if loaded} +{#if enabled && loaded} {#if available}
From 2b8766a1c5b2405add264e0ae99f56e910cdd426 Mon Sep 17 00:00:00 2001 From: Batixx Date: Sun, 5 Apr 2026 05:14:34 +0200 Subject: [PATCH 5/7] adopt suggestion --- .../src/components/Shared/Icons/Lean.svelte | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/packages/viewer/src/components/Shared/Icons/Lean.svelte b/packages/viewer/src/components/Shared/Icons/Lean.svelte index ab214268..bc39924d 100644 --- a/packages/viewer/src/components/Shared/Icons/Lean.svelte +++ b/packages/viewer/src/components/Shared/Icons/Lean.svelte @@ -1,14 +1,14 @@ - + From e06188de146d63fedff817d4375bf5966bcba457 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Wed, 8 Apr 2026 22:30:28 +0200 Subject: [PATCH 6/7] fix capitalization --- packages/viewer/src/components/Shared/LeanLink.svelte | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/packages/viewer/src/components/Shared/LeanLink.svelte b/packages/viewer/src/components/Shared/LeanLink.svelte index 7b267781..742ad648 100644 --- a/packages/viewer/src/components/Shared/LeanLink.svelte +++ b/packages/viewer/src/components/Shared/LeanLink.svelte @@ -2,8 +2,8 @@ const repo = 'felixpernegger/pibase-lean' const directories: Record>> = { - property: fetchDirectory('PibaseLean/Properties'), - theorem: fetchDirectory('PibaseLean/Theorems'), + property: fetchDirectory('PiBaseLean/Properties'), + theorem: fetchDirectory('PiBaseLean/Theorems'), } async function fetchDirectory(path: string): Promise> { @@ -35,7 +35,7 @@ $: folderName = kind === 'property' ? `P${id}` : `T${id}` $: file = kind === 'property' ? 'Defs.lean' : 'Theorem.lean' $: basePath = - kind === 'property' ? 'PibaseLean/Properties' : 'PibaseLean/Theorems' + kind === 'property' ? 'PiBaseLean/Properties' : 'PiBaseLean/Theorems' $: href = `https://github.com/${repo}/blob/master/${basePath}/${folderName}/${file}` onMount(async () => { From 63a3e41da88ee96fabf6670b0650b73014cea0cf Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 24 Apr 2026 01:42:52 +0200 Subject: [PATCH 7/7] fix --- .../viewer/src/components/Dev/Explore.svelte | 16 +--- .../src/components/Shared/LeanLink.svelte | 31 +++---- .../src/components/Traits/Related.svelte | 7 +- packages/viewer/src/stores/settings.test.ts | 85 +++++++++++++++++++ packages/viewer/src/stores/settings.ts | 25 ++++++ 5 files changed, 131 insertions(+), 33 deletions(-) create mode 100644 packages/viewer/src/stores/settings.test.ts create mode 100644 packages/viewer/src/stores/settings.ts diff --git a/packages/viewer/src/components/Dev/Explore.svelte b/packages/viewer/src/components/Dev/Explore.svelte index a88d7413..4d774614 100644 --- a/packages/viewer/src/components/Dev/Explore.svelte +++ b/packages/viewer/src/components/Dev/Explore.svelte @@ -1,20 +1,10 @@

Entities

@@ -52,7 +42,7 @@ @@ -62,7 +52,7 @@
diff --git a/packages/viewer/src/components/Traits/Related.svelte b/packages/viewer/src/components/Traits/Related.svelte index 8e1c4d2c..d3685f7d 100644 --- a/packages/viewer/src/components/Traits/Related.svelte +++ b/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 @@ diff --git a/packages/viewer/src/stores/settings.test.ts b/packages/viewer/src/stores/settings.test.ts new file mode 100644 index 00000000..b86db960 --- /dev/null +++ b/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 = {} + 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) + }) +}) diff --git a/packages/viewer/src/stores/settings.ts b/packages/viewer/src/stores/settings.ts new file mode 100644 index 00000000..f0a51117 --- /dev/null +++ b/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 = defaultStorage, +) { + const store = writable( + 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)