From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id KLsPHNJM/WIVKwAAbAwnHQ (envelope-from ) for ; Wed, 17 Aug 2022 22:17:22 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id +C7+G9JM/WK0ZwAA9RJhRA (envelope-from ) for ; Wed, 17 Aug 2022 22:17:22 +0200 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 33E0FAC4E for ; Wed, 17 Aug 2022 22:17:22 +0200 (CEST) Received: from localhost ([::1]:37108 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oOPTZ-0003qc-Mk for larch@yhetil.org; Wed, 17 Aug 2022 16:17:17 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:56392) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oOPTL-0003mb-6f for guix-patches@gnu.org; Wed, 17 Aug 2022 16:17:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:35159) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oOPTK-00033N-Lk for guix-patches@gnu.org; Wed, 17 Aug 2022 16:17:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1oOPTK-0004RW-Gu for guix-patches@gnu.org; Wed, 17 Aug 2022 16:17:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 17 Aug 2022 20:17:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 57181 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: mail@maxheisinger.at Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.166076737617023 (code B ref 57181); Wed, 17 Aug 2022 20:17:02 +0000 Received: (at 57181) by debbugs.gnu.org; 17 Aug 2022 20:16:16 +0000 Received: from localhost ([127.0.0.1]:53141 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oOPSa-0004QV-AG for submit@debbugs.gnu.org; Wed, 17 Aug 2022 16:16:16 -0400 Received: from mail-ej1-f67.google.com ([209.85.218.67]:39860) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oOPSV-0004QD-IF for 57181@debbugs.gnu.org; Wed, 17 Aug 2022 16:16:15 -0400 Received: by mail-ej1-f67.google.com with SMTP id i14so26422058ejg.6 for <57181@debbugs.gnu.org>; Wed, 17 Aug 2022 13:16:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc; bh=nDVyUvwwis9U6SMmOhI0TCdYLQz69XENKTaoozAEQqw=; b=M3PFuiURJBI+0kcTakzNf43bOA9hCdCNaGeKVajdaxF6D+YM1O0GYGvCcl+vmuOdl9 Dt4HWnJeDhIL+2pTeLx7cA/558TnOqgLQsQKmL9gg8H8pDnBMmi+9DSvtJtxy8MCI9iG Cp5q0zaBnJJCfgFF1dVpJxgpfbicbQz3XxwZwAoXgUPTivYW5eH2jYQmJR6X3WEzbWih CzUtFr74i6g080WV9HJVeH0h5E/S+1G2bDO5g9Ws+HgwSh23elsuZCSYbAzmdrAWmZDE rVyQ/qRWlzZ7tKJrcDC3VYWIQk1muRPXoXr/uvbK6YMVF5pJBXSoqdT1fFjaOivjRCOp cbSw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc; bh=nDVyUvwwis9U6SMmOhI0TCdYLQz69XENKTaoozAEQqw=; b=EJhs+Ydb+a9n4plYoS/jWP/tWcGkDDDKI76zeDs4BvRPn8edHVpAjcix3DsNdXy/pI 3wLh+2RzL+XhV2LCvJLX8SykRFAQnabWQ39UeWoKAN5bd1NRBdbAOgVhrLW37yj8bMNE mqSdnNiyIBf4JFofcRVmV0jcntREa8zx3Ek+mu8mnwzcIhJgS3MsGm6uK45oC7N8UhrK BuOyEP3sC/2djuf2dA9dS6NdMUDyLnZ0O05f/G+06lFKx8tPAhglfNxsWfosesqduyWi JA+SyZAaz5u8uRCbGSUDP9IpZLfT9Tivn1Upafh80x5UkUAOo+Ym7qMA2XgW/gqhJhDi dOBw== X-Gm-Message-State: ACgBeo0WBO3X4IJgt/LgyyC5fgJL0WSLNrv++/7n/sxQ3X+Tlc/uB2Pj Oq8g39Udp/Nx5kx5y79qE1k= X-Google-Smtp-Source: AA6agR5+MSqdxBohngMH5441IgqE70/YnLW61bsPZ50W8yUmL430H7W9ackOaGLhAKMbb9m62+MwAA== X-Received: by 2002:a17:906:58c6:b0:731:39e0:3eb8 with SMTP id e6-20020a17090658c600b0073139e03eb8mr18400204ejs.205.1660767365572; Wed, 17 Aug 2022 13:16:05 -0700 (PDT) Received: from nijino.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id c21-20020a170906341500b00730cc173c6asm7225308ejb.43.2022.08.17.13.16.04 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 17 Aug 2022 13:16:04 -0700 (PDT) Message-ID: From: Liliana Marie Prikler Date: Wed, 17 Aug 2022 22:16:03 +0200 In-Reply-To: <87wnb74c7n.fsf@maxheisinger.at> References: <87wnb74c7n.fsf@maxheisinger.at> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.42.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN X-Migadu-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1660767442; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=nDVyUvwwis9U6SMmOhI0TCdYLQz69XENKTaoozAEQqw=; b=gRfL7jud1oqljSXzvXcVazYDVWqNhmLikYfG7UKWpdpRIE/mlM+ZOIMY/2LZP2k6WPq/lb Br8ewQjHCjCLiXNsI/ngUR/lHjTlgO120NkbzYFJilpkZF8Kk5W9DxqBHlp703FhdJxLwY 8M48T84vz/9kRNCQKetLnjkj1KAaBT1Y28cY21YJrDvUyH3W/dFYXdsTynHml+KQcOQSS3 sNb2q/1eOe/+avdonuMkOlEQQymc8wPsfUGHabI+UiltUzJJZM33P9Uto+9MVQmwbA9mQp mPqloxqjUi+keMBd6oCYFgKro3F3573f50Za/aVtVbfmh3KPHRm9L9SOm1wAyA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1660767442; a=rsa-sha256; cv=none; b=ktfj5i3RIgblWrfDx5+SMfrDmmasBdZ7KymZFv67+TD1lXIKIaXWuqiFe+ggcD6fBueVe/ 5ODg21uv6ei716460VkCMFnm8Q3zblBTSw8Q+MDZ1ltIS+Dncz89pDd5uNcJ7mVw+8tLbV 7BmYuLwPeATsfZHnA5hkxtgsKrTv8t9pYqpl8kdTsuoUSVvZha7OVlvMuxYP6q3SDpgaYq BO64JMAzoEd2DBrBDujk6PIuiYrPQnXd0c7k0EvSe/4gcOWa+NKVcqpC2dGhfUg2Qb9ZLv CSvGMZazKrldYWm2FGwmh9r2Cu+GWh/irXg7dwDbDVudR+/tA5y+iv8/nY9iAA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=M3PFuiUR; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: 6.34 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=M3PFuiUR; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: 33E0FAC4E X-Spam-Score: 6.34 X-Migadu-Scanner: scn0.migadu.com X-TUID: PmwdpQUjBBqq Hi, Am Mittwoch, dem 17.08.2022 um 08:26 +0200 schrieb mail@maxheisinger.at: > [...] [W]e 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? Only running simple tests is preferable to running no tests at all. If you think that unvendoring everything is an unreasonable amount of work, that's a viable solution. However, we do strive to offer complete packages, so feel free to do 1. :) If you need some pointers as for the test files, ppsspp includes both another package's source (not so great, needs better unvendoring) and test files, and there's probably some other packages you could consult as well. > > "Incremental solving" sounds easier to understand. > > Changed it. LGTM. > > 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). Note that python is now missing from native-inputs, but python-lit is in there. I suppose you need python both as input (for linking) and native-input (to run whatever python-lit is supposed to do). Cheers