cmake: Make Python3 default and improve toml error messages. (#5884)

./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag.

6 files changed, 11 insertions, 18 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 5da6b4208..753872ae1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -153,7 +153,6 @@ jobs:
     - name: Configure
       run: |
         ${{ matrix.env }} ./configure.sh ${{ matrix.config }} \
-          --python3 \
           --prefix=$(pwd)/build/install \
           --unit-testing
 
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6c3ed4bbc..4a90afa8b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -152,8 +152,7 @@ option(USE_DRAT2ER            "Include drat2er for making eager BV proofs")
 option(USE_LFSC               "Use LFSC proof checker")
 option(USE_POLY               "Use LibPoly for polynomial arithmetic")
 option(USE_SYMFPU             "Use SymFPU for floating point support")
-option(USE_PYTHON2            "Prefer using Python 2 (for Python bindings)")
-option(USE_PYTHON3            "Prefer using Python 3 (for Python bindings)")
+option(USE_PYTHON2            "Force Python 2 (deprecated)")
 
 # Custom install directories for dependencies
 # If no directory is provided by the user, we first check if the dependency was
@@ -376,10 +375,8 @@ endif()
 
 if(USE_PYTHON2)
   find_package(PythonInterp 2.7 REQUIRED)
-elseif(USE_PYTHON3)
-  find_package(PythonInterp 3 REQUIRED)
 else()
-  find_package(PythonInterp REQUIRED)
+  find_package(PythonInterp 3 REQUIRED)
 endif()
 
 find_package(GMP REQUIRED)
@@ -715,7 +712,6 @@ print_config("Static binary             :" ENABLE_STATIC_BINARY)
 print_config("Python bindings           :" BUILD_BINDINGS_PYTHON)
 print_config("Java bindings             :" BUILD_BINDINGS_JAVA)
 print_config("Python2                   :" USE_PYTHON2)
-print_config("Python3                   :" USE_PYTHON3)
 message("")
 print_config("ABC                       :" USE_ABC)
 print_config("CaDiCaL                   :" USE_CADICAL)
diff --git a/INSTALL.md b/INSTALL.md
index 86a317168..75538d7cf 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -50,7 +50,7 @@ compatible.
   or [Clang](https://clang.llvm.org) (reasonably recent versions)
 - [CMake >= 3.9](https://cmake.org)
 - [GNU Bash](https://www.gnu.org/software/bash/)
-- [Python >= 2.7](https://www.python.org)
+- [Python 3.x](https://www.python.org)
   + module [toml](https://pypi.org/project/toml/)
 - [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
 - [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/)
diff --git a/NEWS b/NEWS
index d915ef44f..1aeac83da 100644
--- a/NEWS
+++ b/NEWS
@@ -37,6 +37,7 @@ Changes:
 * SMT-LIB output for `get-model` command now conforms with the standard,
   and does *not* begin with the keyword `model`. The output
   is the same as before, only with this word removed from the beginning.
+* Building with Python 2 is now deprecated.
 
 
 Changes since 1.7
diff --git a/configure.sh b/configure.sh
index 0455e6360..419d66ea8 100755
--- a/configure.sh
+++ b/configure.sh
@@ -44,8 +44,7 @@ The following flags enable optional features (disable with --no-<option name>).
   --coverage               support for gcov coverage testing
   --profiling              support for gprof profiling
   --unit-testing           support for unit testing
-  --python2                prefer using Python 2 (also for Python bindings)
-  --python3                prefer using Python 3 (also for Python bindings)
+  --python2                force Python 2 (deprecated)
   --python-bindings        build Python bindings based on new C++ API
   --java-bindings          build Java bindings based on new C++ API
   --all-bindings           build bindings for all supported languages
@@ -138,7 +137,6 @@ optimized=default
 profiling=default
 proofs=default
 python2=default
-python3=default
 python_bindings=default
 java_bindings=default
 editline=default
@@ -285,9 +283,6 @@ do
     --python2) python2=ON;;
     --no-python2) python2=OFF;;
 
-    --python3) python3=ON;;
-    --no-python3) python3=OFF;;
-
     --python-bindings) python_bindings=ON;;
     --no-python-bindings) python_bindings=OFF;;
 
@@ -408,8 +403,6 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing"
 [ $python2 != default ] \
   && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2"
-[ $python3 != default ] \
-  && cmake_opts="$cmake_opts -DUSE_PYTHON3=$python3"
 [ $python_bindings != default ] \
   && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
 [ $java_bindings != default ] \
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index cd648955e..663b2bf13 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -18,8 +18,12 @@ execute_process(
 )
 
 if(RET_TOML)
-    message(FATAL_ERROR
-      "Could not find Python module toml. Install via `pip install toml'.")
+  message(FATAL_ERROR
+      "Could not find toml for Python "
+      "version ${PYTHON_VERSION_MAJOR}.${PYTHON_VERSION_MINOR}. "
+      "Make sure to install toml for this Python version "
+      "via \n`${PYTHON_EXECUTABLE} -m pip install toml'.\nNote: You need to "
+      "have pip installed for this Python version.")
 endif()
 
 libcvc4_add_sources(