翻訳準備 (#1)

* 翻訳準備

* CIスクリプト修正

Author: s-taiga

.github/workflows/ci.yml

@@ -3,21 +3,23 @@ on:
     branches:
       - main
   pull_request:
-    branches:
-      - main
-  release:
-    types:
-      - published
-      - released
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
 
 name: Build and deploy sites
 
 jobs:
   build:
     name: Build site and generate HTML
     runs-on: ubuntu-latest
-    outputs:
-      ref-url: ${{ steps.deploy.outputs.deploy-url }}
 
     steps:
       - name: Install deps for figures (OS packages)
@@ -129,100 +131,24 @@ jobs:
           fail: true
           args: --base './_out/html-multi/' --no-progress --offline './_out/html-multi/**/*.html'
 
-      # deploy-alias computes a URL component for the PR preview. This
-      # is so we can have a stable name to use for feedback on draft
-      # material.
-      - id: deploy-alias
-        uses: actions/github-script@v7
-        name: Compute Alias
-        with:
-          script: |
-            if (process.env.PR) {
-                return `pr-${process.env.PR}`
-            } else {
-                return 'deploy-preview-main';
-            }
-        env:
-          PR: ${{ github.event.number }}
-
-        # deploy-info computes metadata that's shown in the Netlify interface
-        # about the deployment (for non-PR deploys)
-      - id: deploy-info
-        name: Compute Deployment Metadata
-        if: github.event_name != 'pull_request'
-        run: |
-          set -e
-          echo "message=$(git log -1 --pretty=format:"%s")" >> "$GITHUB_OUTPUT"
-
-      # When a release is created in GH, push to the main site without proofreading info
-      - name: Deploy releases when tags are pushed
-        id: deploy-release
-        uses: nwtgck/[email protected]
-        if: github.event_name == 'release'
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v3
         with:
-          publish-dir: _out/html-multi
-          production-branch: main
-          production-deploy: true
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          deploy-message: |
-            Release from tag ${{ github.ref }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          fails-without-credentials: true
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "447031bf-9a96-4cee-831b-1f73599a7cb2"
-
-      # When pushing to `main` or a PR branch, deploy what it would look like if this were released
-      - name: Deploy current draft
-        id: deploy-draft
-        uses: nwtgck/[email protected]
-        if: github.event_name == 'push' || github.event_name == 'pull_request'
-        with:
-          publish-dir: _out/html-multi
-          production-branch: main
-          production-deploy: true
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          deploy-message: |
-            ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }}
-          alias: ${{ steps.deploy-alias.outputs.result }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          github-deployment-environment: |
-            ${{ github.event_name == 'pull_request' && format('lean-ref-pr-#{0}', github.event.number) || 'lean-ref' }}
-          github-deployment-description: |
-            Draft without proofreading info
-          fails-without-credentials: true
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "32e0f63e-7a18-4bf9-87f4-713650c7db70"
-
-      # When pushing to `main` or a PR branch, deploy it with proofreading info as well
-      - name: Deploy with proofreading info (draft mode, for PRs)
-        id: deploy-draft-proofreading
-        uses: nwtgck/[email protected]
-        if:
-          github.event_name == 'pull_request'
-        with:
-          publish-dir: _out/draft/html-multi
-          production-branch: main
-          production-deploy: false
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          deploy-message: |
-            ${{ github.event_name == 'pull_request' && format('pr#{0} proofreading: {1}', github.event.number, github.event.pull_request.title) }}
-          alias: draft-${{ steps.deploy-alias.outputs.result }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          github-deployment-environment: |
-            ${{ github.event_name == 'pull_request' && format('lean-ref-pr-draft-#{0}', github.event.number) }}
-          github-deployment-description: |
-            Draft with proofreading info
-          fails-without-credentials: true
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "32e0f63e-7a18-4bf9-87f4-713650c7db70"
-
-
+          path: _out/html-multi
+  
+  # Deployment job
+  deploy:
+    if: github.ref == 'refs/heads/main'
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4
+  
 
   check-links:
     name: Check links

.github/workflows/pr-title.yml

@@ -0,0 +1,10 @@
+# 対訳表
+
+| 英語 | 日本語 |
+| --- | --- |
+
+
+# 英語表現をそのまま用いている単語
+
+| 用語 |
+| --- |

GLOSSARY.md

@@ -18,11 +18,18 @@ open Verso.Genre Manual
 
 set_option pp.rawOnError true
 
+/-
 #doc (Manual) "The Lean Language Reference" =>
+-/
+#doc (Manual) "The Lean Language Reference 日本語訳" =>
 %%%
 tag := "lean-language-reference"
 %%%
 
+**注意:** この翻訳は有志による **非公式** 翻訳です。原文の最新版は [こちら](https://lean-lang.org/doc/reference/latest/) です。
+
+_CAUTION:_ This is an **Unofficial** translation by volunteers.
+The latest version of original is [here](https://lean-lang.org/doc/reference/latest/).
 
 This is the _Lean Language Reference_, an in-progress reference work on Lean.
 It is intended to be a comprehensive, precise description of Lean: a reference work in which Lean users can look up detailed information, rather than a tutorial for new users.
@@ -147,7 +154,17 @@ file := some "the-index"
 
 {theIndex}
 
+# この翻訳について
+
+この翻訳は有志による **非公式** 翻訳です。翻訳に際して分かりやすさのために表現を大きく変えた箇所があります。また、用語の訳が一般的でない・誤りを含む可能性があります。必要に応じて原文 [Lean Language Reference](https://lean-lang.org/doc/reference/latest/)([GitHub](https://github.com/leanprover/reference-manual))をご覧ください。
+
+原文にはライセンスが無かったため、原著者様より許諾をいただいて翻訳させていただいています。（[Zulip Chat](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Discussion.20thread.20for.20Lean.20Language.20Reference/near/478724278)）。
+
+誤字脱字・内容の誤りの指摘・フォークからのPull Request・フォークによる翻訳の改変等歓迎いたします。ご指摘は [当該リポジトリ](https://github.com/lean-ja/reference-manual-ja) にてIssue・Pull Requestで受け付けております。
+
+翻訳に際して、機械翻訳サービス [DeepL翻訳](https://www.deepl.com/ja/translator) を参考にしました。
 
+この翻訳は原文のcommit [2fbf58d9210323e4ebc0a002d9f761074da462cf](https://github.com/leanprover/reference-manual/commit/2fbf58d9210323e4ebc0a002d9f761074da462cf) に基づいています。
 
 ::::::draft
 

Manual.lean

@@ -1,34 +1,69 @@
-# Lean Language Reference
+# Lean Language Reference 日本語訳
 
-The Lean Language Reference is intended as a comprehensive, precise description of Lean. It is first and foremost a reference work in which Lean users can look up detailed information, rather than a tutorial for new users.
+* [原文](https://lean-lang.org/doc/reference/latest/)
+* [原文のソースコード](https://github.com/leanprover/reference-manual)
+* [対訳表](/GLOSSARY.md)
 
-This new reference has been rebuilt from the ground up in Verso. This means that all example code is type checked, the source code contains tests to ensure that it stays up-to-date with respect to changes in Lean, and we can add any features that we need to improve the documentation. Verso also makes it easy to integrate tightly with Lean, so we can show function docstrings directly, mechanically check descriptions of syntax against the actual parser, and insert cross-references automatically.
+## 翻訳する際のルール
 
+### 方針
 
-## Reading the Manual
+* なるべく直訳を心がける。
+* 読みやすさの観点から以下は直訳から変えて良い。 
+  * 文構造の変更
+    * 原文で1文だったところを2文に分ける
+    * 文の前半と後半を入れ替える
+  * 代名詞の明確化
+    * `it`や`that`等で記述されている中で読んだときにわかりづらそうな箇所
+  * 助動詞のニュアンスの変更
+    * `can`で書かれている文章で「～ができます」などの訳し方が日本語的に自然でない場合等
+  * 受動態⇔能動態
+    * 特に無生物主語だったり、主語がyouの場合など
+* 和訳箇所の前後や文脈に無い情報は基本的に入れない。
+* 訳注は以下の場合に記載する。
+  * 最新情報に対する記述が古くなっている場合
+  * 記述が間違っている場合
+  * 文意を把握するにあたって記述および情報が足りていない場合
 
-The latest release of this reference manual can be read [here](https://lean-lang.org/doc/reference/latest/).
+### 表記ルール
 
-For developers:
- * The output of building the current state of the `main` branch can be read [here](https://lean-reference-manual-review.netlify.app/).
- * Each pull request in this repository causes two separate previews to be generated, one with extra information that's only useful to those actively working on the text, such as TODO notes and symbol coverage progress bars. These are posted by a bot to the PR after the first successful build.
+* 文体は常に敬体（です・ます調）とする。
+* 英文をコメントアウトして、その直下に和訳を書く。
+* 和訳文を改行すると、その位置に空白が入ってしまうので段落内で改行しない。
+* 句読点には `、` `。` を用いる。
+* 英数字には半角を用いる。
+* 記号の全角・半角は『[JTF日本語標準スタイルガイド（翻訳用）](https://www.jtf.jp/tips/styleguide)』の「3 記号の表記と用途」に準拠する。
+  * 全角：`、` `。` `・` `：` `！` `？` `～` `（` `）` `「` `」` `『` `』`
+  * 半角：`/` `,`（数字の桁区切り）`.`（小数点）`-` `"` `` ` `` ` `（スペース）
+* 同格の語句の並列には中黒 `・` を用いる。
+  * カタカナ複合語の区切りには中黒を用いない。ただし、人名や熟語など、同格の語句の並列と誤解される可能性の低い箇所では中黒を用いてもよい。
+* 原文で `_` を用いて強調表示されている単語は、`**和訳単語**（元の英単語）`と訳す。ただし、専門用語ではない単語や、文が強調表示されている場合は、英語を併記しない。
+  * 原文例：`This pattern is called _structural recursion_.`
+  * 和訳例：`このパターンは**構造的再帰**（structural recursion）と呼ばれます。`
+* 3音以上のカタカナ語の末尾の長音記号「ー」は省く。
+* カタカナ語のままで違和感のない用語はカタカナ語のまま使う。
+* 原則として全角文字列とアルファベットまたはインラインコードとが隣接した場合は半角スペースを入れるが、見た目の字幅が小さな全角記号（`？` と `～` を除く全ての全角記号）の前後では半角スペースを入れない。
+  * 全角文字列と数字が隣接した場合も半角スペースを入れない。
 
-## Building the Reference Manual Locally
+## 翻訳に貢献したい方へ
 
-To build the manual, run the following command:
+* 競合を防ぐため、翻訳開始したとき、ファイルごとに draft PR を出してください。
+* 1つのPRに含める変更は少なめにしてください。
+
+## ローカルでのビルド方法
+
+1. TeX Live と Python をインストールする
+
+2. 下記コマンドでビルドする
 
 ```
 lake exe generate-manual --depth 2
 ```
 
-Then run a local web server on its output:
+3. 下記コマンドでローカルでサーバを立てる
+
 ```
 python3 -m http.server 8880 --directory _out/html-multi &
 ```
 
-Then open <http://localhost:8880> in your browser.
-
-## Contributing
-
-Please see [CONTRIBUTING.md](CONTRIBUTING.md) for more information.
-
+4. ブラウザで <http://localhost:8880> にアクセスする

README.md

@@ -0,0 +1,34 @@
+# Lean Language Reference
+
+The Lean Language Reference is intended as a comprehensive, precise description of Lean. It is first and foremost a reference work in which Lean users can look up detailed information, rather than a tutorial for new users.
+
+This new reference has been rebuilt from the ground up in Verso. This means that all example code is type checked, the source code contains tests to ensure that it stays up-to-date with respect to changes in Lean, and we can add any features that we need to improve the documentation. Verso also makes it easy to integrate tightly with Lean, so we can show function docstrings directly, mechanically check descriptions of syntax against the actual parser, and insert cross-references automatically.
+
+
+## Reading the Manual
+
+The latest release of this reference manual can be read [here](https://lean-lang.org/doc/reference/latest/).
+
+For developers:
+ * The output of building the current state of the `main` branch can be read [here](https://lean-reference-manual-review.netlify.app/).
+ * Each pull request in this repository causes two separate previews to be generated, one with extra information that's only useful to those actively working on the text, such as TODO notes and symbol coverage progress bars. These are posted by a bot to the PR after the first successful build.
+
+## Building the Reference Manual Locally
+
+To build the manual, run the following command:
+
+```
+lake exe generate-manual --depth 2
+```
+
+Then run a local web server on its output:
+```
+python3 -m http.server 8880 --directory _out/html-multi &
+```
+
+Then open <http://localhost:8880> in your browser.
+
+## Contributing
+
+Please see [CONTRIBUTING.md](CONTRIBUTING.md) for more information.
+