Crucible Tests

Crucible Test Framework

Crucible is a lightweight test framework for Lean 4 used across this workspace.

Quick Start

import Crucible
import MyProject  -- Import the code being tested

namespace MyProjectTests.ModuleTests

open Crucible
open MyProject

testSuite "Module Name"

test "descriptive test name" := do
  actualValue ≡ expectedValue

test "another test" := do
  someOption ≡? expectedValue  -- Option assertion

#generate_tests

end MyProjectTests.ModuleTests

Test Runner (Tests/Main.lean)

import Crucible
import MyProjectTests.ModuleTests
-- import all test modules

open Crucible

def main : IO UInt32 := runAllSuites

Assertions

Core Assertions

Collection Assertions

String Assertions

Exception Assertions

Comparison Assertions

Assertion Context

Test Fixtures (Setup/Teardown)

Use fixture hooks for shared setup and cleanup:

testSuite "Database Tests"

-- Runs once before all tests in the suite
beforeAll := do
  IO.println "Connecting to database..."

-- Runs once after all tests (even if tests fail)
afterAll := do
  IO.println "Closing database connection..."

-- Runs before each individual test
beforeEach := do
  IO.println "Starting transaction..."

-- Runs after each individual test (even if test fails)
afterEach := do
  IO.println "Rolling back transaction..."

test "insert works" := do
  -- database is set up, transaction started
  ...

test "query works" := do
  -- fresh transaction for this test
  ...

#generate_tests

Hook Behavior

Hooks are Optional

You can define any combination of hooks - they're all optional:

testSuite "Simple Tests"

-- Only define beforeEach if you need per-test setup
beforeEach := do
  resetGlobalState

test "test 1" := ...
test "test 2" := ...

#generate_tests

Timeouts and Retries

-- Per-test timeout (milliseconds)
test "slow operation" (timeout := 5000) := do
  slowFunction

-- Per-test retry count
test "flaky test" (retry := 3) := do
  flakyOperation

-- Both
test "network call" (timeout := 2000) (retry := 2) := do
  networkOperation

-- Global defaults in runner
def main : IO UInt32 := runAllSuites (timeout := 10000) (retry := 1)

Test File Structure

MyProject/
  lakefile.lean      # Add: lean_exe tests where root := "Tests/Main.lean"
  Tests/
    Main.lean        # Test runner with runAllSuites
    Core.lean        # Tests for Core module
    Parser.lean      # Tests for Parser module

lakefile.lean

require crucible from git "https://github.com/nathanial/crucible" @ "master"

@[default_target]
lean_lib MyProject

lean_exe tests where
  root := `Tests.Main

Common Patterns

Multiple assertions in one test

test "constructor preserves values" := do
  let obj := MyType.mk 1 "hello"
  obj.id ≡ 1
  obj.name ≡ "hello"

Testing IO operations

test "file operations" := do
  let content ← IO.FS.readFile "test.txt"
  content.length ≡ 42

Custom helper for domain-specific assertions

def colorApproxEq (c1 c2 : Color) (eps : Float := 0.001) : Bool :=
  floatNear c1.r c2.r eps && floatNear c1.g c2.g eps

test "color interpolation" := do
  let c := Color.lerp Color.red Color.blue 0.5
  ensure (colorApproxEq c expectedColor) "colors should match"

Testing error conditions

-- Simple: just verify it throws
test "throws on invalid input" := do
  shouldThrow (riskyOperation (-1))

-- Verify error message contains expected text
test "error message is descriptive" := do
  shouldThrowWith (parseNumber "abc") "invalid number"

-- Custom predicate for complex error checking
test "specific error type" := do
  shouldThrowMatching (networkCall) fun msg => msg.startsWith "NetworkError"

-- Verify operation succeeds (doesn't throw)
test "valid input succeeds" := do
  shouldNotThrow (parseNumber "42")

Adding context to assertions

test "user validation" := do
  let user := fetchUser "alice"
  (user.age ≡ 25) |> withContext "checking user age"
  (user.name ≡ "Alice") |> withContext "checking user name"
  (user.email ≡ "alice@example.com") |> withContext "checking email"

Multiple test suites in one file

namespace Tests.Core
testSuite "Core Types"
test "test 1" := ...
#generate_tests
end Tests.Core

namespace Tests.Parser
testSuite "Parser"
test "test 2" := ...
#generate_tests
end Tests.Parser

Organizing tests with section comments

testSuite "MyModule"

/-! ## Constructor Tests -/

test "default constructor" := ...
test "custom constructor" := ...

/-! ## Method Tests -/

test "method returns correct value" := ...

#generate_tests

Float Comparisons

Use floatNear (from Crucible) or shouldBeNear for floating point:

test "float calculation" := do
  let result := computePi
  shouldBeNear result 3.14159 0.00001
  -- or
  ensure (floatNear result 3.14159 0.00001) "pi approximation"

Running Tests

lake build tests && .lake/build/bin/tests
# or
lake test  # if configured in lakefile.lean