Fix bad destination for #11

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,31 @@ 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, 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<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]
@@ -139,6 +191,63 @@ 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('ignoreComparatorWarning', true)
+              }}
+            >
+              Don't show this again
+            </button>
+          </div>
+        </ClickAwayListener>
+      </Popper>{' '}
     </>
   )
 }
@@ -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 (
     <div className="menu">

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>(settings)
-  const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingAtom)
+  const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingsAtom)
 
   function updateSetting<K extends keyof Settings>(key: K, value: Settings[K]) {
     setNewSettings((prev) => ({ ...prev, [key]: value }))
@@ -209,8 +209,23 @@ export function SettingsPopup({
             }}
             checked={!!localOnlySettings.hideNavbar}
           />
-          <label htmlFor="hideNavbar">Always hide the site navigation header for links from the Lean FRO or Mathlib Initiative</label>
+          <label htmlFor="hideNavbar">
+            Always hide the site navigation header for links from the Lean FRO or Mathlib Initiative
+          </label>
         </p>
+        <p>
+          <Switch
+            id="comparatorWarning"
+            onChange={() => {
+              setLocalOnlySettings(
+                'ignoreComparatorWarning',
+                !localOnlySettings.ignoreComparatorWarning,
+              )
+            }}
+            checked={!!localOnlySettings.ignoreComparatorWarning}
+          />
+          <label htmlFor="comparatorWarning">Hide warnings about code from unknown sources</label>
+        </p>{' '}
       </form>
     </Popup>
   )