Hi,

> - fixed the commit message,
> - hard-coded the compression binaries (and made them regular inputs),
> - fixed the actual test failure,
> - used G-Expressions rather than quasiquoting.
>
> See 9ddd37d6ab59e2519bbcefad15ce62561128f0ee.

Thank you very much!  This really is clearer, better, and gives me more
pointers to research about Guix.

> the problem here is rather that cryptominisat seems to pull in lots of
> stuff that we'd rather have packaged separately instead of vendored
> (e.g. googletest).  Could you try unvendoring those things and place
> the remaining parts in the right location without a recursive
> checkout?

Yes, that would be better... Then we have two choices now I think:

 1. Try to unvendor everything and add minisat as transformed package
    with different sources + lingeling as a new package.  This would
    also still require to download the external test files as additional
    source repositories.
 2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat
    offers that is meant to build a simpler binary, but also deactivates
    more complex tests.  We still build a complex binary (i.e. Boost
    program options for options parsing) by not setting it, but instead
    substitute the query for the option in the  ~test/CMakeLists.txt~
    file.  Additionally, we substitute some other issues away.

The second option loses some scripts and the more comprehensive tests.
I would argue though, that these would be better suited for developing
the solver and less for such a package management situation.  What is
your opinion about this trade-off?

> "Incremental solving" sounds easier to understand.

Changed it.

> If you have a Python interface, you probably also need python in
> inputs, no?

True - it is better to directly expose it.  I also took another look at
the solver's capabilities and output in more detail and added
python-numpy (required dependency for the py API) and sqlite (optional
dependency used for collecting statistics).

Thank you again for your patience and effort!  You find my updated patch
attached.

Best regards (now even written from an Emacs mail client),
Max