fix: suppress deprecated-literal-operator error on Apple Clang 21+ - #57
Open
SebTardif wants to merge 1 commit into
Open
fix: suppress deprecated-literal-operator error on Apple Clang 21+#57SebTardif wants to merge 1 commit into
SebTardif wants to merge 1 commit into
Conversation
On macOS 26+ with Apple Clang 21, the static build fails during the Poly-EP ExternalProject because gmpxx.h uses a deprecated whitespace-before-suffix syntax in user-defined literal operators. libpoly compiles with -Werror, promoting the warning to a fatal error. cvc5's cmake/FindPoly.cmake already suppresses this warning for WASM builds but not for native macOS. This patch makes the suppression unconditional by patching FindPoly.cmake before running configure.sh, using the strong form (-Wno-deprecated-literal-operator) that works regardless of -Werror ordering. The patch is applied in both build.rs (for cargo build --features static) and the setup-cvc5 CI action (for GitHub Actions macOS runners). It is idempotent: if FindPoly.cmake does not contain the expected text, the patch silently does nothing. Closes cvc5#56
3 tasks
SebTardif
added a commit
to assura-lang/assura
that referenced
this pull request
Jul 27, 2026
## Summary MPI pre-rotation gate: land accepted documentation backlog. - **#1413** Competitor-thread reply playbook (`docs/launch/competitor-replies.md`) - **#1411** RFMIG outreach outline (`docs/launch/rfmig-intro.md`) - **#1412** SMT / portfolio technical note (`docs/SMT-NOTE.md`, mdBook link) - **#1399** Document deferred playground alternative: Codespaces (`.devcontainer/`) + demo GIF + install path in GETTING-STARTED ## Not in this PR - **#1410** Actual public posts (Show HN / Lobsters / Reddit / TWiR) need a human owner - **#1396** Awesome-list submissions after hard launch (#1410) - **#436** Still blocked on cvc5/cvc5-rs#57 ## Test plan - [x] Docs are markdown only + symlink; no Rust changes - [ ] Spot-check links in `docs/launch/README.md` and `docs/SMT-NOTE.md` - [ ] Confirm mdBook SUMMARY includes SMT note Closes #1413 Closes #1411 Closes #1412 Closes #1399 Signed-off-by: Sebastien Tardif <sebtardif@ncf.ca>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #56
Problem
On macOS 26+ with Apple Clang 21, the static build fails during the
Poly-EP ExternalProject because
gmpxx.huses a deprecatedwhitespace-before-suffix syntax in user-defined literal operators
(
operator"" _mpz,_mpq,_mpf). libpoly's own CMakeLists.txtcompiles with
-Werror, promoting the warning to a fatal error.cvc5's
cmake/FindPoly.cmakealready has a workaround that passes-DCMAKE_CXX_FLAGS=-Wno-error=deprecated-literal-operatorto thePoly-EP ExternalProject, but only for WASM builds. Native macOS
builds get no suppression.
Fix
Make the warning suppression unconditional by patching
FindPoly.cmakebefore running
configure.sh. The patch replaces the WASM-onlyconditional with an unconditional assignment, and uses the strong form
(
-Wno-deprecated-literal-operator) instead of the weak form(
-Wno-error=deprecated-literal-operator). The strong form suppressesthe warning entirely, so it works regardless of where
-Werrorappearson the command line.
The patch is applied in two places:
cvc5-sys/build.rs: for users building from source viacargo build --features static.github/actions/setup-cvc5/action.yml: for CI builds on macOS runnersThe patch is idempotent: if
FindPoly.cmakedoesn't contain theexpected text (e.g., upstream has already fixed this), it silently
does nothing.
Environment
Related