Skip to content

Add differential testing: Crane C++ vs Rocq OCaml extraction#42

Open
CharlesCNorton wants to merge 1 commit intobloomberg:mainfrom
CharlesCNorton:differential-tests
Open

Add differential testing: Crane C++ vs Rocq OCaml extraction#42
CharlesCNorton wants to merge 1 commit intobloomberg:mainfrom
CharlesCNorton:differential-tests

Conversation

@CharlesCNorton
Copy link
Copy Markdown
Contributor

@CharlesCNorton CharlesCNorton commented Feb 25, 2026

Summary

  • Adds OCaml extraction to 3 existing test .v files (ack, module, mutual_mod) alongside their Crane C++ extraction
  • Each test gets a pair of thin diff harnesses (.d.cpp / .d.ml) that print identical canonical output
  • A driver script (scripts/run-diff-tests.sh) compiles both sides, runs both, and diffs stdout
  • Reuses existing test definitions — no duplicated Coq code

What each test exercises

Test Features
ack Deep recursion, nat→int mapping
mutual_mod Mutually recursive inductives, constant extraction
module Functors, BST tree, option type, comparison

How to run

eval $(opam env --switch=default --set-switch)
dune build tests/basics
bash scripts/run-diff-tests.sh

Test plan

  • All 3 differential tests produce identical C++ and OCaml output
  • Existing tests still build and pass alongside the new OCaml extraction
  • Driver script runs clean end-to-end

Add OCaml extraction to 3 existing test .v files (ack, module,
mutual_mod) alongside their Crane extraction. Each test gets a
pair of thin diff harnesses (.d.cpp / .d.ml) that print identical
canonical output. A driver script compiles both sides, runs both,
and diffs stdout.

Tests exercise: deep recursion with nat-to-int mapping (ack),
mutually recursive inductives (mutual_mod), and functors with
BST/option types (module). All 3 pass.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant