build

Build System

hadlink uses redo as its build system, which aligns with the project's embedded/minimalist philosophy.

Contents

• Why redo?
• Prerequisites
• Building
• Development Workflow
• Build Scripts
• Continuous Integration
• Troubleshooting
• Advanced Usage
• References

---

Why redo?

• Simple, declarative build scripts
• Correct dependency tracking
• No complex syntax or DSL
• Scripts are just shell scripts
• Minimal, auditable
• Fast and reliable

This project uses dinkelk/redo (MIT), a Haskell implementation that is actively maintained and aligns with the project's toolchain.

Prerequisites

Install redo (dinkelk's Haskell implementation):

# Clone and build
git clone https://github.com/dinkelk/redo.git
cd redo && ./do
export PATH=$PATH:$(pwd)/bin

Or if available via your package manager, install from there.

Stack - Haskell build tool

curl -sSL https://get.haskellstack.org/ | sh
# Or: sudo pacman -S stack (Arch)

Building

Build everything

redo all

This builds the SPARK core library, then all Haskell components.

Run tests

redo test

Runs the property-based test suite.

Run SPARK proofs (Phase 2+)

redo prove

Requires Alire with gnatprove. The spark-core/ directory is an Alire project:

cd spark-core
alr build                                    # Build SPARK library
alr exec -- gnatprove -P hadlink_core.gpr   # Run formal proofs

Clean build artifacts

redo clean

Development Workflow

Incremental builds

redo tracks dependencies automatically:

# Edit source files
vim haskell/src/Types.hs

# Rebuild only what changed
redo all

Generate secrets

redo generate-secret

Creates a deployment secret in deploy/docker/secret.key.

Build Scripts

All build logic lives in .do files:

• all.do - Build all components
• test.do - Run tests
• prove.do - Run SPARK proofs
• clean.do - Clean artifacts
• default.do - Show help
• generate-secret.do - Generate deployment secret
• run-shorten.do - Run shorten daemon locally

Writing new build scripts

Follow redo conventions:

#!/bin/bash
# Brief description

exec >&2  # Redirect script output to stderr

# Add dependencies
redo-ifchange dependency1 dependency2

# Do the work
echo "Building..."
actual_build_command

# Mark as done
touch "$3"

Continuous Integration

Example CI configuration using redo:

# .gitlab-ci.yml
image: haskell:9.2

before_script:
  - git clone https://github.com/dinkelk/redo.git
  - cd redo && ./do && cd ..
  - export PATH=$PATH:$(pwd)/redo/bin

test:
  script:
    - redo all
    - redo test
    - redo prove  # if SPARK available

Troubleshooting

redo command not found

Install redo from https://github.com/dinkelk/redo

Requirements:

• Haskell Stack
• Run ./do in the redo repository

Stale builds

Clean and rebuild:

redo clean
redo all

Permission issues

Ensure .do files are executable:

chmod +x *.do haskell/*.do

Advanced Usage

Parallel builds

redo supports parallel execution:

redo -j4 all

Verbose output

redo -v all

Debugging

redo -x all  # Show commands as they execute

Direct Stack usage

You can also use Stack directly:

cd haskell
stack build          # Build
stack test           # Test
stack exec hadlink   # Run
stack clean          # Clean

References

• dinkelk/redo - This implementation
• DJB's redo design - Original design notes
• apenwarr/redo - Python implementation