search

usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

Get rid of `readline` and GPL license #675

Closed Tomaqa closed 8 months ago

Tomaqa commented 9 months ago

.. unless there is a serious reason why readline should be preferred over libedit (or how is is called). I also think that CMAKE_FLAGS=-DENABLE_LINE_EDITING:BOOL=ON should be enabled by default, that is, to link with a line editing tool by default. I do not see any drawback to doing so.

blishko commented 9 months ago

We explicitly make line editing opt-in, in order to not force unnecessary dependency on users who do not need it.

Tomaqa commented 9 months ago

I see, so it is not an integral part of the package and CMake has to check/download it, right?

blishko commented 9 months ago

I believe CMake will check if it can find it on your system and if not, it will report error (when you requested build with line editing capabilities).

Tomaqa commented 9 months ago

I think it would be neat if it was an optional dependency, but I guess that would require dynamic linkage instead of static. Then the library would be used only if it exists at runtime. But I guess none of us can do this with not too much effort .. Until then, I guess that the current solution is sufficient.

Tomaqa commented 8 months ago

There is some reference to readline in ./regression (run-test.sh), but I do not understand the purpose of the tests (they fail on my machine) and not sure if its still being used.

aytey commented 8 months ago

In run-test.sh, can you just change -lreadline to be -ledit?

blishko commented 8 months ago

./regression/run-test.sh can be removed, it is not used anymore. Regression tests use run-test-notiming.sh which don't mention readline.

aytey commented 8 months ago

./regression/run-test.sh can be removed, it is not used anymore.

Seems like a better solution :D