feat: link live.lean-lang.org to comparator.live.lean-lang.org

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$/],
 };

client/src/api/config-types.ts

@@ -13,4 +13,13 @@ export type LeanWebConfig = {
    * (example: `<><p>vat number: 000</p><>`)
    */
   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
 }

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;
+}

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,18 +10,30 @@ export function NavButton({
   title,
   onClick = () => {},
   href = undefined,
+  disabled = false,
+  ref,
 }: {
   icon?: IconDefinition
   iconElement?: JSX.Element
   text: string
   title?: string
   onClick?: MouseEventHandler<HTMLAnchorElement>
   href?: string
+  disabled?: boolean
+  ref?: Ref<HTMLAnchorElement>
 }) {
   // 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 (
-    <a className="nav-link" title={title} onClick={onClick} href={href!} target="_blank">
+    <a
+      ref={ref}
+      className={`nav-link${disabled ? ' disabled' : ''}`}
+      title={title}
+      aria-disabled={disabled || undefined}
+      onClick={disabled ? (e) => e.preventDefault() : onClick}
+      href={href!}
+      target="_blank"
+    >
       {iconElement ?? <FontAwesomeIcon icon={icon!} />}&nbsp;{text}
     </a>
   )

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,26 +21,44 @@ import {
   faXmark,
 } from '@fortawesome/free-solid-svg-icons'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { useAtom } 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'
 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'
 import LoadZulipPopup from '../Popups/LoadZulip'
 import PrivacyPopup from '../Popups/PrivacyPolicy'
 import ToolsPopup from '../Popups/Tools'
-import { mobileAtom } from '../settings/settings-atoms'
+import { localOnlySettingsAtom, mobileAtom, 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'
 
-import { useNavBar } from '../context/NavBarContext'
+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({
@@ -58,8 +82,30 @@ function FlexibleMenu({
   setLoadUrlOpen: Dispatch<SetStateAction<boolean>>
   setLoadZulipOpen: Dispatch<SetStateAction<boolean>>
 }) {
-  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<HTMLAnchorElement | null>(null)
+  const [trustArrowEl, setTrustArrowEl] = useState<HTMLElement | null>(null)
+  const comparatorWarningOpen =
+    !!trustButtonEl && comparatorWarningEligible && !comparatorWarningDismissed
+
   const loadFileFromDisk = (event: ChangeEvent<HTMLInputElement>) => {
     console.debug('Loading file from disk')
     const fileToLoad = event.target.files![0]
@@ -141,6 +187,66 @@ function FlexibleMenu({
           }}
         />
       </Dropdown>
+      {lean4webConfig.comparator && (
+        <NavButton
+          ref={isInDropdown ? undefined : setTrustButtonEl}
+          icon={faHandshake}
+          text={'Can I Trust This Proof?'}
+          disabled={isUsingUrlCode}
+          title={
+            isUsingUrlCode
+              ? 'Example urls not supported by Comparator tool! Edit the text to enable.'
+              : (code ?? '').trim() === ''
+                ? 'Open the Comparator verification tool'
+                : 'Open this proof in the Comparator verification tool'
+          }
+          onClick={() => {
+            window.location.assign(lean4webConfig.comparator + window.location.hash)
+          }}
+        />
+      )}
+      <Popper
+        open={comparatorWarningOpen}
+        anchorEl={trustButtonEl}
+        placement="bottom-end"
+        modifiers={[
+          { name: 'flip', enabled: false },
+          { name: 'offset', options: { offset: [0, 12] } },
+          { name: 'arrow', enabled: true, options: { element: trustArrowEl, padding: 8 } },
+        ]}
+      >
+        <ClickAwayListener onClickAway={() => setComparatorWarningDismissed(true)}>
+          <div
+            className={`comparator-warning ${themeVariant}`}
+            role="status"
+            aria-label="Verify untrusted proofs with Comparator"
+          >
+            <span className="comparator-warning-arrow" ref={setTrustArrowEl}></span>
+            <button
+              className="codicon codicon-close comparator-warning-close"
+              aria-label="Dismiss"
+              onClick={() => setComparatorWarningDismissed(true)}
+            />
+            <p>
+              Don't trust proofs from untrusted sources unless they're validated against a trusted
+              challenge. Use the <strong>Can I Trust This Proof?</strong> button to check this proof
+              with the online version of Lean's Comparator tool.
+            </p>
+            <button
+              className="comparator-warning-perma-dismiss"
+              onClick={() => {
+                setComparatorWarningDismissed(true)
+                setLocalOnlySettings({
+                  ...localOnlySettings,
+                  ignoreComparatorWarning: true,
+                })
+              }}
+            >
+              Don't show this again
+            </button>
+          </div>
+        </ClickAwayListener>
+      </Popper>
     </>
   )
 }
@@ -251,7 +357,13 @@ export function Menu({
           }}
         />
         <NavButton icon={faHammer} text="Lean Info" onClick={() => setToolsOpen(true)} />
-        { navbar.requiresNavBar != 0 && <NavButton icon={faEye} text={`${navbar.hideNavBar ? "Show" : "Hide"} Navbar`} onClick={() => navbar.setHideNavBar(!navbar.hideNavBar)} />}
+        {navbar.requiresNavBar != 0 && (
+          <NavButton
+            icon={faEye}
+            text={`${navbar.hideNavBar ? 'Show' : 'Hide'} Navbar`}
+            onClick={() => navbar.setHideNavBar(!navbar.hideNavBar)}
+          />
+        )}
         <NavButton icon={faArrowRotateRight} text="Restart server" onClick={restart} />
         <NavButton
           icon={faDownload}

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>(settings)
+  const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingsAtom)
 
   function updateSetting<K extends keyof Settings>(key: K, value: Settings[K]) {
     setNewSettings((prev) => ({ ...prev, [key]: value }))
@@ -198,6 +199,23 @@ export function SettingsPopup({
             onClick={() => applySettings(newSettings)}
           />
         </p>
+        <h2>Local Settings</h2>
+        <p>
+          <i>These settings are always preserved in the browser's local storage.</i>
+        </p>
+        <p>
+          <Switch
+            id="comparatorWarning"
+            onChange={() => {
+              setLocalOnlySettings({
+                ...localOnlySettings,
+                ignoreComparatorWarning: !localOnlySettings.ignoreComparatorWarning,
+              })
+            }}
+            checked={!!localOnlySettings.ignoreComparatorWarning}
+          />
+          <label htmlFor="comparatorWarning">Hide warnings about code from unknown sources</label>
+        </p>
       </form>
     </Popup>
   )

client/src/settings/settings-atoms.ts

@@ -13,6 +13,20 @@ const settingsStoreAtom = atomWithStorage<PartialUserSettings>('lean4web:setting
   getOnInit: true,
 })
 
+interface PartialLocalOnlyUserSettings {
+  ignoreComparatorWarning?: boolean
+}
+
+/** Settings always stored on localstorage, never in the URL */
+export const localOnlySettingsAtom = atomWithStorage<PartialLocalOnlyUserSettings>(
+  'lean4web:local-settings',
+  {},
+  undefined,
+  {
+    getOnInit: true,
+  },
+)
+
 /** The settings which are set in the searchParams of the opened URL */
 const settingsUrlAtom = atom(
   (get) => {