search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
607 stars 132 forks source link

C++ compilation failure of `src/HolSat/sat_solvers/zc2hs` on macOS #1233

Closed binghe closed 2 weeks ago

binghe commented 1 month ago

I think this issue is new on macOS 14 (Sonoma) with latest Xcode (I'm using version 15.3). Apple's c++ (clang++) cannot compile src/HolSat/sat_solvers/zc2hs/zc2hs.cpp:

src/HolSat/sat_solvers/zc2hs$ make
ln -fs ../minisat/Proof.o
ln -fs ../minisat/File.o
ln -fs ../minisat/File.h
ln -fs ../minisat/Proof.h
ln -fs ../minisat/Global.h
ln -fs ../minisat/Sort.h
ln -fs ../minisat/SolverTypes.h
In file included from zc2hs.cpp:2:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/iostream:43:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/ios:222:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__locale:15:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/shared_ptr.h:30:
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:613:19: error: use of overloaded operator '!=' is ambiguous (with operand types 'std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>' and 'std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>')
  while (__first1 != __last1) {
         ~~~~~~~~ ^  ~~~~~~~
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1035:27: note: in instantiation of function template specialization 'std::__uninitialized_allocator_move_if_noexcept<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >' requested here
    __v.__begin_   = std::__uninitialized_allocator_move_if_noexcept(
                          ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1620:5: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::__swap_out_circular_buffer' requested here
    __swap_out_circular_buffer(__v);
    ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1648:9: note: in instantiation of function template specialization 'std::vector<std::pair<enum_ty, std::vector<int> > >::__push_back_slow_path<std::pair<enum_ty, std::vector<int> > >' requested here
        __push_back_slow_path(std::move(__x));
        ^
zc2hs.cpp:53:15: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::push_back' requested here
    pclauses->push_back(make_pair(ROOT,lits));
              ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__iterator/reverse_iterator.h:235:1: note: candidate function [with _Iter1 = std::pair<enum_ty, std::vector<int> > *, _Iter2 = std::pair<enum_ty, std::vector<int> > *]
operator!=(const reverse_iterator<_Iter1>& __x, const reverse_iterator<_Iter2>& __y)
^
./Global.h:266:39: note: candidate function [with T = std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>]
template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
                                      ^
In file included from zc2hs.cpp:2:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/iostream:43:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/ios:222:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__locale:15:
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/shared_ptr.h:30:
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:523:18: error: use of overloaded operator '!=' is ambiguous (with operand types 'std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >' and 'std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >')
  for (; __first != __last; ++__first)
         ~~~~~~~ ^  ~~~~~~
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:535:10: note: in instantiation of function template specialization 'std::__allocator_destroy<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >, std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> > >' requested here
    std::__allocator_destroy(__alloc_, std::reverse_iterator<_Iter>(__last_), std::reverse_iterator<_Iter>(__first_));
         ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__utility/exception_guard.h:86:7: note: in instantiation of member function 'std::_AllocatorDestroyRangeReverse<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >::operator()' requested here
      __rollback_();
      ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__memory/uninitialized_algorithms.h:612:7: note: in instantiation of member function 'std::__exception_guard_exceptions<std::_AllocatorDestroyRangeReverse<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> > >::~__exception_guard_exceptions' requested here
      std::__make_exception_guard(_AllocatorDestroyRangeReverse<_Alloc, _Iter2>(__alloc, __destruct_first, __first2));
      ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1035:27: note: in instantiation of function template specialization 'std::__uninitialized_allocator_move_if_noexcept<std::allocator<std::pair<enum_ty, std::vector<int> > >, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >' requested here
    __v.__begin_   = std::__uninitialized_allocator_move_if_noexcept(
                          ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1620:5: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::__swap_out_circular_buffer' requested here
    __swap_out_circular_buffer(__v);
    ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/vector:1648:9: note: in instantiation of function template specialization 'std::vector<std::pair<enum_ty, std::vector<int> > >::__push_back_slow_path<std::pair<enum_ty, std::vector<int> > >' requested here
        __push_back_slow_path(std::move(__x));
        ^
zc2hs.cpp:53:15: note: in instantiation of member function 'std::vector<std::pair<enum_ty, std::vector<int> > >::push_back' requested here
    pclauses->push_back(make_pair(ROOT,lits));
              ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/v1/__iterator/reverse_iterator.h:235:1: note: candidate function [with _Iter1 = std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>, _Iter2 = std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *>]
operator!=(const reverse_iterator<_Iter1>& __x, const reverse_iterator<_Iter2>& __y)
^
./Global.h:266:39: note: candidate function [with T = std::reverse_iterator<std::reverse_iterator<std::pair<enum_ty, std::vector<int> > *> >]
template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
                                      ^
2 errors generated.
make: *** [zc2hs] Error 1

The failure of building this zc2hs (what is it?) doesn't break the entire HOL builds (it seems not used when building core theories), but if you rebuild HOL (even without modifying any code), the building process will restart from generating numheap (a huge waste of time).

Using MacPorts's gcc13 (/opt/local/bin/g++-mp-13), this code can still be compiled without any modification.

I'm no expert to solve this C++ standard compatibility issue.

binghe commented 1 month ago

I suggest at least changing the Holmakefile inside zc2hs folder to the following:

# this assumes minisat's already been built in ../minisat

all: zc2hs

CXX = $(or $(MINISAT_CXX),c++)

zc2hs: 
    ln -fs ../minisat/Proof.o
    ln -fs ../minisat/File.o
    ln -fs ../minisat/File.h
    ln -fs ../minisat/Proof.h
    ln -fs ../minisat/Global.h
    ln -fs ../minisat/Sort.h
    ln -fs ../minisat/SolverTypes.h
    @$(CXX) -O3 Proof.o File.o zc2hs.cpp -o zc2hs

clean:
    @rm -f zc2hs *.h *.o

So that manually calling make MINISAT_CXX=g++-mp-13 could work.

oskarabrahamsson commented 2 weeks ago

The error comes from these: https://github.com/HOL-Theorem-Prover/HOL/blob/develop/src/HolSat/sat_solvers/minisat/Global.h#L264.

I don't know what this nonsense is and I suspect you could safely delete the definitions within the #ifdef, but you could try to pass -D__SGI_STL_INTERNAL_RELOPS and see if it actually improves the situation first.

binghe commented 2 weeks ago

The error comes from these: https://github.com/HOL-Theorem-Prover/HOL/blob/develop/src/HolSat/sat_solvers/minisat/Global.h#L264.

I don't know what this nonsense is and I suspect you could safely delete the definitions within the #ifdef, but you could try to pass -D__SGI_STL_INTERNAL_RELOPS and see if it actually improves the situation first.

Thanks for your investigations. Completely commenting all the 4 definitions doesn't work (even Minisat itself cannot be compiled then). But now I found that it's actually the first one - overloaded != causing problems. Just commenting out that one, and manually change two expressions from a != b to ~(a == b), will fix the building issue with Apple's latest clang++.

I will submit a PR soon.

binghe commented 2 weeks ago

See #1254