From 5c9ff5132cd829d971d123c3490bded42f12ac6f Mon Sep 17 00:00:00 2001
From: s-taiga <neverbefore351@gmail.com>
Date: Mon, 23 Sep 2024 16:50:12 +0900
Subject: [PATCH] =?UTF-8?q?=E6=97=A5=E6=9C=AC=E8=AA=9E=E8=A8=B3=E3=81=AB?=
 =?UTF-8?q?=E9=9A=9B=E3=81=97=E3=81=A6=E3=81=AE=E6=83=85=E5=A0=B1=E8=BF=BD?=
 =?UTF-8?q?=E8=A8=98?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 scripts/mkdoc.py      | 21 +++++++++++++++++++--
 sphinx_source/conf.py |  2 +-
 2 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/scripts/mkdoc.py b/scripts/mkdoc.py
index b8aa0924..22ee60ea 100755
--- a/scripts/mkdoc.py
+++ b/scripts/mkdoc.py
@@ -72,8 +72,8 @@ def make_lean_user_main_import_file():
         import_file.write(f"import MIL.Common\n")
 
 index_file_start = """
-Mathematics in Lean
-===================
+Mathematics in Lean 日本語訳
+============================
 
 .. toctree::
    :numbered:
@@ -86,6 +86,23 @@ def make_lean_user_main_import_file():
    :hidden:
 
    genindex
+
+この翻訳について
+----------------
+
+この翻訳は有志による **非公式** 翻訳です．翻訳に際して分かりやすさのために表現を大きく変えた箇所があります．また，用語の訳が一般的でない・誤りを含む可能性があります．必要に応じて原文 `Mathematics in Lean <https://leanprover-community.github.io/mathematics_in_lean/index.html>`_ ( `GitHub <https://github.com/avigad/mathematics_in_lean_source>`_ )をご覧ください．
+
+原文にはライセンスが無かったため，原著者より許諾をいただいて翻訳させていただいています．（ `Zulip chat <https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Translating.20.60Mathematics.20in.20Lean.60.20to.20Japanese/near/395294386>`_ ）
+
+誤字脱字・内容の誤りの指摘・フォークからのPull Request・フォークによる翻訳の改変等歓迎いたします．ご指摘は `当該リポジトリ <https://github.com/lean-ja/mathematics_in_lean_source>`_ にてIssue・Pull Requestで受け付けております．
+
+翻訳に際して，機械翻訳サービス `DeepL翻訳 <https://www.deepl.com/ja/translator>`_ を参考にしました．
+
+バージョン情報
+--------------
+
+この翻訳は原文のcommit `2bba5592ebfb3075ca1fd4d12843d2bf197bb0d1 <https://github.com/lean-ja/mathematics_in_lean_source/commit/2bba5592ebfb3075ca1fd4d12843d2bf197bb0d1>`_ に基づいています．
+
 """
 
 def make_sphinx_index_file():
diff --git a/sphinx_source/conf.py b/sphinx_source/conf.py
index 441db647..fd4cf26d 100644
--- a/sphinx_source/conf.py
+++ b/sphinx_source/conf.py
@@ -16,7 +16,7 @@
 
 # -- Project information -----------------------------------------------------
 
-project = 'Mathematics in Lean'
+project = 'Mathematics in Lean 日本語訳'
 copyright = '2020, Jeremy Avigad, Patrick Massot'
 author = 'Jeremy Avigad, Patrick Massot'