This document provides essential information for agentic coding assistants working on the REPLica codebase.
REPLica is a CLI golden testing framework written in Idris2. It allows testing command-line interfaces by comparing actual output against "golden values" (expected outputs stored in files). The project supports test organization via suites and tags, test dependencies, and file-based expectations.
- Idris2 v0.8.0 or later
- Dhall and dhall-to-json (for configuration processing)
- Git (for version control)
- Recommended: nix flakes for reproducible development environment
# Full development setup
nix develop # Drop into dev environment with all dependencies
# Build the project
make build # Compile Idris2 project -> build/exec/replica
# Install locally
make install # Copy replica binary to ~/.local/bin/
# Run all tests (using current build)
make test # Runs all tests from tests.dhall against current version
# Update test golden values
make generate # Run tests in interactive mode to update expectations
# Clean build artifacts
make clean # Remove build/ directory
make clean-test # Remove generated .json test files
# Run tests with stable replica version
REPLICA_EXE=/path/to/replica make test # Use specific replica binary
# Run nix checks (linting, testing)
nix flake check # Complete CI-like validation# Generate JSON from Dhall test file
dhall-to-json --file tests/replica/simple/tests.dhall --output tests/replica/simple/tests.json
# Run specific test file
./build/exec/replica run tests/replica/simple/tests.json
# Run with filtering
./build/exec/replica run -t tag_name tests/replica/simple/tests.json # Include tests with tag
./build/exec/replica run -T tag_name tests/replica/simple/tests.json # Exclude tests with tag
./build/exec/replica run -s suite_name tests/replica/simple/tests.json # Run specific suite
# Interactive mode (updates golden values)
./build/exec/replica run --interactive tests/replica/simple/tests.json
# Get help
./build/exec/replica helpsrc/Replica/
├── Replica.idr # Entry point, arg parsing, exit codes
├── App/ # Application logic (run, info, new, set commands)
├── Command/ # Command parsers and handlers
├── Core/ # Core types and test parsing
├── Option/ # CLI option parsing and filtering
└── Other/ # Utilities (Validation, Decorated, Free, String)
tests/ # Test files
├── replica/ # Replica's own test suite (Dhall)
└── Meta/ # Common test utilities and types
.replica/test/ # Golden test expectations and outputs
- Language: Idris2 (functional with dependent types)
- Default Totality:
%default totalis used in most modules- Functions must be proven total (terminating, covering all cases)
- Use
coveringfor partial functions (with explicit justification) - Pattern matching must be exhaustive
- Type Safety: Leverage the type system for correctness (use
So, dependent pairs, etc.)
- Top-level comments: Use triple-pipe comments (
|||) for module documentation - Imports: Group by purpose (standard library → local)
module Replica.Core.Types import Data.String import Data.List import Language.JSON import Replica.Core.Types
- Exports: Use
public exportfor public API,exportfor helper functions - Module re-exports: Use
import publicto expose submodule APIs (seeReplica.App)
- Types/Records:
CamelCase(e.g.,Test,Expectation,ReplicaError) - Functions:
camelCase(e.g.,parseArgs,runTest,displayExit) - Type constructors:
CamelCase(e.g.,Ordered,StdOut,Generated) - Record fields:
camelCasewith dot notation (e.g.,test.name,ctx.global) - Module names:
CamelCasewith dot hierarchy (e.g.,Replica.App.Run)
Use record syntax for complex data with named fields:
record Test where
constructor MkTest
name: String
pending : Bool
description: Maybe String
-- ... other fieldsUse union types (sum types) for variants:
data Expectation
= Exact String
| StartsWith String
| Partial OrderSensitive (List String)
| GeneratedUse dependent types to encode invariants (e.g., So (not $ n == 0) ensures non-zero).
-
Validation Accumulation: Use
Validation err afromReplica.Other.Validationfor collecting multiple errors:validateField : String -> Validation (List String) Field validateField x = if valid x then Valid (field x) else Error ["Field invalid"]
-
Custom Error Types: Define error sum types and implement
Show:data ReplicaError = CantAccessTestFile String | InvalidJSON (List String) Show ReplicaError where show (CantAccessTestFile s) = "Can't access: \{s}" show (InvalidJSON errs) = "JSON errors: \{show errs}"
-
Exit Codes: Map errors to explicit exit codes in
exitCodefunctions (seeReplica.idr) -
Error Propagation: Use
EitherandValidationfor recoverable errors; reserve exceptions for unrecoverable failures
- Line length: Target 100 characters (soft limit)
- Indentation: 2 spaces (consistent throughout codebase)
- Comments: Use triple-pipe (
|||) for top-level documentation,--for inline - String interpolation: Use
\{var}syntax for embedding values - Whitespace: Single blank lines between definitions, double for major sections
- Function composition: Chain operations with
>>,<*>, etc. when appropriate - Record updates: Use
{field := value}syntax for non-destructive updates - Effect handling: Use
Control.Appmonads (seerunReplicainReplica.idr) - First-class handlers: Use continuation-passing with
handlefor effect handling
- Use Dhall for test specifications (see
tests.dhall) - Convert Dhall to JSON with
dhall-to-jsonbefore running - Use golden file mode (
Generated True) for output comparison - Structure complex expectations with ordered/unordered fragments:
stdOut = Replica.Expectation :: { consecutive = ["hello", "world"] , end = Some "!" }
Replica.idr: Main entry point, arg parsing, exit handlingReplica/Core/Types.idr: Core data structures (Test,Expectation,Part)Replica/Core/Parse.idr: JSON parsing for test specificationsReplica/App/Run.idr: Test execution logicReplica/Option/Parse.idr: CLI argument parsingReplica/Other/Validation.idr: Error accumulation patterntests.dhall: Primary test suite definitionMakefile: Build and test automation
- Total functions: Always prove totality unless using
coveringwith explicit coverage - String handling: Use
Stringtype; leverageData.Stringutilities - Applicative validation: Combine validators to collect all errors at once
- Effect monad: Use
Control.Appfor I/O operations with structured error handling - Custom operators: Sparingly; prefer explicit function names for clarity
make clean build test # Full clean build + test
nix flake check # Comprehensive CI checksEnsure all tests pass with the current version before committing.