From 478fa821ee5bea7baa18e76ef54405b9bd6b479f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 2 Apr 2026 19:11:29 -0400 Subject: [PATCH] chore: add test suite, gitignore third_party, update CI to run tests - Add tests/ directory with integration tests: minimal translation, enum translation, and impl methods translation - CI now runs `bazel test` on both examples and tests (was only `bazel build`) - Add third_party/ to .gitignore (superseded by hermetic rocq-of-rust download) - Update issue #1 checklist with completed items Co-Authored-By: Claude Opus 4.6 (1M context) --- .github/workflows/ci.yml | 29 +++++----------- .gitignore | 1 + tests/BUILD.bazel | 71 ++++++++++++++++++++++++++++++++++++++++ tests/enums.rs | 14 ++++++++ tests/impl_methods.rs | 20 +++++++++++ tests/minimal.rs | 4 +++ 6 files changed, 118 insertions(+), 21 deletions(-) create mode 100644 tests/BUILD.bazel create mode 100644 tests/enums.rs create mode 100644 tests/impl_methods.rs create mode 100644 tests/minimal.rs diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3d6ae9e..6f2adda 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -95,22 +95,15 @@ jobs: bazel build @rocq_of_rust_source//:rocq_of_rust_main echo "RocqOfRust library built" - - name: Build example proofs + - name: Run tests run: | - echo "Building example proofs..." - bazel build //examples/rust_to_rocq:point_proofs - echo "Example proofs verified" - - - name: Build advanced example - run: | - echo "Building advanced Rust features example..." - bazel build //examples/rust_to_rocq:advanced_verified - echo "Advanced example verified" + echo "Running all tests..." + bazel test //examples/rust_to_rocq:all //tests:all --test_output=errors + echo "All tests passed" - name: Collect verified artifacts run: | mkdir -p verified-artifacts - # Copy compiled proof files find bazel-bin/examples -name "*.vo" -exec cp {} verified-artifacts/ \; find bazel-bin/examples -name "*.v" -exec cp {} verified-artifacts/ \; ls -la verified-artifacts/ @@ -155,17 +148,11 @@ jobs: restore-keys: | bazel-build-${{ runner.os }}- - - name: Build example proofs - run: | - echo "Building example proofs on macOS..." - bazel build //examples/rust_to_rocq:point_proofs - echo "Example proofs verified on macOS" - - - name: Build advanced example + - name: Run tests run: | - echo "Building advanced Rust features example..." - bazel build //examples/rust_to_rocq:advanced_verified - echo "Advanced example verified" + echo "Running all tests on macOS..." + bazel test //examples/rust_to_rocq:all //tests:all --test_output=errors + echo "All tests passed on macOS" - name: Collect verified artifacts run: | diff --git a/.gitignore b/.gitignore index b9b867d..af80d03 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ bazel-testlogs bazel-loom .claude/ MODULE.bazel.lock +third_party/ diff --git a/tests/BUILD.bazel b/tests/BUILD.bazel new file mode 100644 index 0000000..683287e --- /dev/null +++ b/tests/BUILD.bazel @@ -0,0 +1,71 @@ +# Integration tests for rules_rocq_rust +# +# These tests verify the full Rust → Rocq translation and compilation pipeline. + +load("@rules_rocq_rust//coq_of_rust:defs.bzl", "coq_of_rust_library", "rocq_rust_verified_library") +load("@rules_rocq_rust//rocq:defs.bzl", "rocq_proof_test") + +# ============================================= +# Test 1: Minimal translation + compilation +# ============================================= +# Verifies the simplest possible Rust file translates and compiles. + +rocq_rust_verified_library( + name = "minimal_verified", + rust_sources = ["minimal.rs"], + edition = "2021", + extra_flags = ["-impredicative-set"], +) + +rocq_proof_test( + name = "minimal_test", + srcs = [], + deps = [":minimal_verified"], +) + +# ============================================= +# Test 2: Enum translation +# ============================================= +# Verifies enum variants (unit, tuple) translate correctly. + +rocq_rust_verified_library( + name = "enums_verified", + rust_sources = ["enums.rs"], + edition = "2021", + extra_flags = ["-impredicative-set"], +) + +rocq_proof_test( + name = "enums_test", + srcs = [], + deps = [":enums_verified"], +) + +# ============================================= +# Test 3: Impl methods +# ============================================= +# Verifies struct with impl block translates correctly. + +rocq_rust_verified_library( + name = "impl_methods_verified", + rust_sources = ["impl_methods.rs"], + edition = "2021", + extra_flags = ["-impredicative-set"], +) + +rocq_proof_test( + name = "impl_methods_test", + srcs = [], + deps = [":impl_methods_verified"], +) + +# ============================================= +# Test 4: Translation step only +# ============================================= +# Verifies coq_of_rust_library produces .v output without compilation. + +coq_of_rust_library( + name = "minimal_translated", + rust_sources = ["minimal.rs"], + edition = "2021", +) diff --git a/tests/enums.rs b/tests/enums.rs new file mode 100644 index 0000000..164397c --- /dev/null +++ b/tests/enums.rs @@ -0,0 +1,14 @@ +/// Test enum translation with variants. +pub enum Color { + Red, + Green, + Blue, + Custom(u8, u8, u8), +} + +pub fn is_red(c: &Color) -> bool { + match c { + Color::Red => true, + _ => false, + } +} diff --git a/tests/impl_methods.rs b/tests/impl_methods.rs new file mode 100644 index 0000000..4c3cde2 --- /dev/null +++ b/tests/impl_methods.rs @@ -0,0 +1,20 @@ +/// Test struct with impl block methods. +pub struct Counter { + pub value: u32, +} + +impl Counter { + pub fn new() -> Self { + Counter { value: 0 } + } + + pub fn increment(&self) -> Self { + Counter { + value: self.value + 1, + } + } + + pub fn get(&self) -> u32 { + self.value + } +} diff --git a/tests/minimal.rs b/tests/minimal.rs new file mode 100644 index 0000000..b67d1cb --- /dev/null +++ b/tests/minimal.rs @@ -0,0 +1,4 @@ +/// Minimal Rust code for testing the translation pipeline. +pub fn identity(x: i32) -> i32 { + x +}