agda-zh / plfa-zh Goto Github PK

At https://travis-ci.org/Agda-zh/PLFA-zh/jobs/559531094#L863, the jekyll report:

ruby -S bundle exec jekyll build
Configuration file: /home/travis/build/Agda-zh/PLFA-zh/_config.yml
            Source: /home/travis/build/Agda-zh/PLFA-zh
       Destination: /home/travis/build/Agda-zh/PLFA-zh/_site
 Incremental build: disabled. Enable with --incremental
      Generating... 
       Jekyll Feed: Generating feed for posts
  Liquid Exception: Liquid syntax error (line 78): Unknown tag 'endraw' in out/tspl/2018/Assignment4.md
jekyll 3.8.5 | Error:  Liquid syntax error (line 78): Unknown tag 'endraw'
make: *** [build] Error 1
The command "make test-offline" exited with 2.

But in my local environment there is no such error.
(instead a htmlproofer 3.11.0 | Error: HTML-Proofer found 739 failures!, while it's another problem ╮(╯▽╰)╭)

Do you have any idea? @wenkokke

官方文档中会自动在代码内跳转链接前加上 https://agda.github.io/agda-stdlib/ 前缀，而我们的文档由于没有任何前缀会导致跳转时在当前 URL 下寻找文档。有人知道生成文档这块是哪里控制的吗？

• 初译
• 初校

• 初译
• 初校

• README #4
• Index #5

Front matter

• Dedication
• Preface #13

Part 1: Logical Foundations

• Naturals #3
• Induction #15
• Relations #17
• Equality #20
• Isomorphism #22
• Connectives #24
• Negation #35
• Quantifiers #44
• Decidable #46
• Lists #49

Part 2: Programming Language Foundations

• Lambda #168
• Properties #169
• DeBruijn #166
• More #167
• Bisimulation #165
• Inference #164
• Untyped #163
• Confluence #171
• BigStep #170

Part 3: Denotational Semantics

• #172
• #173
• #174
• #175
• #176

Backmatter

• Acknowledgements
• Fonts
• Statistics

• 初译
• 初校

• 初译
• 初校

Missing translators. See https://tex.stackexchange.com/a/19709/145304 for formatting

Originally posted by @ice1000 in #69

• 初译
• 初校

• 初译
• 初校

翻译原则可参考 Agda/Idris 文档翻译规范。

段落翻译

翻译通常以段落为基本单位。译者将原文围在 <!-- 和 --> 之间注释掉后，在下方空一行再进行翻译。考虑到中文斜体的渲染问题，英文原文中出现的 _text_ 在翻译时需改为 **文本**，特殊格式需要在两侧留下空格以便正确解析。例如：

<!--
Now that we've defined the naturals and operations upon them, our next
step is to learn how to prove properties that they satisfy.  As hinted
by their name, properties of _inductive datatypes_ are proved by
_induction_.
-->

现在我们定义了自然数及其运算，下一步是学习如何证明它们满足的性质。
如其名称所示，**归纳数据类型（inductive datatype）**是通过**归纳（induction）**
来证明的。

术语翻译

文档中的术语请参考术语表，术语在正文中第一次出现时，如果是名词，需要在后面的括号中注明英文原词，首字母大写；如果不是名词，则为小写；标题中不添加英文。常见术语一般无需添加原词。示例见上。

标点符号

为了排版美观，中文和英文、数字之间要留有空格，中文标点和英文、数字之间无需空格。例如：

<!--
We require equality as in the previous chapter, plus the naturals
and some operations upon them.  We also import a couple of new operations,
`cong`, `sym`, and `_≡⟨_⟩_`, which are explained below:
-->

我们需要上一章中的相等性，加上自然数及其运算。我们还导入了一些新的运算：
`cong`、`sym` 和 `_≡⟨_⟩_`，之后会解释它们：

列表翻译

为了让源码中的上下文更加紧凑，较短的列表一般整块注释掉后再在下方翻译；如果列表前的段落不长且后跟冒号，则可一并注释。例如：

<!--
* _Identity_.   Operator `+` has left identity `0` if `0 + n ≡ n`, and
  right identity `0` if `n + 0 ≡ n`, for all `n`. A value that is both
  a left and right identity is just called an identity. Identity is also
  sometimes called _unit_.

* _Associativity_.   Operator `+` is associative if the location
  of parentheses does not matter: `(m + n) + p ≡ m + (n + p)`,
  for all `m`, `n`, and `p`.

* _Commutativity_.   Operator `+` is commutative if order of
  arguments does not matter: `m + n ≡ n + m`, for all `m` and `n`.

* _Distributivity_.   Operator `*` distributes over operator `+` from the
  left if `(m + n) * p ≡ (m * p) + (n * p)`, for all `m`, `n`, and `p`,
  and from the right if `m * (p + q) ≡ (m * p) + (m * q)`, for all `m`,
  `p`, and `q`.
-->

* **幺元（Identity）**。对于所有的 `n`，若 `0 + n ≡ n`，则 `+` 有左幺元 `0`；
  若 `n + 0 ≡ n`，则 `+` 有右幺元 `0`。同时为左幺元和右幺元的值称简称幺元。
  幺元有时也称作**单位元（Unit）**。

* **结合律（Associativity）**。若括号的位置无关紧要，则称运算符 `+` 满足结合律，
  即对于所有的 `m`、`n` 和 `p`，有 `(m + n) + p ≡ m + (n + p)`。

* **交换律（Commutativity）**。若参数的位置无关紧要，则称运算符 `+` 满足交换律，
  即对于所有的 `m` 和 `n`，有 `m + n ≡ n + m`。

* **分配率（Distributivity）**。对于所有的 `m`、`n` 和 `p`，若
  `(m + n) * p ≡ (m * p) + (n * p)`，则运算符 `*` 对运算符 `+` 满足左分配率；
  对于所有的 `m`、`n` 和 `p`，若 `m * (p + q) ≡ (m * p) + (m * q)`，则满足右分配率。

代码块翻译

一般来说，代码块直接跳过不用翻译。不过有时代码块中包含需要翻译的注释，因此请整块注释掉后再进行翻译。例如：

<!--
```
-- Your code goes here
```
-->

```
-- 请将代码写在此处。
```

• 初译
• 初校

在markdown转换成HTML的过程中，换行符会变成空格。在英文里这样做没有问题，但是在中文里就产生了额外的空格。

• 初译
• 初校

• 初译
• 初校

I noticed that on the citation page, the references and the BibTeX do not include the translators. I feel you should add these! This might be as simple as adding translators in the appropriate places, as I've done below, but it probably makes sense to translate the titles in their entirety.

Wadler, Philip and Wen Kokke. Programming Language Foundations in Agda. Translated by Fangyi Zhou, Oling Cat, and Rongxiao Fu. Available at https://agda-zh.github.io/PLFA-zh/. 2019.

@Book{plfa2019,
  author     = {Philip Wadler and Wen Kokke},
  title      = {Programming Language Foundations in {A}gda},
  translator = {Fangyi Zhou and Oling Cat and and Rongxiao Fu},
  note       = {Available at \url{https://agda-zh.github.io/PLFA-zh/}},
  year       = 2019,
}

• 初译
• 初校

• 初译
• 初校

• 初译
• 初校

按照原文，译文中此处≡-reasoning和≤-reasoning或许应该是≡-Reasoning和≤-Reasoning

• 初译
• 初校

• 初译
• 初校

• 初译
• 初校

需要解决大量的冲突，应该是个不小的工作量。不过咱倒是有这方面的经验。

• 初译
• 初校

In part1/Relations.lagda.md
First,

反演
In our definitions, we go from smaller things to larger things. For instance, from m ≤ n we can conclude suc m ≤ suc n, where suc m is bigger than m (that is, the former contains the latter), and suc n is bigger than n. But sometimes we want to go from bigger things to smaller things. {:/}

This paragraph was not commented.

Second,

≤-trans (s≤s m≤n) z≤n 不可能发生，因为第一个不等式告诉我们中间的数是一个 suc n， 而第二个不等式告诉我们中间的**书**是 zero。Agda 可以推断这样的情况不可能发现，所以我们不需要 （也不可以）列出这种情况。

"书" need to be changed to "数".

• 初译
• 初校

• 初译
• 初校

https://github.com/Agda-zh/PLFA-zh/blob/dev/src/plfa/part1/Quantifiers.lagda.md?plain=1#L353

此处写道“积是依赖积的一种特殊形式”，原文为“Products arise as a special case of existentials”。

应该更正为“积是存在量词的一种特殊形式”。

https://plfa-zh.github.io/ 和 https://agda-zh.github.io/PLFA-zh/ 的显示并不一致，但差不多都是同一时间部署的。https://plfa-zh.github.io/ 看起来更旧一些，似乎用了旧的缓存？

咱注意到 https://github.com/Agda-zh/PLFA-zh/blob/dev/.travis.yml 里对两个 repo 的部署用到了同一个 GITHUB_TOKEN，应该是现在这个 repo 的。我们似乎应该给 https://github.com/plfa-zh/plfa-zh.github.io 再生成一个 Token？

好吧跟 GITHUB_TOKEN 无关。

有人问这两个 URL 访问哪一个才对？为避免混乱，或许我们应该只保留 https://plfa-zh.github.io/ ，本 repo 不再开启 GitHub Pages 并删除 master 分支。

@roger-uw

• 初译
• 初校

• 初译
• 初校

• 初译
• 初校

• 初译
• 初校

• 初译
• 初校

• 初译
• 初校

https://agda-zh.github.io/PLFA-zh/plfa.pdf

现在中文字符全部显示为方框，我试着更换中文字体，然而所有的 Unicode 字符却变成了方框。

可能有用的方法：
https://tex.stackexchange.com/questions/514940/define-fallback-font-for-missing-glyphs-in-lualatex

epubcheck will complain about -- in comments, which is a requirement of XHTML/XML. This is particularly annoying, since we put original text in English in comments, and sometimes they involve -- in a number of places. I've made a temporary fix in 7ed0e5d but probably we want a long term solution.

• 初译
• 初校

• README #4
• Index #5

Front matter

• Dedication
• Preface #13

Part 1: Logical Foundations

• Naturals #3
• Induction #15
• Relations #17
• Equality #20
• Isomorphism #22
• Connectives #24
• Negation #35
• Quantifiers #44
• Decidable #46
• Lists #49

由于官方已经迁移到了 Agda 2.6.0，使用 lagda.md 格式，去掉了 agda2html，因此我们终于可以肆无忌惮地用译注和 ruby 标签了！jekyll 已经有了一个很方便的扩展 jekyll-furigana 可用，我们应该只需要替换掉就可以了。

• 初校
• 初译

• 初译
• 初校

考虑到原版的PLFA并未提供官方的PDF版，请问中文翻译版能否提供官方的PDF。

是否需要将正文部分的中文引号统一为 '「」' 或 '“”' ？
目前部分译文出现了混用现象

• 初译
• 初校