From 034ac233c90d2476237411e9f6e31110cefb5a67 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 5 Jun 2026 17:57:25 -0400 Subject: [PATCH 1/3] Add 'Can I Trust This Code?' button, and setting to turn off a warning that I haven't added yet --- client/src/css/Navigation.css | 4 +++ client/src/navigation/NavButton.tsx | 11 +++++++- client/src/navigation/Navigation.tsx | 37 ++++++++++++++++++++++----- client/src/settings/SettingsPopup.tsx | 20 ++++++++++++++- client/src/settings/settings-atoms.ts | 14 ++++++++++ 5 files changed, 78 insertions(+), 8 deletions(-) diff --git a/client/src/css/Navigation.css b/client/src/css/Navigation.css index dc155427..ad93cdc0 100644 --- a/client/src/css/Navigation.css +++ b/client/src/css/Navigation.css @@ -78,6 +78,10 @@ nav select { padding-bottom: 0.6rem; } +nav .nav-link.disabled { + cursor: not-allowed; +} + /* Zulip logo (instead of font-awesome icon) */ nav .nav-link svg { width: 1.4rem; diff --git a/client/src/navigation/NavButton.tsx b/client/src/navigation/NavButton.tsx index a7a1920e..09dc99cf 100644 --- a/client/src/navigation/NavButton.tsx +++ b/client/src/navigation/NavButton.tsx @@ -10,6 +10,7 @@ export function NavButton({ title, onClick = () => {}, href = undefined, + disabled = false, }: { icon?: IconDefinition iconElement?: JSX.Element @@ -17,11 +18,19 @@ export function NavButton({ title?: string onClick?: MouseEventHandler href?: string + disabled?: boolean }) { // note: it seems that we can just leave the `target="_blank"` and it has no // effect on links without a `href`. If not, add `if (href)` statement here... return ( - + e.preventDefault() : onClick} + href={href!} + target="_blank" + > {iconElement ?? } {text} ) diff --git a/client/src/navigation/Navigation.tsx b/client/src/navigation/Navigation.tsx index f6100f0a..d30a5a27 100644 --- a/client/src/navigation/Navigation.tsx +++ b/client/src/navigation/Navigation.tsx @@ -1,7 +1,13 @@ import '../css/Modal.css' import '../css/Navigation.css' -import { faArrowRotateRight, faCode, faInfoCircle, faEye } from '@fortawesome/free-solid-svg-icons' +import { + faArrowRotateRight, + faCode, + faEye, + faHandshake, + faInfoCircle, +} from '@fortawesome/free-solid-svg-icons' import { faArrowUpRightFromSquare, faBars, @@ -15,11 +21,12 @@ import { faXmark, } from '@fortawesome/free-solid-svg-icons' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { useAtom } from 'jotai' +import { useAtom, useAtomValue, useSetAtom } from 'jotai' import { ChangeEvent, Dispatch, SetStateAction, useState } from 'react' import { lean4webConfig } from '../../config' import ZulipIcon from '../assets/zulip.svg' +import { useNavBar } from '../context/NavBarContext' import { codeAtom } from '../editor/code-atoms' import ImpressumPopup from '../Popups/Impressum' import LoadUrlPopup from '../Popups/LoadUrl' @@ -30,12 +37,11 @@ import { mobileAtom } from '../settings/settings-atoms' import { SettingsPopup } from '../settings/SettingsPopup' import { setImportUrlAndProjectAtom } from '../store/import-atoms' import { currentProjectAtom, projectsAtom, visibleProjectsAtom } from '../store/project-atoms' +import { urlArgsStableAtom } from '../store/url-atoms' import { save } from '../utils/SaveToFile' import { Dropdown } from './Dropdown' import { NavButton } from './NavButton' -import { useNavBar } from '../context/NavBarContext' - /** The menu items either appearing inside the dropdown or outside */ function FlexibleMenu({ isInDropdown = false, @@ -58,8 +64,12 @@ function FlexibleMenu({ setLoadUrlOpen: Dispatch> setLoadZulipOpen: Dispatch> }) { - const [, setImportUrlAndProject] = useAtom(setImportUrlAndProjectAtom) - const [{ data: projects }] = useAtom(projectsAtom) + const setImportUrlAndProject = useSetAtom(setImportUrlAndProjectAtom) + const { data: projects } = useAtomValue(projectsAtom) + const urlArgs = useAtomValue(urlArgsStableAtom) + const code = useAtomValue(codeAtom) + const isUsingUrlCode = !!urlArgs?.url + const loadFileFromDisk = (event: ChangeEvent) => { console.debug('Loading file from disk') const fileToLoad = event.target.files![0] @@ -141,6 +151,21 @@ function FlexibleMenu({ }} /> + { + window.location.assign('https://comparator.live.lean-lang.org/' + window.location.hash) + }} + /> ) } diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index a386ab5d..dafb35eb 100644 --- a/client/src/settings/SettingsPopup.tsx +++ b/client/src/settings/SettingsPopup.tsx @@ -6,7 +6,7 @@ import { useState } from 'react' import { Popup } from '../navigation/Popup' import { shallowEqualSubset } from '../utils/shallowEqual' -import { settingsAtom } from './settings-atoms' +import { localOnlySettingsAtom, settingsAtom } from './settings-atoms' import type { MobileValues, Theme } from './settings-types' import { defaultSettings, Settings } from './settings-types' @@ -21,6 +21,7 @@ export function SettingsPopup({ }) { const [settings, applySettings] = useAtom(settingsAtom) const [newSettings, setNewSettings] = useState(settings) + const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingsAtom) function updateSetting(key: K, value: Settings[K]) { setNewSettings((prev) => ({ ...prev, [key]: value })) @@ -198,6 +199,23 @@ export function SettingsPopup({ onClick={() => applySettings(newSettings)} />

+

Local Settings

+

+ These settings are always preserved in the browser's local storage. +

+

+ { + setLocalOnlySettings({ + ...localOnlySettings, + ignoreComparatorWarning: !localOnlySettings.ignoreComparatorWarning, + }) + }} + checked={!!localOnlySettings.ignoreComparatorWarning} + /> + +

) diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts index a777f43a..4d1e6a6c 100644 --- a/client/src/settings/settings-atoms.ts +++ b/client/src/settings/settings-atoms.ts @@ -13,6 +13,20 @@ const settingsStoreAtom = atomWithStorage('lean4web:setting getOnInit: true, }) +interface PartialLocalOnlyUserSettings { + ignoreComparatorWarning?: boolean +} + +/** Settings always stored on localstorage, never in the URL */ +export const localOnlySettingsAtom = atomWithStorage( + 'lean4web:local-settings', + {}, + undefined, + { + getOnInit: true, + }, +) + /** The settings which are set in the searchParams of the opened URL */ const settingsUrlAtom = atom( (get) => { From 9d5d459e68143f800b90a6fe461b55ae5c3adb1c Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 8 Jun 2026 17:57:30 -0400 Subject: [PATCH 2/3] Configurable companion-site, trigger warning for untrusted code --- client/config.tsx | 2 + client/src/api/config-types.ts | 9 ++ client/src/css/Navigation.css | 74 ++++++++++++++++ client/src/navigation/NavButton.tsx | 5 +- client/src/navigation/Navigation.tsx | 121 +++++++++++++++++++++++---- 5 files changed, 193 insertions(+), 18 deletions(-) diff --git a/client/config.tsx b/client/config.tsx index 0b4ae72d..ff2b1fb4 100644 --- a/client/config.tsx +++ b/client/config.tsx @@ -5,4 +5,6 @@ export const lean4webConfig: LeanWebConfig = { serverCountry: "Germany", contactDetails: null, impressum: null, + comparator: "https://comparator.live.lean-lang.org/", + comparatorSafeList: ["lean-lang.org", /^.*\.lean-lang\.org$/], }; diff --git a/client/src/api/config-types.ts b/client/src/api/config-types.ts index 7f05a165..27ddbfdf 100644 --- a/client/src/api/config-types.ts +++ b/client/src/api/config-types.ts @@ -13,4 +13,13 @@ export type LeanWebConfig = { * (example: `<>

vat number: 000

<>`) */ impressum: JSX.Element | null + /** Base href for a comparator live deployment that encourages the verification of proofs from untrusted sources. + * If `null`, the "Can I Trust This Proof?" button will be hidden. + * (example: `"https://comparator.live.lean-lang.org/"`) + */ + comparator: string | null + /** URLs to safelist so that they do not prompt a popup highlighting the "Can I Trust This Proof?" button. + * Ignored if `comparator` option is `null`. + */ + comparatorSafeList: (string | RegExp)[] | null } diff --git a/client/src/css/Navigation.css b/client/src/css/Navigation.css index ad93cdc0..56b3d98f 100644 --- a/client/src/css/Navigation.css +++ b/client/src/css/Navigation.css @@ -152,3 +152,77 @@ nav select:hover { font-style: italic; color: var(--vscode-textLink-foreground); } + +.comparator-warning { + max-width: 290px; + color: var(--vscode-editorHoverWidget-foreground); + background-color: var(--comparator-warning-bg); + font-size: 90%; + padding: 0.9em 1em; + box-shadow: 0 0.2rem 0.6rem 0 var(--vscode-widget-shadow); + border: 1px solid var(--vscode-editorHoverWidget-border); + border-radius: 0.4em; + position: relative; +} + +.comparator-warning.dark { + --comparator-warning-bg: oklch(0.2264 0.1066 0); +} +.comparator-warning.light { + --comparator-warning-bg: oklch(0.9581 0.0293 0); +} +.comparator-warning.cobalt { + --comparator-warning-bg: oklch(0.2981 0.1382 0); +} + +.comparator-warning button.comparator-warning-close { + float: right; + font-size: 1.6em; + cursor: pointer; + padding-top: 0.1em; + border: none; + background: none; + color: inherit; + margin: 0; +} +.comparator-warning button.comparator-warning-close:hover { + color: var(--vscode-inputOption-activeForeground); +} + +.comparator-warning p { + margin: 0 0 0.6em; +} + +.comparator-warning-arrow { + position: absolute; + width: 1em; + height: 1em; + margin-top: -0.5em; + top: 0; +} + +.comparator-warning-arrow::before { + content: ''; + display: block; + width: 100%; + height: 100%; + background-color: var(--comparator-warning-bg); + border: 1px solid var(--vscode-editorHoverWidget-border); + transform: rotate(45deg); + border-right: none; + border-bottom: none; +} + +.comparator-warning-perma-dismiss { + padding: 0; + background: none; + border: none; + cursor: pointer; + font-size: inherit; + color: var(--vscode-textLink-foreground); + font-weight: bold; +} + +.comparator-warning-perma-dismiss:hover { + text-decoration: underline; +} diff --git a/client/src/navigation/NavButton.tsx b/client/src/navigation/NavButton.tsx index 09dc99cf..cc1c6321 100644 --- a/client/src/navigation/NavButton.tsx +++ b/client/src/navigation/NavButton.tsx @@ -1,6 +1,6 @@ import { IconDefinition } from '@fortawesome/free-solid-svg-icons' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { JSX, MouseEventHandler } from 'react' +import { JSX, MouseEventHandler, Ref } from 'react' /** A button to appear in the hamburger menu or to navigation bar. */ export function NavButton({ @@ -11,6 +11,7 @@ export function NavButton({ onClick = () => {}, href = undefined, disabled = false, + ref, }: { icon?: IconDefinition iconElement?: JSX.Element @@ -19,11 +20,13 @@ export function NavButton({ onClick?: MouseEventHandler href?: string disabled?: boolean + ref?: Ref }) { // note: it seems that we can just leave the `target="_blank"` and it has no // effect on links without a `href`. If not, add `if (href)` statement here... return ( { + // Never highlight comparator option if there's no code + const args = parseArgs(window.location.hash) + if (!args.code?.trim() && !args.codez?.trim()) return false // No warning for empty code or example-url-driven code + + // Highlight comparator if there's no referrer or if the referrer isn't safelisted + if (!document.referrer) return true + const referrer = new URL(document.referrer) + if (!lean4webConfig.comparatorSafeList) return true + return !lean4webConfig.comparatorSafeList.some((item) => + item instanceof RegExp ? referrer.hostname.match(item) : referrer.hostname === item, + ) +})() + /** The menu items either appearing inside the dropdown or outside */ function FlexibleMenu({ isInDropdown = false, @@ -70,6 +88,24 @@ function FlexibleMenu({ const code = useAtomValue(codeAtom) const isUsingUrlCode = !!urlArgs?.url + const settings = useAtomValue(settingsAtom) + const themeVariant = lightThemes.includes(settings.theme) + ? 'light' + : settings.theme === 'Cobalt' + ? 'cobalt' + : 'dark' + const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingsAtom) + const [comparatorWarningDismissed, setComparatorWarningDismissed] = useState(false) + const comparatorWarningEligible = + !isInDropdown && + !isUsingUrlCode && + referrerNeedsComparator && + !localOnlySettings.ignoreComparatorWarning + const [trustButtonEl, setTrustButtonEl] = useState(null) + const [trustArrowEl, setTrustArrowEl] = useState(null) + const comparatorWarningOpen = + !!trustButtonEl && comparatorWarningEligible && !comparatorWarningDismissed + const loadFileFromDisk = (event: ChangeEvent) => { console.debug('Loading file from disk') const fileToLoad = event.target.files![0] @@ -151,21 +187,66 @@ function FlexibleMenu({ }} /> - { - window.location.assign('https://comparator.live.lean-lang.org/' + window.location.hash) - }} - /> + {lean4webConfig.comparator && ( + { + window.location.assign(lean4webConfig.comparator + window.location.hash) + }} + /> + )} + + setComparatorWarningDismissed(true)}> +
+ + +
+ + ) } @@ -276,7 +357,13 @@ export function Menu({ }} /> setToolsOpen(true)} /> - { navbar.requiresNavBar != 0 && navbar.setHideNavBar(!navbar.hideNavBar)} />} + {navbar.requiresNavBar != 0 && ( + navbar.setHideNavBar(!navbar.hideNavBar)} + /> + )} Date: Tue, 9 Jun 2026 13:45:27 -0400 Subject: [PATCH 3/3] wording --- client/src/api/config-types.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/api/config-types.ts b/client/src/api/config-types.ts index 27ddbfdf..0757c00c 100644 --- a/client/src/api/config-types.ts +++ b/client/src/api/config-types.ts @@ -18,7 +18,7 @@ export type LeanWebConfig = { * (example: `"https://comparator.live.lean-lang.org/"`) */ comparator: string | null - /** URLs to safelist so that they do not prompt a popup highlighting the "Can I Trust This Proof?" button. + /** URLs to safelist so that refer links do not prompt a popup highlighting the "Can I Trust This Proof?" button. * Ignored if `comparator` option is `null`. */ comparatorSafeList: (string | RegExp)[] | null