ExactTex: LaTeXの段階的型付けスーパーセット

［画像: ExactTeX］

PDFを確認する前に、ドキュメントが整合しているかを知る。

［画像: CI］ ［画像: MIT］ ［画像: zero dependencies］ ［画像: latest release］ ［画像: Rust 1.88 or newer］ ［画像: docs］

ExactTeXは、アノテーション（注釈）を追加できるLaTeXのスーパーセットです。チェックしたいオブジェクトに名前を付ければ、それ以外の部分は通常のLaTeXとして扱われ、変更されずにそのまま出力されます。.texファイルを.xtexにリネームしても、コンパイルは可能です。アノテーションは、必要に応じて多くても少なくても構いません。アノテーションを付けた部分がチェックされます。

私がExactTexを作成する際に念頭に置いた記事には、多くの要素（図、表、アルゴリズムなど）が含まれています。表の中で ef{tab:runtime}と書き、ラベルを able(tab:runtime_1)とした場合、コンパイラはPDFが間違った単語を出力する前にエラーをフラグ立てしますが、参照tab:runtimeが存在しないため、誰もそれに気づきません。それが私が期待していたことですが、LaTeXはそのようには機能しません。代わりに、PDFにはサイレントな??シンボルと、不可解なログメッセージが表示されます。まさに私が修正したかった点です。

WebAssemblyビルドに基づいたエディタであるVitelaで、ブラウザ上でExactTexを試すことができます。チェックはページ内でローカルに実行されます。

［画像: Vitela: 入力中に下線が引かれ、ホバーするとコンパイラの回答が表示される、スペルミスのある参照］

---

何をするのか

自分の言葉でエラーを表現。 ExactTeXは組版を行いません。xtex compileは、生成されたLaTeXを指定したエンジン（デフォルトはtectonic）に渡し、残された.logファイルを読み込み、各警告をソースマップ経由でそれを囲むエンティティにマッピングします。表が幅を取りすぎる場合、TeXは次のように言います。

Overfull \hbox (99.82014pt too wide) in paragraph at lines 7--10

ExactTexは次のように言います。

warning[TEX]: table `tab:wide` overflows its line by 99.82014pt
  TeX said: Overfull \hbox (99.82014pt too wide) in paragraph at lines 7--10
  emitted at build/wide.tex:7
  corresponds to wide.xtex:3:1

同じ事実を、あなたがテーブルに付けた名前で表現します。アノテーションはそのためにあります。ツールに名前を使わせるのです。

ファイル内のリビジョン。 Wordは.docx内に変更履歴を追跡して保持し、他のツールが編集を提案できるようにします。LaTeXにはそのような機能がなく、各ツールは独自の互換性のないレイヤーを構築します。ExactTexは変更モデルをファイル形式に組み込みます。提案された変更はドキュメント内のテキストです。

The gain is @sub(change:gain) {dramatic -> consistent} across both corpora.

ファイルは引き続きビルドされます。xtex build paper.xtex --markedは、変更されたテキストを取り消し線で、新しいテキストを色付きで表示して読みやすくします。

The gain is \textcolor{red}{\sout{dramatic}}\textcolor{blue}{consistent} across both corpora.

--originalと--finalは、変更がない状態と変更が適用された状態のドキュメントをビルドします。受け入れはソースの書き直しであり、受け入れられた変更はもはや変更ではありません。

xtex revise paper.xtex --accept change:gain

The gain is consistent across both corpora.

サイドカーファイルpaper.xtexrevには、誰がいつ変更を提案したかが記録されます。拒否すると、削除されたテキストがそのまま残るため、レビューで破棄された段落でも6ヶ月後に再度生成できます。共同執筆者、レビュー担当者、またはコーディングエージェントが提案できますが、著者のみが受け入れられます。モデルはdocs/revisions.mdにあります。

プレーンLaTeXを出力。 ジャーナルは.texファイルを受け取ります。このブロック：

\figure(fig:runtime) {
  src     = "figures/runtime.pdf"
  width   = 80%
  caption = {Runtime architecture for \emph{multi-agent} systems}
}

はxtex buildによって次のように出力されます。

\begin{figure}
  \centering
  \includegraphics[width=0.80\linewidth]{figures/runtime.pdf}
  \caption{Runtime architecture for \emph{multi-agent} systems}
  \label{fig:runtime}
\end{figure}

そして@ref(fig:runtime)は ef{fig:runtime}になります。アノテーションを付けなかった部分はコンパイラによってそのまま渡されるため、明日ExactTexの使用を停止した場合でも、生成されたファイルはそのまま保持できます。

---

試してみる

まだ事前ビルドされたバイナリはありません。Rustツールチェーン（1.88以降）があれば、1つのコマンドでコンパイラをビルドしてインストールできます。依存関係の取得は不要です。

cargo install --git https://github.com/camilochs/exacttex xtex-cli

次に、このリポジトリの例で試します。

git clone https://github.com/camilochs/exacttex
cd exacttex
xtex check examples/hello.xtex

coverage: 11.8%
bibliography: unavailable — the document declares no bibliography

ファイルは1つのセクションがアノテーションされた通常のLaTeXです。coverageはチェックされたドキュメントの割合です。次に参照のスペルミスをしてみましょう。@ref(sec:results)を@ref(sec:resutls)に変更して、再度チェックします。

error[XT1003]: identifier `sec:resutls` is not declared — did you mean `sec:results`?
  --> examples/hello.xtex:6:30
  entity: section
  name: sec:resutls
  span: offset 106, length 11
  --> examples/hello.xtex:4:22: `sec:results` is declared here
  blame: xtex-construct

プレーンLaTeXでは??と表示され、何も言わなかったでしょう。

リネームはコマンドで行い、プロジェクト全体で全ての参照を追跡します。

xtex rename paper.xtex sec:results sec:findings

paper.xtex: 1 renamed

エディタ内で。 言語サーバーを介して、入力中に同じチェックが実行されます。

cargo install --git https://github.com/camilochs/exacttex xtex-lsp

xtex-lspは標準入出力でLSPを話し、引数は取りません。.xtexファイルに対して、エディタの「カスタム言語サーバー」設定でこれを指定してください。キーストロークごと、ホバー、補完、定義へ移動、リネームに対して診断情報を返します。話すプロトコルは、メッセージごとにdocs/lsp.mdに記載されています。

---

見た目

\documentclass[11pt]{article}
\usepackage{amsmath}

\begin{document}
\section{Introduction}@id(sec:intro)

We argue the opposite in Section~@ref(sec:model), and
@cite(knuth1984) showed that cost grows with $n$.

The architecture is shown in Figure~@ref(fig:runtime).

\figure(fig:runtime) {
  src     = "figures/runtime.pdf"
  width   = 80%
  caption = {Runtime architecture for \emph{multi-agent} systems}
}

@import("sections/model.xtex")

Ordinary LaTeX keeps working: \emph{emphasis}, $E = mc^2$, \citep{blum2020}.
\end{document}

アノテーションには2つのレベルがあります。@id(x)は任意のLaTeX構造にアタッチされ、チェックされた参照とxtex renameを提供します。定理やアルゴリズムは、ExactTeXがそれらを認識しなくても機能します。igure(x)のような型付きブロックは、コンパイラにフィールドをチェックさせることもできます。例えば、画像が存在するか、キャプションがあるか、列数がtabularと一致するかなどです。

---

型システムは段階的

ドキュメントのほとんどは、コンパイラがモデル化しないLaTeXです。それが通常の状態で、言語はこのために構築されています。

各エンティティは、コンパイラが知っているクラスか、未知のオープン型である?Oのいずれかです。

xtex inventory paper.xtexは、ドキュメントごとのこのテーブルを表示します。各識別子につき1行で、そのクラス、参照数、宣言場所が示されます。

「オープン」が重要です。段階的型システムでは、?は「固定セット内の未知」を意味します。LaTeXには固定セットがないため、任意のパッケージが新しいコンストラクタを定義できるため、ここでの未知は無限です。この用語は、Malewski、Greenberg、TanterのGradually Structured Data（OOPSLA 2021）に由来します。

比較は、等価性ではなく整合性です。チェックポリシー全体は2行です。

Known(A) ~ Known(B)   if and only if A == B     <- this can fail
?O       ~ T          for every T               <- this never fails

?Oは全てのものと整合するため、モデル化されていないLaTeXが関わるものは失敗しません。?Oは、コンパイラが判断する根拠がなく、それ以上のものはないことを意味します。

これにより2つの結果が得られます。

.texファイルを.xtexにリネームして何も変更しない場合、全てのエンティティが?Oであるため、チェックはクリーンに完了します。これはドキュメントに適用された段階的保証（Siek、Vitousek、Cimini、Boyland、SNAPL 2015）であり、オンランプが機能する理由です。

アノテーションの量を自分で選択でき、コンパイラはその量を示します。xtex checkは、チェックされたドキュメントの割合であるカバレッジを表示します。これはanyやnoImplicitAnyのアナログです。トレンドは数よりも重要です。60%から30%になったファイルは、パーサーがモデル化できない何かを得たことを意味します。

型によって可能になり、LaTeXツールでは実行されない1つのチェックがあります。それは@ref(fig:main)が able(fig:main)を指す場合です。プレフィックスは図を示しますが、宣言はテーブルです。同様に、テーブル上のFigure~@ref(tab:main)も、文は図を示しますが、宣言はテーブルです。LaTeXは両方をコンパイルし、間違った単語を出力します。docs/checking.mdとdocs/decisions/0019を参照してください。

---

構築方法

［画像: ExactTeX architecture］

依存関係のない1つのコア。3つの薄いサーフェス（ターミナル、エディタ、ブラウザ）がそれを呼び出し、CIのパリティスイートがそれらの出力をバイト単位で同一に保ちます。アノテーションされていないバイトはパイプラインに入らず、その周りを渡されます。完全な説明はdocs/architecture.mdにあります。

外部検証（参考文献エントリ、URL、DOI、リポジトリをライブソースに対してチェック）は別のステップです。日付付きのレコードを作成し、コンパイラはそのレコードをオフラインで再生するため、コンパイルはネットワークに触れることはありません。docs/verification.mdを参照してください。

---

どのくらい初期段階か

コンパイラはまだ若いです。そして、はい、私はエージェントを使ってそれを構築しました。それらがなければ、数ヶ月かかったでしょう。しかし、デザインは私のものです。

---

ドキュメント

https://camilochs.github.io/exacttex/には、言語仕様、コンパイラがエラーと呼ぶもの、変更モデル、WebAssemblyおよびLSPサーフェス、そして証拠付きの全ての承認済み決定事項があります。同じページがdocs/にもあり、それぞれ1つのMarkdownファイルです。

コードを変更する者は誰でも、2つのドキュメントに拘束されます。PHILOSOPHY.md（何を主張できるか）とAGENTS.md（不変量とワークフロー）。

---

ライセンス

MIT。LICENSEを参照してください。

AF Labsプロジェクトです。