プロジェクト・テスト・ツール

大きなプログラムに育てるときの、基本の作業を見ます。

12.1 ファイルの分割と import

小さなプログラムは、一つの .taut ファイルで十分です。大きくなったら src/ の中で分割します。取り込みは、そのファイルからの相対パスです。

src/math.taut

pub fn add(a: i64, b: i64): i64 {
  a + b
}

✓ 検査を通過

・ add

src/main.taut

import "math.taut"

let x := add(20, 22)
perform show("result", x)

実行結果

result = 42

tauto run --tote .

result = 42

src/ は暗黙のソースルートです。追加のソースルートは、マニフェスト Tauto.eure の additional-sources に指定します。標準ライブラリを読み込むときも、同じ import を使います（第 6 章）。

12.2 普段使うコマンド

コマンド	何をするか
`tauto init PATH`	新しいプロジェクトを作る
`tauto run --tote .`	プロジェクトを評価する
`tauto check FILE`	証明宣言をカーネルで検査する
`tauto check FILE --fresh`	キャッシュを使わずに検査し直す
`tauto fmt FILE`	ソースコードを整形する
`tauto lint FILE`	スタイル上の規則を検査する
`tauto test PATH`	`tests/` と `cases/` のテストを実行する
`tauto doc PATH`	ローカルの HTML ドキュメントを作る

tauto fmt は 2 スペースのインデントに整形します。この本のコードも、それに合わせています。

tauto check は、命題の証明と、実行するプログラムの型・effect・所有権を検査します。 skipped は、その宣言が証明カーネルの対象ではないことを表し、プログラム側の検査まで省略したという意味ではありません。実際の値や副作用は run とテストで確認します。

12.3 テスト

tauto test は、プロジェクトの tests/ と cases/ を探して実行します。tests/ の .taut ファイルは、まず証明検査を通り（穴が残っていてはいけません）、次に評価されます。show や print は表明（アサーション）ではありません。出力の期待値は、Eure の case ファイルに書きます。

tests/add.taut

import std::Base
import "../src/math.taut"

theorem add_ok(): (2: Nat) + 2 = 4 {
  Refl
}

perform show("x", add(20, 22))

実行結果

✓ theorem add_ok : 2 + 2 = 4

x = 42

tauto test .

passed tests/add.taut
1 passed; 0 failed

12.4 証明を支援するコマンド

証明の途中では、まだ証明されていない命題（ゴール）を確認できます。証明の一部を、名前付きの穴 ?name にしておきます。

ch12-holes.taut

import std::Base

theorem and_comm(A: Prop, B: Prop, p: A ∧ B): B ∧ A {
  AndIntro(?right, ?left)
}

… 残っているゴール

… theorem and_comm : ∀ A: Prop. ∀ B: Prop. (And(A, B)) -> And(B, A)

?right  (4:12)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ B

?left  (4:20)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ A

穴を含む宣言は、受理されません。INCOMPLETE と報告され、終了コードは 3 です（sorry のような抜け道はありません）。

tauto check ch12-holes.taut
tauto goals ch12-holes.taut

INCOMPLETE and_comm (?right, ?left)
?right in and_comm (ch12-holes.taut:2:15)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ B
?left in and_comm (ch12-holes.taut:2:23)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ A

穴に式を入れて検査だけしてみるのが tauto try、実際にファイルへ書き込むのが tauto fill です。

tauto try ch12-holes.taut --hole right --with 'And::right(p)'
tauto fill ch12-holes.taut --hole right --with 'And::right(p)'
tauto fill ch12-holes.taut --hole left --with 'And::left(p)'
tauto check ch12-holes.taut

ok      and_comm

ほかにも、検査結果を JSON で受け取る tauto check FILE --json（各宣言が使った公理も含みます）、使える定理や構成子の一覧を出す tauto library FILE、穴に合う候補を探す tauto suggest FILE --hole NAME があります。

演習 12.1：プロジェクトを一つ作って、fmt・run・test・check を使い分けてみましょう。