Deploy lean-ja/lean-ja.github.io to lean-ja/lean-ja.github.io:gh-pages

lean-ja · Oct 14, 2023 · 8df4320 · 8df4320
commit 8df4320
Show file tree

Hide file tree

Showing 9 changed files with 839 additions and 0 deletions.
diff --git a/404.html b/404.html
@@ -0,0 +1,3 @@
+<!doctype html>
+<title>404 Not Found</title>
+<h1>404 Not Found</h1>
diff --git a/index.html b/index.html
@@ -0,0 +1,195 @@
+<!DOCTYPE html>
+<html lang="ja">
+
+<head>
+    <meta charset="UTF-8">
+    <title>LEAN JA</title>
+    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
+
+    <link rel="icon" type="image/png" href="/favicon.ico">
+
+
+<style>
+    :root {
+        /* Primary theme color: gray-50 */
+        --primary-color: #f9fafb;
+        /* Primary theme text color: gray-900*/
+        --primary-text-color: #111827;
+        --primary-text-color-over: #0c4a6e;
+        /* Primary theme link color */
+        --primary-link-color: #60a5fa;
+        /* Secondary color: the background body color: gray-100 */
+        --secondary-color: #f3f4f6;
+        --secondary-text-color: #303030;
+        /* Highlight text color of table of content: sky-700 */
+        --toc-highlight-text-color: #0369a1;
+        --toc-background-color: white;
+        --code-color: #4a4a4a;
+        --code-background-color: white;
+        --shadow-color: #ddd;
+        /* Font used for headers (h1 & h2) */
+        --header-font-family: "Fira Sans", sans-serif;
+        /* Font used for text */
+        --text-font-family: "Noto Sans JP", "Fira Sans", sans-serif;
+    }
+</style>
+
+    <link href="https://fonts.googleapis.com/css?family=Alfa+Slab+One&display=swap" rel="stylesheet">
+    <link href="https://fonts.googleapis.com/css?family=Fira+Sans:400,500,600&display=swap" rel="stylesheet">
+    <link href="https://fonts.googleapis.com/css2?family=Noto+Sans+JP:wght@400;500;700&display=swap" rel="stylesheet">
+
+    <link rel="stylesheet" href="/normalize.css">
+    <link rel="stylesheet" href="https://lean-ja.github.io/juice.css">
+
+
+</head>
+
+<body>
+
+
+    <header class="pos-absolute" style="background-color: transparent">
+
+
+<a href="https://lean-ja.github.io/">
+    <div class="logo">
+        <img src="https://lean-ja.github.io/lean_ja.svg" alt="logo">
+        LEAN JA
+    </div>
+</a>
+
+<nav>
+
+
+
+    <a class="nav-item subtitle-text" href="https://lean-ja.github.io/links/">Links</a>
+
+
+
+
+        <a class="nav-item subtitle-text" href="https://github.com/lean-ja">Github</a>
+
+
+</nav>
+
+    </header>
+
+    <div class="hero">
+
+    <script async defer src="https://buttons.github.io/buttons.js"></script>
+    <section class="text-center">
+        <img class="hero-image" style="max-width: 70%; min-width: 300px;" src="https://lean-ja.github.io/lean_ja.svg">
+        <h1 class="heading-text">
+            Lean 言語の日本語コミュニティ
+        </h1>
+    </section>
+
+
+    <div class="explore-more text"
+        onclick="document.getElementById('features').scrollIntoView({behavior: 'smooth'})">
+        Explore More ⇩
+    </div>
+    <style>
+        .hero section {
+            padding: 0 5rem;
+        }
+
+        h1.heading-text {
+            font-size: 40px;
+        }
+
+        @media screen and (max-width: 768px) {
+            .hero section {
+                padding: 0 2rem;
+            }
+
+            h1.heading-text {
+                font-size: 20px;
+            }
+        }
+    </style>
+
+    </div>
+
+
+
+    <main>
+
+
+
+
+
+        <div class="toc">
+            <div class="toc-sticky">
+
+                <div class="toc-item">
+                    <a class="subtext" href="https://lean-ja.github.io/#lean-nituite">Lean について</a>
+                </div>
+
+
+                <div class="toc-item">
+                    <a class="subtext" href="https://lean-ja.github.io/#watasitatinituite">わたしたちについて</a>
+                </div>
+
+
+            </div>
+        </div>
+
+
+
+        <div class="content text">
+
+
+    <span id="features"></span>
+
+    <h2 id="lean-nituite"><strong>Lean について</strong></h2>
+<p><a href="https://leanprover.github.io/">Lean</a> は容易に正しく保守性の高いコードを書くことができるよう設計された，純粋関数型言語です．依存型という表現力の高い型システムを備えており，アルゴリズムなどが本当に意図したものを返すことを証明することができます．</p>
+<p>Lean は証明支援系でもあり，数学の証明を検証する能力を備えています．Lean で証明を書いている限り，コンパイルが通れば証明は正しいと自信を持つことができます．</p>
+<p>そして Lean はパワフルです．いま示すべきことと得られていることを逐一表示できるのはもちろん，証明の一部を自動化したり，強すぎる仮定を自動的に検出したりすることもできます．</p>
+<p><img src="https://lean-ja.github.io/./lean-playing.png" alt="Leanのプレイ風景" /></p>
+<p>現在，Lean で数学理論を実装していこうという努力が積極的に行われています．<a href="https://github.com/leanprover-community/mathlib4">mathlib4</a> というライブラリがあり，大学の学部程度の数学のかなりの部分を Lean で行うことが可能になっています．</p>
+<p><a href="https://lean.math.hhu.de/">Lean 4 Web</a> から Lean を試すことができます．あなたも Lean で新しい数学を体験してみませんか？</p>
+<h2 id="watasitatinituite"><strong>わたしたちについて</strong></h2>
+<p>lean-ja は，Lean に関する情報の交換と集積を目的とした日本語コミュニティです．<a href="https://github.com/orgs/lean-ja/discussions">discussion</a>でLeanに関する情報を日本語でやり取りすることができます．質問やアイデア共有などにぜひお使いください．</p>
+<p>また，Leanの学習リソースの翻訳を順次ホスト・公開する予定です．</p>
+
+
+        </div>
+
+
+
+    </main>
+
+
+    <footer>
+        <small class="subtext">
+            Maintained by the lean-ja
+        </small>
+    </footer>
+
+</body>
+<script>
+    const scrollHandler = entries => {
+        // Find the first entry which intersecting and ratio > 0.9 to highlight.
+        let entry = entries.find(entry => {
+            return entry.isIntersecting && entry.intersectionRatio > 0.9;
+        });
+        if (!entry) return;
+
+        document.querySelectorAll(".toc a").forEach((item) => {
+            item.classList.remove("active");
+        });
+
+        // let url = new URL(`#${entry.target.id}`);
+        let link = document.querySelector(`.toc a[href$="${decodeURIComponent(`#${entry.target.id}`)}"]`)
+        if (link) {
+            link.classList.add("active");
+            link.scrollIntoView({ behavior: "auto", block: "nearest" });
+        }
+    };
+    // Set -100px root margin to improve highlight experience.
+    const observer = new IntersectionObserver(scrollHandler, { threshold: 1 });
+    let items = document.querySelectorAll('h1,h2,h3,h4,h5,h6');
+    items.forEach(item => observer.observe(item));
+</script>
+
+</html>
diff --git a/juice.css b/juice.css
diff --git a/lean-playing.png b/lean-playing.png
diff --git a/lean_ja.svg b/lean_ja.svg