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

ドキュメントのPDFを見る前に、そのドキュメントが健全かどうかを確認できます。ExactTeXは、段階的なアノテーションを備えたLaTeXです。チェックしたいオブジェクトに名前を付ければ、名前を付けなかった部分は通常のLaTeXとしてバイト単位でそのまま転送されます。.texファイルを.xtexにリネームしても動作し続けます。そこから、どの程度アノテーションを付けるかを選択でき、アノテーションを付けた部分は保証されます。Vitelaで今日からブラウザ上でExactTeXを使用できます。VitelaはコンパイラのWebAssemblyビルド上に構築されたエディタで、同じチェック、診断、ナビゲーションがページ内でローカルに実行されます。現在の状況：コンパイラは動作しており、3つのインターフェース（ターミナル、エディタ、ブラウザ）が利用可能です。xtexはパース、チェック、LaTeX出力、ソースマップの書き込み、リビジョンの適用を行います。xtex-lspはエディタに診断、ホバー、補完、定義への移動機能を提供します。WebAssemblyビルドは、コンパイルサーバーなしで同じコアを任意のホストで実行します。パリティスイートは、3つのインターフェースを1つの回答にまとめます。以下のすべての主張は、構築されたものに関するものであり、各数値はそれを生成したコマンドで再現可能です。 何のためのものか 今日LaTeXができない2つのこと。 自分の言葉でのエラー。 ページに収まらないとき、LaTeXは次のように言います：「Overfull \hbox (12.3pt too wide) in paragraph at lines 45--47」。ExactTeXは次のように言います：「あなたのテーブル "results" は右マージンを12.3pt超えています paper.xtex:212 — 列3は宣言した幅に収まりません」。同じ事実を、オブジェクトに付けた名前を使って伝えます。これは、あなたがそれを宣言したからこそ機能します。それが構文の目的です。ツールに話させるための名前を与えます。 ファイル内に存在するリビジョン。 Wordは追跡された変更を.docx内に保存するため、ツールは編集を提案し、受け入れるか拒否できます。LaTeXには同等のものがないため、すべてのツールが独自のレイヤーを構築し、それらは相互運用できません。ExactTeXはモデルをフォーマットに組み込みます。 数分で試せます。 git clone https://github.com/camilochs/exacttex cd exacttex cargo run -p xtex-cli -- check examples/hello.xtex coverage: 11.8% bibliography: unavailable — the document declares no bibliography ファイルは通常のLaTeXですが、1つのセクションがアノテーション付けされています。メーターは、ドキュメントのどの程度が契約下にあるかを示します。ここで、参照を間違って入力してみてください — @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では、これは静かな「?」として表示されていました。 Rustツールチェーン（1.88以降）が必要です。コンパイラ自体は依存関係を一切取得しません。 見た目 \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構造に付加され、チェックされた参照と安全なリネームを可能にします — 定理やアルゴリズムは、ExactTeXがそれらを認識していなくても機能します。\figure(x) のような型付きブロックは、コンパイラにチェックすべきフィールドも提供します：画像は解決され、キャプションは存在し、列数は表と一致します。 型システムは段階的であり、それが設計全体です。 ドキュメントの大部分はLaTeXであり、コンパイラはそれをモデル化しません。これは修正されるべき欠陥ではありません。これは言語が構築されている状態です。すべてのエンティティは、コンパイラが知っているクラスか、未知のオープン型である ?O のいずれかです。 クラス Figure, Table (型付きブロック — \figure(fig:x), \table(tab:x)) Section, Appendix, Algorithm, Equation (@id をLaTeX構造に付加し、チェックされた参照と安全なリネームを可能にします) Citation (@cite、IDではなく参考文献に対してチェックされます) ?O それ以外のすべて xtexインベントリ paper.xtex は、あなたのドキュメントのためにそのテーブルを出力します：IDごとの1行、そのクラス、参照されている数、宣言されている場所。 「オープン」が負荷を支える言葉です。 段階的型システムにおける「?」は、「固定セット内の未知」を意味します。LaTeXには固定セットがありません — 任意のパッケージがいずれかの時点で新しいコンストラクタを定義できるため、ここでの未知は無制限です。この用語は、Malewski, Greenberg, Tanter の Gradually Structured Data (OOPSLA 2021) に由来します。 比較は等価性ではなく一貫性です。2行がチェックポリシー全体です。 Known(A) ~ Known(B) iff A == B <- これは失敗する可能性があります ?O ~ T (すべてのTに対して) <- これは決して失敗しません ?O はすべてと一貫性があるため、モデル化されていないLaTeXを含むものは何も一貫性がなく、モデル化されていないLaTeXを含むものは何も失敗しません。?O は無効性ではなく、根拠の欠如を示します。 明確に述べる価値のある2つの結果。 .tex を .xtex にリネームして何も変更しない場合、クリーンにチェックされます。なぜなら、すべてのエンティティが ?O だからです。これは、ケースバイケースの注意なしに、構築によって保持されます。これは、ドキュメントにインスタンス化された段階的保証 (Siek, Vitousek, Cimini, Boyland, SNAPL 2015) であり、オンランプを約束ではなく現実のものにします。 アノテーションをどの程度付けるかを選択すると、コンパイラが選択した量を示します。xtex check はカバレッジを報告します：チェックされたドキュメントの割合。これは、any や noImplicitAny のアナロジーです。この数値自体よりもその傾向が重要です：60%チェックされていたファイルが30%になった場合、それはパーサーがモデル化できないものを獲得したことを意味します。 型が提供するチェックであり、LaTeXツールは実行しません：@ref(fig:main) が able(fig:main) を指している — 接頭辞は図を要求しますが、宣言は表です。その兄弟：Figure~@ref(tab:main) が表を指している — 文章は図と言っていますが、宣言は表と言っています。LaTeXは両方をコンパイルし、間違った単語を出力します。詳細は docs/checking.md および docs/decisions/0019 を参照してください。 どのように構築されているか 依存関係ゼロのコア1つ。それ（コンパイラ）を呼び出す3つの薄いサーフェス（ターミナル、エディタ、ブラウザ）。CIでのパリティスイートによってバイト単位で同一に保たれます。転送保証は、アノテーションのないバイトは処理されず転送されるため、パイプラインの外側に配置されます。完全なウォークスルー：docs/architecture.md。 外部検証 — 参考文献エントリ、URL、DOI、リポジトリはライブソースに対してチェックされます — 独自のドアの後ろにあります：別のステップが日付付きのレコードを書き込み、コンパイラはそれをオフラインで再生するため、ネットワークはコンパイルに入りません。方法と理由：docs/verification.md。 何ではないか LaTeXをより短く書く方法ではありません。TypeScriptはJavaScriptよりも冗長ですが、タイプを少なくするために採用した人はいません。ツールがより多くを知るために、あなたはより多くを書きます。TeXを置き換えず、組版せず、LaTeXエコシステムを離れるように求めません。あなたのジャーナルは依然として.texファイルを受け取ります。 どれくらい新しいか コンパイラは新しく、そうでないふりをすることはあなたの時間を無駄にするでしょう。堅固なもの：転送保証 — 未変更のLaTeXはバイト単位で同一に出力される — は、ここで最も古い不変条件であり、最も頻繁にテストされています。チェッカー、エミッタ、および2つのサーフェス（WebAssemblyとLSP）は、同じ入力に対して同一に応答し、CIのパリティスイートがそれを維持します。100ページ強の本 — 40パッケージ、索引、章ごとの参考文献、TikZ — は、TeX Live全体と同じページ数にコンパイルされます。 まだデリケートな部分：変更モデル。2026年8月の実際の使用で1晩で3つの欠陥が表面化しました — \author{…} 内に書かれたリビジョンは、画面上では解決可能でしたが、PDFにはそのまま出力されました。 返信が、それが応答した変更よりも長く存続しました。 1つを拒否すると、余分なスペースが残りました。 これら3つはすべて同じもので、3つの側面から見られたものでした：ドキュメントがテキストをどこに運ぶかについて異なるルールを参照する2つのコードパス。それらは修正され、それぞれ前のコンパイラに対して失敗するテストがあり、tests/dialogues.rs は現在、タイトルページ、キャプション、ネストされたコマンド、テーブルセル、リストアイテムを通過する完全な会話を実行しています。それが正直な要約です：その部分