Merge branch 'main' into release/0.21.1

docs/components/home/ProsOrConsList.tsx

@@ -0,0 +1,53 @@
+import { ComponentProps } from "react";
+import { twMerge } from "tailwind-merge";
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
+import { faCheck, faXmark } from '@fortawesome/free-solid-svg-icons'
+import { classNames } from "./classNames";
+
+interface ProsOrConsListProps extends ComponentProps<"div"> {
+  items: Readonly<string[]>;
+  label: string;
+  type: "pro" | "con";
+}
+
+export function ProsOrConsList({ items, label, type }: ProsOrConsListProps) {
+  const pluralType = `${type}s`;
+
+  return (
+    <div
+      className={twMerge(
+        classNames.prosOrConsContainer,
+        classNames[`${pluralType}Container`]
+      )}
+    >
+      <div
+        className={twMerge(
+          classNames.prosOrConsLabel,
+          classNames[`${pluralType}Label`]
+        )}
+      >
+        {label}
+      </div>
+
+      {items.map((item) => (
+        <div
+          className={twMerge(
+            classNames.proOrConContainer,
+            classNames[`${type}Container`]
+          )}
+          key={item}
+        >
+          <div
+            className={twMerge(
+              classNames.proOrConIcon,
+              classNames[`${pluralType}Icon`]
+            )}
+          >
+            <FontAwesomeIcon icon={type === "pro" ? faCheck : faXmark} />
+          </div>
+          {item}
+        </div>
+      ))}
+    </div>
+  );
+}

docs/components/home/classNames.ts

@@ -0,0 +1,87 @@
+export const classNames = {
+  container: `
+    flex
+    flex-col
+    gap-6
+  `,
+
+  benefitContainer: `
+    flex
+    flex-col
+    gap-2
+  `,
+
+  benefitTitle: `
+    text-2xl
+    flex
+    items-center
+    gap-2
+  `,
+
+  benefitIcon: `
+    text-quint-purple
+    w-8
+  `,
+
+  prosAndConsContainer: `
+    flex
+    ml-4
+  `,
+
+  prosOrConsContainer: `
+    px-6
+    py-3
+    flex
+    flex-col
+    gap-2
+    w-full
+  `,
+
+  prosContainer: `
+    bg-quint-purple/10
+    rounded-l-xl
+  `,
+
+  consContainer: `
+    bg-quint-orange/10
+    rounded-r-xl
+  `,
+
+  prosOrConsLabel: `
+    font-bold
+  `,
+
+  prosLabel: `
+    text-quint-purple
+  `,
+
+  consLabel: `
+    text-quint-orange
+  `,
+
+  proOrConContainer: `
+    grid
+    grid-cols-[min-content,auto]
+    gap-2
+    w-full
+  `,
+
+  proContainer: `
+  `,
+
+  conContainer: `
+  `,
+
+  proOrConIcon: `
+    col-start-1
+    col-end-2
+  `,
+
+  proIcon: `
+    text-violet-400
+  `,
+
+  conIcon: `
+    text-amber-400
+  `,
+};

docs/components/home/index.tsx

@@ -1,24 +1,49 @@
 import { Code, Pre } from "nextra/components"
 
 import React from "react";
-import { useState } from 'react'
+import { useState, useEffect } from 'react'
 import { useTheme } from 'nextra-theme-docs'
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
+import { faCheckCircle } from '@fortawesome/free-solid-svg-icons'
 import CodeSample from './code_sample.mdx'
 import ViolationSample from './violation_sample.mdx'
 
 import Image from 'next/image'
 
+import { classNames } from "./classNames";
+import { ProsOrConsList } from "./ProsOrConsList";
+
+const benefits = [
+  [
+    "Executable",
+    ["Quint", ["checked names and types", "executable"]],
+    ["English & Markdown", ["not checked", "not executuable"]],
+  ],
+  [
+    "Abstract",
+    ["Specification Languages", ["define only what you care about"]],
+    ["Programming Languages", ["define how things happen, in detail"]],
+  ],
+  [
+    "Modern",
+    ["Quint", ["familiar syntax", "CLI and your editor"]],
+    ["Existing Spec Languages", ["math-y syntax", "old GUI tools"]],
+  ],
+] as const;
+
+
 function informalSystemsLogo() {
-    const { resolvedTheme } = useTheme()
-    if (resolvedTheme == "dark") {
-      return (
-        <Image src="/informal-systems-white.png" alt="Informal Systems" width={200} height={200} />
-      );
-    } else {
-      return (
-        <Image src="/informal-systems.png" alt="Informal Systems" width={200} height={200} />
-      );
-  }
+  const { resolvedTheme } = useTheme();
+  const [theme, setTheme] = useState(null);
+    useEffect(() => {
+    setTheme(resolvedTheme);
+  }, [resolvedTheme]);
+
+  return (
+    <a href="https://informal.systems">
+      <Image src={theme == "dark" ? "/informal-systems-white.png" : "/informal-systems.png"} alt="Informal Systems" width={200} height={200} />
+    </a>
+  )
 }
 
 const components = {
@@ -42,41 +67,37 @@ export function Home() {
       <div className="relative px-4 mx-auto max-w-7xl sm:px-6 lg:px-2">
         <h1 className="text-4xl text-center font-bold leading-tight text-inherit sm:text-5xl sm:leading-tight lg:text-6xl lg:leading-tight font-pj">Quint</h1>
         <h2 className="text-quint-purple text-2xl text-center font-bold leading-tight sm:text-2xl sm:leading-tight lg:text-3xl lg:leading-tight font-pj">A modern and executable specification language</h2>
-        <div className="grid grid-cols-1 py-8 gap-y-4 lg:mt-8 lg:items-start lg:grid-cols-2 xl:grid-cols-2">
-          <div className="xl:col-span-1 lg:text-left text-center md:px-16 lg:px-0 xl:pr-20">
-            <h3 className="text-2xl font-bold leading-relaxed">Executable</h3>
-            <ul className="list-inside indent-4">
-              <li>English and Markdown: not checked, not executable</li>
-              <li className="font-bold">Quint: checked names and types, <a className="underline decoration-2 decoration-quint-purple">executable</a></li>
-            </ul>
-            <br />
-
-            <h3 className="text-2xl font-bold leading-relaxed">Specification language</h3>
-            <ul className="list-inside indent-4">
-              <li>Programming languages: define how things happen in detail</li>
-              <li className="font-bold">Specification languages: define only what you <a className="underline decoration-2 decoration-quint-purple">care</a> about</li>
-            </ul>
-            <br />
-
-            <h3 className="text-2xl font-bold leading-relaxed">Modern</h3>
-            <ul className="list-inside indent-4">
-              <li>Existing specification languages: Mathy syntax, old GUI tools</li>
-              <li className="font-bold">Quint: <a className="underline decoration-2 decoration-quint-purple">Familiar</a> syntax, CLI-first, tools for VSCode, Vim and Emacs</li>
-            </ul>
-
-            <a href="/docs/getting-started" title="" className="inline-flex px-8 py-4 mt-8 text-lg font-bold transition-all duration-200 bg-quint-purple text-white rounded sm:mt-10 font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900" role="button">
-              Get started
-            </a>
-
-            <div className="mt-8 mb-8 flex justify-center lg:justify-start">
-              {informalSystemsLogo()}
+        <div className="grid grid-cols-1 py-8 gap-y-4 gap-x-8 lg:mt-8 lg:items-start lg:grid-cols-2 xl:grid-cols-2">
+          <div className="xl:col-span-1">
+            <div className={classNames.container}>
+              {benefits.map(([label, [prosLabel, pros], [consLabel, cons]]) => (
+                <div className={classNames.benefitContainer}>
+                  <h1 className={classNames.benefitTitle}>
+                    <div className={classNames.benefitIcon}>
+                      <FontAwesomeIcon icon={faCheckCircle} />
+                    </div>
+                    {label}
+                  </h1>
+
+                  <div className={classNames.prosAndConsContainer}>
+                    <ProsOrConsList items={pros} label={prosLabel} type="pro" />
+                    <ProsOrConsList items={cons} label={consLabel} type="con" />
+                  </div>
+                </div>
+              ))}
+            </div>
+
+            <div className="mt-4 mb-8 flex justify-center">
+              <a href="/docs/getting-started" title="" className="inline-flex px-8 py-4 mt-8 text-lg font-bold transition-all duration-200 bg-quint-purple text-black rounded sm:mt-10 font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900" role="button">
+                Get started
+              </a>
             </div>
           </div>
 
           <div className="xl:col-span-1 text-lg">
             <CodeSample components={components} />
             <div className="flex justify-center">
-              <button onClick={handleToggleVisibility} className={`transition-all duration-500 ease-out overflow-hidden ${isViolationVisible ? 'hidden' : 'visible'} inline-flex px-4 py-2 font-bold transition-all duration-200 bg-quint-purple text-white rounded font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900`}>
+              <button onClick={handleToggleVisibility} className={`transition-all duration-500 ease-out overflow-hidden ${isViolationVisible ? 'hidden' : 'visible'} inline-flex px-4 py-2 font-bold transition-all duration-200 bg-quint-purple text-black rounded font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900`}>
                 Find bug
               </button>
             </div>
@@ -85,6 +106,10 @@ export function Home() {
             </div>
           </div>
         </div>
+
+        <div className="mt-8 mb-8 flex justify-center">
+          {informalSystemsLogo()}
+        </div>
       </div>
     </section >
   </div >

docs/package.json

@@ -1,11 +1,15 @@
 {
   "dependencies": {
+    "@fortawesome/fontawesome-svg-core": "^6.5.2",
+    "@fortawesome/free-solid-svg-icons": "^6.5.2",
+    "@fortawesome/react-fontawesome": "^0.2.2",
     "next": "^14.2.4",
     "nextra": "^2.13.4",
     "nextra-theme-docs": "^2.13.4",
     "react": "^18.3.1",
     "react-dom": "^18.3.1",
-    "react-svg": "^16.1.34"
+    "react-svg": "^16.1.34",
+    "tailwind-merge": "2.3.0"
   },
   "scripts": {
     "dev": "next",