Skip to content
This repository has been archived by the owner on Jan 5, 2025. It is now read-only.

Commit

Permalink
翻訳準備 (#1)
Browse files Browse the repository at this point in the history
* 翻訳準備

* CIスクリプト修正
  • Loading branch information
s-taiga committed Jan 4, 2025
1 parent 4ca9921 commit b4f9a25
Show file tree
Hide file tree
Showing 6 changed files with 137 additions and 110 deletions.
97 changes: 24 additions & 73 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,16 @@ 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 check HTML"

Expand Down Expand Up @@ -122,77 +126,24 @@ jobs:
fail: true
args: --base './_out/html-multi/' --no-progress --offline './_out/html-multi/**/*.html'

# This saved number is used by a workflow_run trigger. It
# manages labels that indicate the status of the built HTML.
- name: Save PR number
if: github.event_name == 'pull_request'
run: |
mkdir -p ./pr
echo ${{ github.event.number }} > ./pr/NR
- uses: actions/upload-artifact@v4
if: github.event_name == 'pull_request'
- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
name: pr
path: pr/

path: _out/html-multi

# Deployment job
deploy:
name: Deploy release
if: github.ref == 'refs/heads/main'
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
needs: [build]
if: github.event_name == 'release'
outputs:
ref-url: ${{ steps.deploy-release.outputs.deploy-url }}
needs: build
steps:
- name: Get generated HTML from artifact storage
uses: actions/download-artifact@v4
with:
name: 'html'
path: '_out/'

# 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/actions-netlify@v2.0
if: github.event_name == 'release'
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"

- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4


check-links:
name: Check links
Expand Down
20 changes: 0 additions & 20 deletions .github/workflows/pr-title.yml

This file was deleted.

10 changes: 10 additions & 0 deletions GLOSSARY.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
# 対訳表

| 英語 | 日本語 |
| --- | --- |


# 英語表現をそのまま用いている単語

| 用語 |
| --- |
17 changes: 17 additions & 0 deletions Manual.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,11 +22,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 intended for new users.
Expand Down Expand Up @@ -149,7 +156,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

Expand Down
69 changes: 52 additions & 17 deletions README.md
Original file line number Diff line number Diff line change
@@ -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> にアクセスする
34 changes: 34 additions & 0 deletions README.origin.md
Original file line number Diff line number Diff line change
@@ -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.

0 comments on commit b4f9a25

Please sign in to comment.