Integrate CodSpeed for Continuous Performance Monitoring

Summary

Integrate CodSpeed to continuously monitor performance of the regex engine. Since CodSpeed doesn't support Lean directly, we'll use Rust integration via C FFI. In other words, we'll expose C functions from the Lean library and write benchmarks in Rust.

Motivation

• Detect performance regressions early in PRs
• Quantitatively measure optimization impact
• Compare Backtracker vs VM engine performance

Implementation Plan

1. Export C Functions from Lean

Expose key API functions via Lean's FFI:

Function	Description
regex_parse	Parse and compile regex
regex_test	Test for match existence
regex_find_all	Find all matches
regex_capture_all	Match with capture groups

2. Rust Benchmark Crate

bench/
├── Cargo.toml
├── build.rs           # Link Lean library
├── src/lib.rs         # FFI shim
└── benches/
    └── matching.rs    # Benchmarks using divan

Cargo.toml:

[dev-dependencies]
divan = { package = "codspeed-divan-compat", version = "*" }

[[bench]]
name = "lean-regex-bench"
harness = false

3. GitHub Actions Workflow

name: CodSpeed Benchmarks

on:
  push:
    branches:
      - "main"
  pull_request:
  # `workflow_dispatch` allows CodSpeed to trigger backtest
  # performance analysis in order to generate initial data.
  workflow_dispatch:

permissions:
  contents: read
  id-token: write # required for OIDC authentication with CodSpeed

jobs:
  benchmarks:
    name: Run benchmarks
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - name: Build Regex
        uses: leanprover/lean-action@v1
        with:
          build-args: '--wfail'
          lake-package-directory: regex
      - name: Setup Rust toolchain, cache and cargo-codspeed
        uses: moonrepo/setup-rust@v1
        with:
          channel: stable
          cache-target: release
          bins: cargo-codspeed
      - name: Build the benchmark target(s)
        working-directory: bench
        run: cargo codspeed build
      - name: Run the benchmarks
        uses: CodSpeedHQ/action@v4
        with:
          mode: simulation
          working-directory: bench
          run: cargo codspeed run

Benchmark Candidates

Consider sourcing benchmark patterns from burntsushi/rebar (regex barometer), which provides a curated collection of:

• Real-world regex patterns from various domains
• Pathological cases that stress regex engines
• Standardized input corpora for fair comparison

This would give us battle-tested benchmarks and enable comparison with other regex implementations.

Suggested Categories

1. Parsing — Simple patterns, complex quantifiers, large character classes
2. Matching — Short/long inputs, match present/absent, multiple matches
3. Engine comparison — Backtracker vs VM on same workloads
4. Edge cases — Catastrophic backtracking resistance

Tasks

• Investigate Lean 4 FFI for C function exports
• Select benchmark patterns from rebar or create our own
• Implement Rust benchmark crate

I'll integrate CodSpeed into the repository.

References

• CodSpeed Rust/divan docs
• Lean 4 FFI docs
• burntsushi/rebar