stacksプロジェクト

blitの原点ともいえるgerbyによるstacksプロジェクトを見ると:

  1. bibエントリーから逆ポインタがある。
  2. 参照は、ジャンプと切り取り引用がある。セクションにはジャンプ、remarkは切り取り引用。
  3. セクション間のナビゲーションは next, prev とパンくずリスト
  4. lemmaはタイトル〈ラベル〉をクリックすると自分自身を切り取り引用する。
  5. sloganというtooltipがある。
  6. lemmaの切り取りは証明を含む。
  7. ひとつ上の階層のナビゲーションリンクはないようだ。パンくずリストで間に合う。
  8. 切り抜きブロックのあいだのナビゲーションもある。next, prev
  9. 切り抜きブロックから親にもどるナビゲーションリンクはないようだ。ちょっと不便。
  10. webページは基本セクション単位。エントリーと言ってもいい。
  11. 定義ブロック内で定義される用語はイタリックだが、それ以上の構造はない。
  12. 記法定義を識別・参照する方法がない。記法定義は定義に含まれないで、本文(フィラー)になる。
  13. exampleは識別できるが、何の事例かが辿れない。
  14. 定義内に記法が含まれる場合もある。が、記法だけを識別・参照できない。
  15. 概念の定義〈指標〉と実例〈モデル〉がそれほど明確ではない。
  16. セクションとブロックは区別されていて、ブロックは切り抜き可能で、ブロックのあいだのナビゲーションが出来る。ブロックはセクションの下にぶら下がる。
  17. Gerbyタグはブロックを識別する。
  18. 「Lemma 9.4.1. If k is a field, then every k-module is free.」、これなら、"field", "k-module", "free" からの参照が欲しいが、それは出来ない。
  19. 「Proof. This follows from Lemma 9.4.1 as every vector space is a projective module.」、ここで "Lemma 9.4.1" からのリンクはある。
  20. "the category of k-modules" で "category" はイタリックだが、リンクはない。
  21. "a so-called abelian category." で、地の文で用語定義がされている。
  22. ブロックは、definition, example, lemma/theorem+proof, exercise
  23. 地の文、ナラティヴが何の役割を演じているのか、ちょっと分からない。
  24. ページの下部にもナビゲーションリンクがあるといい。
  25. 「Definition 9.9.1. The polynomial P above is called the minimal polynomial of α over k.」が切り抜きブロックになるが、above があるので切り抜きだけでは意味不明。
  26. タグによって参照されるブロックも「タグ」と呼んでいるようだ。
  27. タグ=ID で、タグにステートメントと証明が付随して。タグごとに履歴を管理している。

gerbyのタグはIDのことだが、タグを付けられる対象物は:

  • 'definition'
  • 'lemma', 'proposition', 'theorem'
  • 'equation' 単一の命題のことだろう、formula でもいいかも
  • 'remark', 'remarks'
  • `example'
  • 'exercise'
  • 'situation' 記述のセットアップのことか?
  • 'section', 'subsection', 'subsubsection', 'item'

ルーリーのKerodonでは、次の統計情報〈Statistics〉がある。

type count
definition 292
example 651
exercise 115
lemma 108
proposition 666
theorem 82
question 11
remark 1079
part 3
chapter 9
section 50
subsection 294

この統計情報には、

  • notation が入ってない
  • construction が入ってない
  • warning が入ってない

また、

  • equation は使ってないようだ。
  • slogan は使ってないようだ。
  • future reference (参照先が存在しない参照)がある