search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
363 stars 45 forks source link

hack: undef status_interrupted to fix windows build #467

Closed ahmed-irfan closed 9 months ago

ahmed-irfan commented 9 months ago

this hack is a temporary fix for the windows build.

A proper fix (https://github.com/SRI-CSL/yices2/pull/466) will go into the Yices 2.8 release.

coveralls commented 9 months ago

Coverage Status

coverage: 65.098%. remained the same when pulling 4bea5b98918c5d1468e056bf8d55b6f3432eecc9 on patch-iss-418-prerelease into 95f13c6777b9c262dc13aebd908aa52fda0892d2 on master.

markpmitchell commented 9 months ago

There’s no backwards compatibility problem on MINGW if the code never compiled before. Did it?

If it didn’t, you could do this:

  1. In the enum definition use YICES_STATUS_INTERRUPTED.
  2. Elsewhere in yices.h add:

/ To avoid breaking backwards compatibility until Yices 2.8. /

ifndef MINGW

define STATUS_INTERRUPTED YICES_STATUS_INTERRUPTED

endif

Then, change all the .c files to use YICES_STATUS_INTERRUPTED.

That avoids changing the API for 2.7 update releases on non-Windows platforms. And it avoids undef’ing a Windows API macro.

FWIW,

-- Mark Mitchell

On Oct 9, 2023, at 6:28 PM, Ahmed @.***> wrote:

this hack is a temporary fix for the windows build.

A proper fix (#466 https://github.com/SRI-CSL/yices2/pull/466) will go the Yices 2.8 release.

You can view, comment on, or merge this pull request online at:

https://github.com/SRI-CSL/yices2/pull/467

Commit Summary

8638a19 https://github.com/SRI-CSL/yices2/pull/467/commits/8638a1987e5b6ef0a1151901bfd02a5ab2a6ee76 hack: undef status_interrupted to fix windows build File Changes (1 file https://github.com/SRI-CSL/yices2/pull/467/files) M src/include/yices_types.h https://github.com/SRI-CSL/yices2/pull/467/files#diff-568871607b523aa15c2c53076965871130ee4c3ebe40ba075a8a0cf9c57b52af (9) Patch Links:

https://github.com/SRI-CSL/yices2/pull/467.patch https://github.com/SRI-CSL/yices2/pull/467.diff — Reply to this email directly, view it on GitHub https://github.com/SRI-CSL/yices2/pull/467, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKVS3BEVFBOJFNRINHHWODX6SQDLAVCNFSM6AAAAAA5ZR7BBCVHI2DSMVQWIX3LMV43ASLTON2WKOZRHEZTIMJRGA2TANA. You are receiving this because you are subscribed to this thread.

ahmed-irfan commented 9 months ago

There’s no backwards compatibility problem on MINGW if the code never compiled before. Did it? If it didn’t, you could do this: 1. In the enum definition use YICES_STATUS_INTERRUPTED. 2. Elsewhere in yices.h add: / To avoid breaking backwards compatibility until Yices 2.8. / #ifndef MINGW #define STATUS_INTERRUPTED YICES_STATUS_INTERRUPTED #endif Then, change all the .c files to use YICES_STATUS_INTERRUPTED. That avoids changing the API for 2.7 update releases on non-Windows platforms. And it avoids undef’ing a Windows API macro. FWIW, …

I like it. Updating the PR accordingly. Thanks Mark!

disteph commented 9 months ago

I agree with that solution.