From a65bcb4ae88be1034312f41710a8d10637277c1b Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 9 Jun 2026 18:18:33 -0400 Subject: [PATCH 1/2] update types --- client/src/api/config-types.ts | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/client/src/api/config-types.ts b/client/src/api/config-types.ts index 7f05a165..0757c00c 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 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 } From 4d4ef642fb483860c33facdae2d417d108ba97e3 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 9 Jun 2026 18:26:01 -0400 Subject: [PATCH 2/2] Add the rest of comparator-on-live infra --- client/config.tsx | 2 + client/src/css/Navigation.css | 78 ++++++++++++++++ client/src/navigation/NavButton.tsx | 17 +++- client/src/navigation/Navigation.tsx | 123 ++++++++++++++++++++++++-- client/src/settings/SettingsPopup.tsx | 21 ++++- client/src/settings/settings-atoms.ts | 10 ++- 6 files changed, 235 insertions(+), 16 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/css/Navigation.css b/client/src/css/Navigation.css index dc155427..107bc822 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; @@ -148,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; +} \ No newline at end of file diff --git a/client/src/navigation/NavButton.tsx b/client/src/navigation/NavButton.tsx index a7a1920e..faa641c4 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({ @@ -10,6 +10,8 @@ export function NavButton({ title, onClick = () => {}, href = undefined, + disabled = false, + ref, }: { icon?: IconDefinition iconElement?: JSX.Element @@ -17,11 +19,22 @@ export function NavButton({ title?: string 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 ( - + e.preventDefault() : onClick} + href={href!} + target="_blank" + > + {' '} {iconElement ?? } {text} ) diff --git a/client/src/navigation/Navigation.tsx b/client/src/navigation/Navigation.tsx index 2f7cde95..fa8d2872 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, faEye, faInfoCircle } from '@fortawesome/free-solid-svg-icons' +import { + faArrowRotateRight, + faCode, + faEye, + faHandshake, + faInfoCircle, +} from '@fortawesome/free-solid-svg-icons' import { faArrowUpRightFromSquare, faBars, @@ -15,7 +21,9 @@ import { faXmark, } from '@fortawesome/free-solid-svg-icons' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { useAtom, useAtomValue } from 'jotai' +import ClickAwayListener from '@mui/material/ClickAwayListener' +import Popper from '@mui/material/Popper' +import { useAtom, useAtomValue, useSetAtom } from 'jotai' import { ChangeEvent, Dispatch, SetStateAction, useState } from 'react' import { lean4webConfig } from '../../config' @@ -26,14 +34,36 @@ import LoadUrlPopup from '../Popups/LoadUrl' import LoadZulipPopup from '../Popups/LoadZulip' import PrivacyPopup from '../Popups/PrivacyPolicy' import ToolsPopup from '../Popups/Tools' -import { localOnlySettingAtom, mobileAtom, navBarRequestedAtom } from '../settings/settings-atoms' +import { + localOnlySettingsAtom, + mobileAtom, + navBarRequestedAtom, + settingsAtom, +} from '../settings/settings-atoms' +import { lightThemes } from '../settings/settings-types' 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 { parseArgs } from '../store/url-converters' import { save } from '../utils/SaveToFile' import { Dropdown } from './Dropdown' import { NavButton } from './NavButton' +const referrerNeedsComparator = (() => { + // 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, @@ -56,8 +86,30 @@ 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 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] @@ -139,6 +191,63 @@ function FlexibleMenu({ }} /> + {lean4webConfig.comparator && ( + { + window.location.assign(lean4webConfig.comparator + window.location.hash) + }} + /> + )} + + setComparatorWarningDismissed(true)}> +
+ + +
+ + {' '} ) } @@ -175,8 +284,8 @@ export function Menu({ const [mobile] = useAtom(mobileAtom) const hasImpressum = lean4webConfig.impressum || lean4webConfig.contactDetails - const navBarRequested = useAtomValue(navBarRequestedAtom); - const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingAtom) + const navBarRequested = useAtomValue(navBarRequestedAtom) + const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingsAtom) return (
diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index 2228163d..c08d9fe6 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 { localOnlySettingAtom, settingsAtom } from './settings-atoms' +import { localOnlySettingsAtom, settingsAtom } from './settings-atoms' import type { MobileValues, Theme } from './settings-types' import { defaultSettings, Settings } from './settings-types' @@ -21,7 +21,7 @@ export function SettingsPopup({ }) { const [settings, applySettings] = useAtom(settingsAtom) const [newSettings, setNewSettings] = useState(settings) - const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingAtom) + const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingsAtom) function updateSetting(key: K, value: Settings[K]) { setNewSettings((prev) => ({ ...prev, [key]: value })) @@ -209,8 +209,23 @@ export function SettingsPopup({ }} checked={!!localOnlySettings.hideNavbar} /> - +

+

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

{' '} ) diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts index b4644989..7c503334 100644 --- a/client/src/settings/settings-atoms.ts +++ b/client/src/settings/settings-atoms.ts @@ -17,12 +17,14 @@ const settingsStoreAtom = atomWithStorage('lean4web:setting interface PartialLocalOnlyUserSettings { /** Hide the navigation bar that otherwise appears when `?from=lean` or `?from=mathlib` is set. */ hideNavbar?: boolean + /** Suppress the warning about checking code from unknown websites with comparator. */ + ignoreComparatorWarning?: boolean } // Migrate legacy `hideNavBar` option to new setting (added June 2026, delete after October 2026) if (localStorage.getItem('hideNavBar')) { - if (localStorage.getItem('hideNavBar') === "true") { - localStorage.setItem("lean4web:local-settings", '{"hideNavbar":true}') + if (localStorage.getItem('hideNavBar') === 'true') { + localStorage.setItem('lean4web:local-settings', '{"hideNavbar":true}') } localStorage.removeItem('hideNavBar') } @@ -49,7 +51,7 @@ const fullLocalOnlySettingsAtom = atomWithStorage( ) /** Local-only settings are always stored in local storage, never in the URL */ -export const localOnlySettingAtom = atom( +export const localOnlySettingsAtom = atom( (get) => get(fullLocalOnlySettingsAtom), (get, set, key: keyof PartialLocalOnlyUserSettings, value: boolean) => { const next = { ...get(fullLocalOnlySettingsAtom) } @@ -73,7 +75,7 @@ export const navBarRequestedAtom = atom(() => { /** Which navigation header will be shown */ export const navBarAtom = atom((get) => { - if (get(localOnlySettingAtom).hideNavbar) return null + if (get(localOnlySettingsAtom).hideNavbar) return null return get(navBarRequestedAtom) })