Fixed platform detection on MSYS (was #908)

[wintersteiger]

This is a replacement for the broken PR #908.

[wintersteiger]

@Uni- Could you try this change to see whether Z3 compiles on your MSYS system with this?

[eonj]

@wintersteiger, still same error as seen in #908.

Traceback (most recent call last):
  File "scripts/mk_make.py", line 21, in <module>
    mk_makefile()
  File "/home/Eon/Development/z3/scripts/mk_util.py", line 2576, in mk_makefile
    mk_config()
  File "/home/Eon/Development/z3/scripts/mk_util.py", line 2475, in mk_config
    raise MKException('Unsupported platform: %s' % sysname)
mk_exception.MKException: 'Unsupported platform: MSYS_NT-10.0'

[wintersteiger]

What kind of Python do you use? Did you compile your own or is that in the MSYS package management repository somewhere?

[wintersteiger]

Bumping. Is this still a problem or has it been resolved?

[eonj]

@wintersteiger, sorry for coming late. I use python2, python3 packages as-is delivered from MSYS Pacman. /usr/bin/python.exe is a copy of /usr/bin/python3.exe, as the packages default.

And still the same exception.

Thank you for your efforts, but I think you should see what's happening on the point build error occurs, scripts/mk_util.py:2475 (at your commit 514f08f). The if-else around this line does not use is_cygwin_mingw(), but the raw uname. That's why at first I modified exactly that line in commit 387970f (initially suggested via #908).

Moreover, I think you commit 514f08f is going little weird. Please see scripts/mk_util.py:614, scripts/mk_util.py:2492, scripts/mk_util.py:2526. The condition setting IS_CYGWIN_MINGW and usages of is_cygwin_mingw() supposes that is_cygwin_mingw() for the MinGW cross-compiling toolchain running on Cygwin, not for the Cygwin native compiling toolchain. Definitely native compiling on MSYS2 is more likely to compiling on Cygwin for itself, not cross-compiling.

I also looked around the whole appearance of '_CYGWIN' macro. As you said in #908 it changes the behavior of Z3, but many of them are unsignificant (like in src/util/trace.h:23, and the rests are used with '_WINDOWS' which means the macro-defined sections should be used instead of other sections for OS X or Linux (because of the limits of Windows environment). Note that IS_CYGWIN always gets True before IS_CYGWIN_MINGW gets True (scripts/mk_util.py:614 again), so the cross-compiled artifact of Z3 for Windows (cross-compiled in Cygwin) obviously has been defined '_CYGWIN' (because the condition making IS_CYGWIN True is same as the condition defining '_CYGWIN', see scripts/mk_util.py:2469). In short, defining _CYGWIN in MSYS2 does not change the behavior of Z3 on Windows.

[wintersteiger]

This is now fixed (e50470f).

Whether the _CYGWIN macro actually, in it's current version, changes the behavior of Z3 is ultimately irrelevant. If -D _CYGWIN is on, we will rely on the platform actually being cygwin and not mingw. Anyways, MSYS2 is now recognized as it's own platform.

[eonj]

@wintersteiger It builds well. Thank you.

BTW why did you decide shared object artifact to have .so extension? In MSYS2 it should be .dll. Also, the dll file should be installed to /usr/bin not /usr/lib (configured with --prefix=/usr). Can it be fixed also?

[wintersteiger]

I assumed MSYS uses .so and binaries with .exe, if that's not so we should of course change that. The install path can be set manually and I'd really like to avoid have a huge list of default install paths for every option on flavors of unpopular OSs...

[wintersteiger]

Ah, I see, the .so/.dll gets put into bin instead of lib? Strange. May be related to the file extensions not matching up.

[wintersteiger]

(Should work as expected now.)