From 480b6eeb521c1eb4275e20b8fd83f02d142e1539 Mon Sep 17 00:00:00 2001 From: Sergey Fedorov Date: Tue, 3 Sep 2024 18:58:26 +0800 Subject: [PATCH] vampire: update to 4.9 release --- math/vampire/Portfile | 19 +++++++----- ...x-for-macOS-where-aligned_alloc-may-.patch | 31 +++++++++++++++++++ 2 files changed, 42 insertions(+), 8 deletions(-) create mode 100644 math/vampire/files/0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch diff --git a/math/vampire/Portfile b/math/vampire/Portfile index 73f9d9f142385..6605f6c035f2d 100644 --- a/math/vampire/Portfile +++ b/math/vampire/Portfile @@ -4,19 +4,19 @@ PortSystem 1.0 PortGroup cmake 1.1 PortGroup github 1.0 -# Temporarily remains commit-based until the next release -# due to important fixes being added by the upstream recently. -github.setup vprover vampire 1b080631257a403681d1287f87f8d3ac1ee97c63 -version 2024-05-31 +github.setup vprover vampire 4.9 v casc2024 +revision 0 +epoch 1 categories math science platforms darwin freebsd maintainers {landonf @landonf} openmaintainer description Vampire Theorem Prover long_description High performance automated theorem prover. -checksums rmd160 e09d316e9fda2479726491f197d8b4edbf5e2e2f \ - sha256 f0f1ee2bbd10b82e0373a53357572f5f3801568e5c67aaba2fdc5209b8091a34 \ - size 1466583 +checksums rmd160 e62573a009237c43c550837ad5f34476fbdaa235 \ + sha256 7d0101dc296d0f6fb4f3326febf6a3f3bfd3400b36249a91794789c68a855f3d \ + size 1502934 +github.tarball_from releases # Vampire is BSD-licensed, embedded minisat is MIT-licensed license BSD MIT @@ -25,11 +25,14 @@ github.tarball_from archive patchfiles patch-CMakeLists.txt.diff +# https://github.com/vprover/vampire/pull/593 +patchfiles-append 0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch + cmake.build_type Release cmake.generator Ninja compiler.cxx_standard \ - 2014 + 2017 configure.args-append \ -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON diff --git a/math/vampire/files/0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch b/math/vampire/files/0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch new file mode 100644 index 0000000000000..15ce50ce62a2a --- /dev/null +++ b/math/vampire/files/0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch @@ -0,0 +1,31 @@ +From 94819be610e27eff71e2d692c618345d405dcd17 Mon Sep 17 00:00:00 2001 +From: Sergey Fedorov +Date: Tue, 3 Sep 2024 18:38:34 +0800 +Subject: [PATCH] Allocator.cpp: fix for macOS where aligned_alloc may not be + supported + +--- Lib/Allocator.cpp ++++ Lib/Allocator.cpp +@@ -19,6 +19,10 @@ + #include "Allocator.hpp" + #include "Lib/Timer.hpp" + ++#ifdef __APPLE__ ++#include ++#endif ++ + #ifndef INDIVIDUAL_ALLOCATIONS + Lib::SmallObjectAllocator Lib::GLOBAL_SMALL_OBJECT_ALLOCATOR; + #endif +@@ -43,9 +47,10 @@ + ALLOCATED += size; + { + Lib::TimeoutProtector tp; ++#if !defined(__APPLE__) || (defined(__APPLE__) && MAC_OS_X_VERSION_MIN_REQUIRED >= 101300) + if(void *ptr = std::aligned_alloc(align, size)) + return ptr; +- ++#endif + // we might be here because `aligned_alloc` is finicky (Apple, looking at you) + // so try again with `malloc` and hope for good alignment + if(void *ptr = std::malloc(size))