HTML で bussproofs スタイルの証明木を描画する JavaScript エンジンを作りました．

\begin{prooftree} \AXC{$1 + 2$} \AXC{$1 + 2 + 3$} \BIC{$1 + 2$} \AXC{$1 + 2 + 3$} \RightLabel{Label} \BIC{$1 + 2 + 3 + 4$} \end{prooftree}

  • ✓ 数式：KaTeX と一緒に使用できる！
  • ✓ 簡単：スクリプトタグを追加するだけで，証明がレンダリングされます．
  • ✓ マークダウン：markdown-preview.nvim との統合も提供されています．
  • ✓ スライド：Marp でも使用できます．
目次

使用方法

このツールを使うのは簡単です．

HTML の場合

HTML で bussproofs スタイルの証明木を描画するのは簡単です． HTML に以下の script タグを追加するだけでできます．

<script type="module">
  import { renderProofTreesOnLoad } from "https://sano-jin.github.io/bussproofs-html/assets/prooftree.js";
  renderProofTreesOnLoad();
</script>

サンプルの HTML ソースはこちらです: demo/sample.html

これをブラウザで開くと以下のようになります．

demo

サンプル HTML ファイルをデプロイしたページはこちらです: https://sano-jin.github.io/bussproofs-html/demo/sample.html

Neovim でマークダウンを編集している場合

あなたは Neovim を使っていますか？ Neovim はマークダウンを編集するのに最適なツール． markdown-preview.nvim を使えば，マークダウンをプレビューしながら編集できます．

私は markdown-preview.nvim をフォークし， この描画エンジンを統合しました． こちら がフォークしたプレビュワーです．

こんな感じで使うことができます． 素晴らしい！

demo

もし Lazy を Neovim のプラグインマネージャーとして使用している場合， 以下を設定に追加するだけでこのプレビュワーを使用できます．

-- Configuration for the forked previewer
  {
    "sano-jin/markdown-preview.nvim",
    cmd = { "MarkdownPreviewToggle", "MarkdownPreview", "MarkdownPreviewStop" },
    build = "cd app && yarn install",
    init = function()
      vim.g.mkdp_filetypes = { "markdown" }
    end,
    ft = { "markdown" },
  },

Marp でスライドを作っている場合

Marp はご存知ですか？ Marp はマークダウンからスライドを作ることができる非常に便利なツールです．

Marp では KaTeX を用いることで数式の描画も可能です． さらに，このツールを使えば，証明木もレンダリングできます．

こんな感じ． demo

Marp でこのツールを使うのは簡単です． HTML でレンダリングする際のものと同じ script タグを追加するだけで， このエンジンを使用できます．

例えば以下のようなマークダウンから証明木を含むスライドを作ることができます．

---
marp: true
math: katex
paginate: true
footer: https://github.com/sano-jin/bussproofs-html
---

# Marp との統合は簡単です！

ここに証明木があります:
\begin{prooftree}
\AXC{$1 + 2$}
\AXC{$1 + 2 + 3$}
\BIC{$1 + 2$}
\AXC{$1 + 2 + 3$}
\RightLabel{Label}
\BIC{$1 + 2 + 3 + 4$}
\end{prooftree}

<script type="module">
  import { renderProofTreesOnLoad } from "https://sano-jin.github.io/bussproofs-html/assets/prooftree.js";
  renderProofTreesOnLoad();
</script>

サンプルの Markdown はこちらです: demo/marp-sample.md

Marp を使って出力したスライド (PDF) はこちらです: demo/marp-sample.pdf

VSCode を使っている場合

私は VSCode に詳しくないので，まだ統合プランを検討していません．

進展があれば，PR を送ってください．

現在の仕様

  • p 要素の直下にある証明木のみが描画されます．
  • 現在のところ，ラベルには \RightLabel のみ使用可能です．
  • Bussproofs のコマンドとして使用できるのは， \AXC，\UIC，\BIC，\TIC，および \QuaternaryInfCのみです．
  • \normalsize，\small，\footnotesize，\scriptsize，および \tiny は無視されます．
  • その他の LaTeX コマンドがあった場合はエラーとなります．

[!NOTE]
bussproofs-html__で始まる CSS クラス名は予約されています．

もしも他の機能を実装したら，PR を送ってください．

設定オプション

証明木のレンダリングの際に，もっとあなたの美的感覚を活かすこともできます． 例えば推論の横線が横に飛び出る長さをゼロにしたいとか．

以下のように定義された configP 型を持つオプションを， renderProofTreesOnLoadおよびrenderProofTreesに渡すことができます．

interface configP {
  // 前提条件間の余白（デフォルトは20）．
  marginPremises?: number;

  // 公理と結論の左および右のパディング（デフォルトは20）．
  paddingAxiomConclusion?: number;

  // ラベルの左余白（デフォルトは10）．
  marginLabelLeft?: number;

  // スタイルの適用タイミング：ロード後（nullの場合）または手動で設定したタイムアウト後（数値の場合）（デフォルトはnull）．
  styleOnLoad?: null | number;
}

例えば，次のように設定すると， 前提条件間の余白が 100px， 公理と結論の左右のパディングが 0px， ラベルの左余白が 0px になり， スタイルは 100 ミリ秒後に適用されます．

renderProofTreesOnLoad({
  marginPremises: 100,
  paddingAxiomConclusion: 0,
  marginLabelLeft: 0,
  styleOnLoad: 100,
});

demo

開発者向け

このツールはオープンソースで，github で公開しています．

https://github.com/sano-jin/bussproofs-html

改善点が見つかりましたか？ PR を送って私を助けてください．

ビルド方法

開発:

cd proof-tree
yarn dev
# 表示されたURLにブラウザからアクセス．

デプロイ:

cd proof-tree
yarn build
cd ..
cp proof-tree/dist/index.js docs/assets/prooftree.js

ロードマップ

以下のロードマップがあります． 進展があれば，PR を送ってください．

  1. \LeftLabelを有効化する．
  2. VSCode との統合を追加する．
  3. スタイリングプロセスを強化する．
    • このツールでは証明木を美しくスタイルするために二回に分けて描画を行っています． まずは証明木の DOM を作り，特にその各ノードの位置などの調整は行わずにレンダリングします． 次に，証明木の各ノードの幅を取得し，各ノードの位置や推論の横線の長さなどを計算して， スタイルを反映させます．
    • 現在，スタイリング（二回目のレンダリング）のタイミングには 2 つのオプションがあります：
      • A: loadイベント後にスタイルを適用する．
      • B: 証明木の DOM 要素の挿入後，指定されたミリ秒後にスタイルを適用する．
    • (B) DOM 要素の挿入後，指定されたミリ秒後にスタイルを適用するのは，正確なレンダリング時間を予測できないため，堅牢な方法ではありません．レンダリング完了前にスタイルを適用しようとすると，期待通りの結果が得られません．
    • (A) loadイベント後にスタイルを適用する方法は，私の理解では DOM コンテンツが完全にレンダリングされた後に発生するため，より堅牢な方法です．しかし，markdown-preview.nvim との統合など，いくつかのケースではうまく機能しないようです．より深い理解が必要です．
  4. 最初のバージョンをリリースする．

まとめ

きっと便利だと思うので，是非使ってみてください．

もし改良したら PR を送ってください．