From: Andrew V. Jones Date: Fri, 17 Jul 2020 17:09:14 +0000 (+0100) Subject: Support for using 'libedit' over 'readline' #4571 (#4579) X-Git-Tag: cvc5-1.0.0~3091 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8df6f67cc2654f50d49995377a4b411668235e1;p=cvc5.git Support for using 'libedit' over 'readline' #4571 (#4579) Signed-off-by: Andrew V. Jones --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7dd080f71..e9587e2e6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,7 +16,7 @@ jobs: include: - name: production - config: production --all-bindings --lfsc + config: production --all-bindings --lfsc --editline cache-key: production python-bindings: true check-examples: true @@ -28,7 +28,7 @@ jobs: env: CC=clang CXX=clang++ - name: debug - config: debug --symfpu --lfsc --no-debug-symbols + config: debug --symfpu --lfsc --no-debug-symbols --editline cache-key: debug - name: debug-cln @@ -51,11 +51,14 @@ jobs: cxxtest \ libcln-dev \ libgmp-dev \ + libedit-dev \ swig3.0 python3 -m pip install toml python3 -m pip install setuptools + python3 -m pip install pexpect echo "::add-path::/usr/lib/ccache" + # Note: macOS comes with a libedit; it does not need to brew-installed - name: Install Packages (macOS) if: runner.os == 'macOS' run: | @@ -67,6 +70,7 @@ jobs: swig python3 -m pip install toml python3 -m pip install setuptools + python3 -m pip install pexpect echo "::add-path::/usr/local/opt/ccache/libexec" # Note: We install Cython with sudo since cmake can't find Cython otherwise. diff --git a/CMakeLists.txt b/CMakeLists.txt index f4aa6c611..7fc0af52c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -139,7 +139,7 @@ cvc4_option(USE_CLN "Use CLN instead of GMP") cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") cvc4_option(USE_GLPK "Use GLPK simplex solver") cvc4_option(USE_KISSAT "Use Kissat SAT solver") -cvc4_option(USE_READLINE "Use readline for better interactive support") +cvc4_option(USE_EDITLINE "Use Editline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) option(USE_DRAT2ER "Include drat2er for making eager BV proofs") @@ -274,7 +274,7 @@ if(ENABLE_BEST) cvc4_set_option(USE_CLN ON) cvc4_set_option(USE_CRYPTOMINISAT ON) cvc4_set_option(USE_GLPK ON) - cvc4_set_option(USE_READLINE ON) + cvc4_set_option(USE_EDITLINE ON) endif() # Only enable unit testing if assertions are enabled. Otherwise, unit tests @@ -514,12 +514,11 @@ else() set(CVC4_USE_POLY_IMP 0) endif() -if(USE_READLINE) - set(GPL_LIBS "${GPL_LIBS} readline") - find_package(Readline REQUIRED) - set(HAVE_LIBREADLINE 1) - if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR) - set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1) +if(USE_EDITLINE) + find_package(Editline REQUIRED) + set(HAVE_LIBEDITLINE 1) + if(Editline_COMPENTRY_FUNC_RETURNS_CHARPTR) + set(EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP 1) endif() endif() @@ -707,7 +706,7 @@ if(CVC4_USE_CLN_IMP) else() message("MP library : gmp") endif() -print_config("Readline :" ${USE_READLINE}) +print_config("Editline :" ${USE_EDITLINE}) print_config("SymFPU :" ${USE_SYMFPU}) message("") if(ABC_DIR) diff --git a/COPYING b/COPYING index e0d15cf03..d6f66b097 100644 --- a/COPYING +++ b/COPYING @@ -8,9 +8,9 @@ original or modified versions; distribution is under the terms of the modified BSD license (reproduced below). Please note that CVC4 can be configured (however, by default it is not) to link against some GPLed libraries, and therefore the use of these builds may be restricted in non-GPL-compatible -projects. See below for a discussion of CLN, GLPK, and Readline (the three -GPLed optional library dependences for CVC4), and how to ensure you have a -build that doesn't link against GPLed libraries. +projects. See below for a discussion of CLN and GLPK (the two GPLed optional +library dependences for CVC4), and how to ensure you have a build that doesn't +link against GPLed libraries. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are @@ -80,6 +80,7 @@ CVC4 optionally links against the following libraries: CryptoMiniSat (https://github.com/msoos/cryptominisat) LFSC checker (https://github.com/CVC4/LFSC) LibPoly (https://github.com/SRI-CSL/libpoly) + libedit (https://thrysoee.dk/editline) Linking CVC4 against these libraries does not affect the license terms of the CVC4 code. See the respective projects for copyright and licensing @@ -108,7 +109,3 @@ version of GLPK, the GNU Linear Programming Kit, available here: https://github.com/timothy-king/glpk-cut-log -CVC4 can be optionally configured to link against GNU Readline for improved -text-editing support in interactive mode. GNU Readline is available here: - - http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html diff --git a/INSTALL.md b/INSTALL.md index 2c73827c1..a5b048131 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -176,18 +176,12 @@ and-inverter-graphs (AIG) and ABC is used to simplify these AIGs. ABC can be installed using the `contrib/get-abc` script. Configure CVC4 with `configure.sh --abc` to build with this dependency. -### GNU Readline library (Improved Interactive Experience) +### Editline library (Improved Interactive Experience) -The [GNU Readline](http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html) -library is optionally used to provide command editing, tab completion, and -history functionality at the CVC4 prompt (when running in interactive mode). -Check your distribution for a package named "libreadline-dev" or -"readline-devel" or similar. - -Note that GNU Readline is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). -If you choose to use CVC4 with GNU Readline support, you are licensing CVC4 -under that same license. -(Usually CVC4's license is more permissive; see above discussion.) +The [Editline Library](https://thrysoee.dk/editline/) library is optionally +used to provide command editing, tab completion, and history functionality at +the CVC4 prompt (when running in interactive mode). Check your distribution +for a package named "libedit-dev" or "libedit-devel" or similar. ### Boost C++ base libraries (Examples) diff --git a/NEWS b/NEWS index b34d9b116..f74fe2631 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,10 @@ Improvements: Changes: * SyGuS: Removed support for SyGuS-IF 1.0. * Removed Java and Python bindings for the legacy API +* Interactive shell: the GPL-licensed Readline library has been replaced the + BSD-licensed Editline. Compiling with `--best` now enables Editline, instead + of Readline. Without selecting optional GPL components, Editline-enabled CVC4 + builds will be BSD licensed. Changes since 1.7 ================= diff --git a/cmake/FindEditline.cmake b/cmake/FindEditline.cmake new file mode 100644 index 000000000..fe4001173 --- /dev/null +++ b/cmake/FindEditline.cmake @@ -0,0 +1,40 @@ +# Find Editline +# Editline_FOUND - found Editline lib +# Editline_INCLUDE_DIR - the Editline include directory +# Editline_LIBRARIES - Libraries needed to use Editline +# Editline_COMPENTRY_FUNC_RETURNS_CHARPTR - Indicates if compentry function +# returns a (char *) + +find_path(Editline_INCLUDE_DIR NAMES histedit.h) +find_library(Editline_LIBRARIES NAMES edit libedit) + +if(Editline_INCLUDE_DIR) + # Check which standard of editline is installed on the system. + # https://github.com/CVC4/CVC4/issues/702 + include(CheckCXXSourceCompiles) + set(CMAKE_REQUIRED_QUIET TRUE) + set(CMAKE_REQUIRED_LIBRARIES ${Editline_LIBRARIES}) + set(CMAKE_REQUIRED_INCLUDES ${Editline_INCLUDE_DIR}) + check_cxx_source_compiles( + "#include + #include + char* foo(const char*, int) { return (char*)0; } + int main() { rl_completion_entry_function = foo; return 0; }" + Editline_COMPENTRY_FUNC_RETURNS_CHARPTR + ) + unset(CMAKE_REQUIRED_QUIET) + unset(CMAKE_REQUIRED_LIBRARIES) + unset(CMAKE_REQUIRED_INCLUDES) +endif() + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(Editline + DEFAULT_MSG Editline_INCLUDE_DIR Editline_LIBRARIES) +mark_as_advanced( + Editline_INCLUDE_DIR + Editline_LIBRARIES + Editline_COMPENTRY_FUNC_RETURNS_CHARPTR +) +if(Editline_LIBRARIES) + message(STATUS "Editline library: ${Editline_LIBRARIES}") +endif() diff --git a/cmake/FindReadline.cmake b/cmake/FindReadline.cmake deleted file mode 100644 index edac03027..000000000 --- a/cmake/FindReadline.cmake +++ /dev/null @@ -1,69 +0,0 @@ -# Find Readline -# Readline_FOUND - system has Readline lib -# Readline_INCLUDE_DIR - the Readline include directory -# Readline_LIBRARIES - Libraries needed to use Readline -# Readline_COMPENTRY_FUNC_RETURNS_CHARPTR - Indicates if compentry function -# returns a (char *) - -find_path(Readline_INCLUDE_DIR NAMES readline/readline.h) -find_library(Readline_LIBRARIES NAMES readline) - -# Try to compile and link a simple program against readline. 'libs' can be -# used to specify additional required libraries. -function(try_compile_readline libs _result) - set(CMAKE_REQUIRED_QUIET TRUE) - set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs}) - check_cxx_source_compiles( - " - #include - #include - int main() { readline(\"\"); return 0; } - " - ${_result} - ) - set(${_result} ${${_result}} PARENT_SCOPE) -endfunction() - -if(Readline_INCLUDE_DIR) - # We only need to figure out readline's additional libraries dependencies if - # we compile static. - # Note: It might be the case that we need to check for more/other libraries - # depending on what the installed version of readline is linked against - # (e.g., termcap, ncurses, ...). - find_library(TINFO_LIBRARY tinfo) - try_compile_readline(${TINFO_LIBRARY} OK) - if(OK) - list(APPEND Readline_LIBRARIES ${TINFO_LIBRARY}) - else() - message(FATAL_ERROR - "Could not link against readline. " - "Check CMakeError.log for more details") - endif() - - # Check which standard of readline is installed on the system. - # https://github.com/CVC4/CVC4/issues/702 - include(CheckCXXSourceCompiles) - set(CMAKE_REQUIRED_QUIET TRUE) - set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES}) - check_cxx_source_compiles( - "#include - #include - char* foo(const char*, int) { return (char*)0; } - int main() { rl_completion_entry_function = foo; return 0; }" - Readline_COMPENTRY_FUNC_RETURNS_CHARPTR - ) - unset(CMAKE_REQUIRED_QUIET) - unset(CMAKE_REQUIRED_LIBRARIES) -endif() - -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(Readline - DEFAULT_MSG Readline_INCLUDE_DIR Readline_LIBRARIES) -mark_as_advanced( - Readline_INCLUDE_DIR - Readline_LIBRARIES - Readline_COMPENTRY_FUNC_RETURNS_CHARPTR -) -if(Readline_LIBRARIES) - message(STATUS "Found Readline libs: ${Readline_LIBRARIES}") -endif() diff --git a/configure.sh b/configure.sh index f720e67c2..3bce5a548 100755 --- a/configure.sh +++ b/configure.sh @@ -64,7 +64,7 @@ The following flags enable optional packages (disable with --no-