max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(CMakeLists): make python dependency optional

Browse source
This commit is contained in:
Gabriel Ebner 2016-11-30 09:40:32 -05:00
parent c3f72ec0d8
commit db67c1fde3
2 changed files with 4 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
doc/make/msys2.md
View file

@ -11,11 +11,6 @@ It is easy to install all dependencies, it produces native
## Installing dependencies
Lean requires Python2 or Python3. If you do not have a Python installation on your machine,
please download and install one from [Python.org](https://www.python.org/downloads/windows).
Also please make sure that your `PATH` environment variable includes the installed
Python directory (i.e. `C:\Python27`).
[The official webpage of msys2][msys2] provides one-click installers.
We assume that you install [msys2][msys2] at `c:\msys64`.
Once installed it, you can run msys2 shell from the start menu.

8
src/CMakeLists.txt
View file

@ -317,7 +317,7 @@ if(NOT "${EMSCRIPTEN}" AND NOT "${TCMALLOC_FOUND}" AND NOT "${JEMALLOC_FOUND}" A
endif()
# Python
find_package(PythonInterp REQUIRED)
find_package(PythonInterp)
include_directories(${LEAN_SOURCE_DIR})
@ -452,7 +452,7 @@ endif()
add_subdirectory(tests/util/lp)
# Include style check
if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND PYTHONINTERP_FOUND)
include(StyleCheck)
file(GLOB_RECURSE LEAN_SOURCES
"${LEAN_SOURCE_DIR}"
@ -541,9 +541,9 @@ else()
endif()
# CPack -- Debian
if(STATIC)
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "python")
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "")
else()
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev,libmpfr-dev,python")
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev,libmpfr-dev")
endif()
SET(CPACK_DEBIAN_PACKAGE_DESCRIPTION "Lean Theorem Prover")
SET(CPACK_DEBIAN_PACKAGE_SECTION "devel")