Projects, Tests, and Tools

Learn the basic workflow for growing a program.

12.1 Split files and import definitions

A small program can fit in one .taut file. As it grows, split it within src/. Imports use paths relative to the importing file.

src/math.taut

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

// Export the addition function for another source file.

✓ Check passed

・ add

src/main.taut

import "math.taut"

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

// Import the helper and observe its result.

Execution result

result = 42

tauto run --tote .

result = 42

src/ is an implicit source root. Declare extra roots in additional-sources in Tauto.eure. Standard-library definitions use the same import syntax (Chapter 6).

12.2 Everyday commands

Command	Purpose
`tauto init PATH`	Create a project
`tauto run --tote .`	Evaluate a project
`tauto check FILE`	Check proof declarations with the kernel
`tauto check FILE --fresh`	Check again without using the cache
`tauto fmt FILE`	Format source code
`tauto lint FILE`	Check style rules
`tauto test PATH`	Run tests in `tests/` and `cases/`
`tauto doc PATH`	Generate local HTML documentation

tauto fmt uses two-space indentation, as do the examples in this book.

tauto check checks proofs of propositions as well as program types, effects, and ownership. skipped means a declaration is outside the proof kernel's scope; it does not mean that program checking was omitted. Use run and tests to observe actual values and effects.

12.3 Tests

tauto test discovers and runs a project's tests/ and cases/. A .taut file in tests/ must first pass proof checking without holes, then be evaluated. Neither show nor print is an assertion. Declare expected output in an Eure case file.

tests/add.taut

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

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

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

// Combine a checked equality theorem with an executable observation.

Execution result

✓ theorem add_ok : 2 + 2 = 4

x = 42

tauto test .

passed tests/add.taut
1 passed; 0 failed

12.4 Tools for developing proofs

During a proof, inspect the propositions that remain unproved: the goals. Leave a named hole ?name for an unfinished part.

ch12-holes.taut

import std::Base

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

// Leave named holes to inspect the two remaining propositions.

… Remaining goals

… 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

A declaration containing holes is not accepted. It is reported as INCOMPLETE with exit code 3; there is no bypass such as 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 checks a candidate expression for a hole without editing the file; tauto fill writes it into the file.

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

Other tools include tauto check FILE --json, which reports results and each declaration's axioms; tauto library FILE, which lists available theorems and constructors; and tauto suggest FILE --hole NAME, which searches for suitable candidates.

Exercise 12.1: Create a project and practice choosing between fmt, run, test, and check.