leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 217 forks source link

Problem building master on Windows: CMake can't find GMP (mingw64, cmake, make) #1392

Closed kevinsullivan closed 7 years ago

kevinsullivan commented 7 years ago

I'm having trouble building master on Windows/MSYS2/mingw64. Looks like build script is having trouble finding GMP library. Do I need to set GMP_INCLUDE_DIR and GMP_LIBRARIES environment variables? If so, what settings, and should be documented. Below find output of (1) attempt to build lean following instructions from lean repo, and confirmation that GMP libraries are already installed.

================================

$ cmake -DCMAKE_BUILD_TYPE=RELEASE ../../src System is unknown to cmake, create: Platform/MINGW64_NT-6.1 to use this system, please send your config file to cmake@www.cmake.org so it can be added to cmake Your CMakeCache.txt file was copied to CopyOfCMakeCache.txt. Please send that file to cmake@www.cmake.org. -- Lean emacs-mode will be installed at /usr/local/share/emacs/site-lisp/lean -- Lean library will be installed at /usr/local/lib/lean CMake Error at cmake/Modules/FindPackageHandleStandardArgs.cmake:91 (MESSAGE): Could NOT find GMP (missing: GMP_INCLUDE_DIR GMP_LIBRARIES) (Required is at least version "5.0.5") Call Stack (most recent call first): cmake/Modules/FindPackageHandleStandardArgs.cmake:252 (_FPHSA_FAILURE_MESSAGE) cmake/Modules/FindGMP.cmake:12 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) CMakeLists.txt:207 (find_package)

===================

GMP is confirmed installed, version gmp-6.1.0-2

$ pacman -S gmp warning: gmp-6.1.0-2 is up to date -- reinstalling resolving dependencies... looking for conflicting packages...

Packages (1) gmp-6.1.0-2

Total Installed Size: 0.67 MiB Net Upgrade Size: 0.00 MiB

:: Proceed with installation? [Y/n] (1/1) checking keys in keyring [###############################################################] 100% (1/1) checking package integrity [###############################################################] 100% (1/1) loading package files [###############################################################] 100% (1/1) checking for file conflicts [###############################################################] 100% (1/1) checking available disk space [###############################################################] 100% :: Processing package changes... (1/1) reinstalling gmp [###############################################################] 100%

==================

kevinsullivan commented 7 years ago

Tried this command next (defining directories for GMP libraries and header).

cmake -DGMP_INCLUDE_DIR=/usr/local/include -DGMP_LIBRARIES=/usr/lib -DCMAKE_BUILD_TYPE=RELEASE ../../src

Made progress. Should not have to do that. Still not perfect in any case. Is Python (which version?) a dependency? Here's the output:

===========

cmake -DGMP_INCLUDE_DIR=/usr/local/include -DGMP_LIBRARIES=/usr/lib -DCMAKE_BUILD_TYPE=RELEASE ../../src System is unknown to cmake, create: Platform/MINGW64_NT-6.1 to use this system, please send your config file to cmake@www.cmake.org so it can be added to cmake Your CMakeCache.txt file was copied to CopyOfCMakeCache.txt. Please send that file to cmake@www.cmake.org. -- Lean emacs-mode will be installed at /usr/local/share/emacs/site-lisp/lean -- Lean library will be installed at /usr/local/lib/lean -- Using standard malloc. -- Could NOT find PythonInterp (missing: PYTHON_EXECUTABLE) -- git commit sha1: 04fd50e4e8b2df1256983b309ea8d99357c27aa2 -- Configuring done WARNING: Target "leanshared" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "leanstatic" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lean_js" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lean" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "bitap_fuzzy_search" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "rb_tree" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "stackinfo" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "scoped_map" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "options" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "bit_tricks" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "set" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "list" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "serializer" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "name" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "format" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "thread" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "sequence" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "scoped_set" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "rb_map" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "exception" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "hash" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "safe_arith" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "optional" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "buffer" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "sexpr_tst" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "trie" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lru_cache" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "worker_queue" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "mpz" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "mpbq" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "double" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "float" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "xnumeral" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "primes" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "mpq" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "numeric_traits" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "gcd" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "zpz" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "max_sharing" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "free_vars" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "expr" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "replace" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "environment" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "instantiate" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "level" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "head_map" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "parray" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "expr_lt" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "deep_copy" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "occurs" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "delayed_abstraction" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lean_scanner" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "shell_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_name_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_name_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "thread_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "thread_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_univ_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_univ_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_options_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_options_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "shared_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "shared_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_expr_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_expr_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lp_tst" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "double_compare" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. -- Generating done -- Build files have been written to: /c/users/sullivan/lean/build/release

kevinsullivan commented 7 years ago

Next installed python (pacman -S python). Further progress, but still getting warnings about Targets linking to /usr/lib. Not entirely sure what resulting status is.

$ cmake -DGMP_INCLUDE_DIR=/usr/local/include -DGMP_LIBRARIES=/usr/lib -DCMAKE_BUILD_TYPE=RELEASE ../../src System is unknown to cmake, create: Platform/MINGW64_NT-6.1 to use this system, please send your config file to cmake@www.cmake.org so it can be added to cmake Your CMakeCache.txt file was copied to CopyOfCMakeCache.txt. Please send that file to cmake@www.cmake.org. -- Lean emacs-mode will be installed at /usr/local/share/emacs/site-lisp/lean -- Lean library will be installed at /usr/local/lib/lean -- Using standard malloc. -- Found PythonInterp: /usr/bin/python.exe (found version "3.4.3") -- git commit sha1: 04fd50e4e8b2df1256983b309ea8d99357c27aa2 -- Configuring done WARNING: Target "leanshared" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "leanstatic" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lean_js" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lean" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "bitap_fuzzy_search" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "rb_tree" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "stackinfo" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "scoped_map" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "options" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "bit_tricks" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "set" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "list" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "serializer" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "name" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "format" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "thread" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "sequence" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "scoped_set" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "rb_map" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "exception" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "hash" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "safe_arith" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "optional" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "buffer" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "sexpr_tst" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "trie" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lru_cache" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "worker_queue" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "mpz" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "mpbq" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "double" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "float" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "xnumeral" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "primes" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "mpq" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "numeric_traits" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "gcd" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "zpz" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "max_sharing" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "free_vars" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "expr" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "replace" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "environment" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "instantiate" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "level" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "head_map" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "parray" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "expr_lt" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "deep_copy" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "occurs" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "delayed_abstraction" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lean_scanner" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "shell_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_name_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_name_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "thread_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "thread_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_univ_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_univ_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_options_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_options_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "shared_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "shared_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_expr_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "c_expr_test" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "lp_tst" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. WARNING: Target "double_compare" requests linking to directory "/usr/lib". Targets may link only to libraries. CMake is dropping the item. -- Generating done -- Build files have been written to: /c/users/sullivan/lean/build/release

gebner commented 7 years ago

msys2 has special packages for mingw-w64:

pacman -S mingw-w64-x86_64-gcc mingw-w64-x86_64-mpfr mingw-w64-x86_64-ninja mingw-w64-x86_64-cmake git

(The gmp package is different.) See here for the instructions: https://github.com/leanprover/lean/blob/3153b72415866c9b2175b85eef1467361ad2bd11/doc/make/msys2.md

You also need to compile inside the special MinGW 64-bit shell.

kevinsullivan commented 7 years ago

Got it. FWIW, I found the instructions at the lean github site confusing (just me). I saw that I needed MSYS2 and proceeded to the instructions to install the software per the "Build Instructions (CMake + Make)." That is what failed. I've now got it working. Devs might edit the readme file to clarify. Thanks. --Kevin

zk744750315 commented 6 years ago

hello, I heve the same trouble but I can not solve it, can you help me? I have installed the software MSYS2 , then what i should do?

Kha commented 6 years ago

It looks like the build instructions are incomplete, can you try another build after running pacman -S mingw-w64-x86_64-gmp in the mingw-w64 shell?