Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 24 additions & 0 deletions .github/actions/setup-cvc5/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,30 @@ runs:
path: cvc5-sys/cvc5/build
key: ${{ runner.os }}-cvc5-${{ hashFiles('cvc5-sys/cvc5/**/*.cmake', 'cvc5-sys/cvc5/CMakeLists.txt') }}

- name: Patch FindPoly.cmake for Apple Clang 21+
if: steps.cache-static.outputs.cache-hit != 'true'
shell: bash
run: |
# Apple Clang 21+ (macOS 26+) errors on the deprecated
# whitespace-before-suffix syntax in gmpxx.h literal operators.
# libpoly builds with -Werror, so the warning becomes fatal.
# The existing cmake only suppresses this for WASM builds;
# make it unconditional using the strong -Wno- form.
# See https://github.com/cvc5/cvc5-rs/issues/56
F=cvc5-sys/cvc5/cmake/FindPoly.cmake
python3 -c "
import pathlib, sys
f = pathlib.Path('$F')
if not f.exists():
sys.exit(0)
t = f.read_text()
old = 'set(POLY_CXX_FLAGS \"\")\n if(NOT(WASM STREQUAL \"OFF\"))\n set(POLY_CXX_FLAGS -DCMAKE_CXX_FLAGS=-Wno-error=deprecated-literal-operator)\n endif()'
new = 'set(POLY_CXX_FLAGS -DCMAKE_CXX_FLAGS=-Wno-deprecated-literal-operator)'
if old in t:
f.write_text(t.replace(old, new))
print('Patched FindPoly.cmake')
"

- name: Build cvc5 (static)
if: steps.cache-static.outputs.cache-hit != 'true'
shell: bash
Expand Down
50 changes: 50 additions & 0 deletions cvc5-sys/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -252,6 +252,45 @@ fn check_cvc5_version(cvc5_dir: &Path, expected: &str) {
println!("cargo:rerun-if-changed={}", version_file.display());
}

/// Patch `cmake/FindPoly.cmake` in the cvc5 source tree so the
/// `-Wno-deprecated-literal-operator` flag is always passed to the
/// Poly-EP ExternalProject, not only for WASM builds. This fixes a
/// build failure on Apple Clang 21+ (macOS 26+) where `gmpxx.h`
/// user-defined literal operators trigger `-Werror`.
///
/// The patch is idempotent: if the file was already patched (or doesn't
/// exist), it is a no-op.
#[cfg(feature = "static")]
fn patch_find_poly_cmake(cvc5_dir: &Path) {
let cmake_file = cvc5_dir.join("cmake/FindPoly.cmake");
if !cmake_file.exists() {
return;
}
let content = fs::read_to_string(&cmake_file).expect("Failed to read FindPoly.cmake");

// The upstream file conditionally sets POLY_CXX_FLAGS only for WASM:
//
// set(POLY_CXX_FLAGS "")
// if(NOT(WASM STREQUAL "OFF"))
// set(POLY_CXX_FLAGS -DCMAKE_CXX_FLAGS=-Wno-error=deprecated-literal-operator)
// endif()
//
// Replace with an unconditional assignment using the strong form of
// the flag (-Wno- instead of -Wno-error=), which suppresses the
// warning entirely regardless of -Werror ordering.
let old = r#"set(POLY_CXX_FLAGS "")
if(NOT(WASM STREQUAL "OFF"))
set(POLY_CXX_FLAGS -DCMAKE_CXX_FLAGS=-Wno-error=deprecated-literal-operator)
endif()"#;
let new = r#"set(POLY_CXX_FLAGS -DCMAKE_CXX_FLAGS=-Wno-deprecated-literal-operator)"#;

if content.contains(old) {
let patched = content.replace(old, new);
fs::write(&cmake_file, patched).expect("Failed to write FindPoly.cmake");
eprintln!("Patched FindPoly.cmake: unconditional -Wno-deprecated-literal-operator");
}
}

// return (include path, lib path) if exist

#[cfg(unix)]
Expand Down Expand Up @@ -283,6 +322,17 @@ fn ensure_cvc5_built_and_install() -> (Option<PathBuf>, Option<PathBuf>) {

let build_dir = cvc5_dir.join("build");

// Patch FindPoly.cmake to fix the deprecated-literal-operator build
// failure on Apple Clang 21+ (macOS 26+). The existing cmake file
// uses -Wno-error=deprecated-literal-operator (the weak form), which
// only prevents -Werror from promoting the warning. But libpoly's
// CMakeLists.txt adds -Werror via target_compile_options, which
// appears after CMAKE_CXX_FLAGS on the command line, overriding the
// weak form. The strong form -Wno-deprecated-literal-operator
// suppresses the warning entirely, so -Werror has nothing to promote.
// See https://github.com/cvc5/cvc5-rs/issues/56
patch_find_poly_cmake(&cvc5_dir);

let status = Command::new("bash")
.arg(&configure)
.arg("--static")
Expand Down