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 OAwWBexJ+mLoSgAAbAwnHQ (envelope-from ) for ; Mon, 15 Aug 2022 15:28:12 +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 WG9RBexJ+mLLPwAA9RJhRA (envelope-from ) for ; Mon, 15 Aug 2022 15:28:12 +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 48FD41EA15 for ; Mon, 15 Aug 2022 15:28:11 +0200 (CEST) Received: from localhost ([::1]:33164 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oNa8Y-0003vc-2X for larch@yhetil.org; Mon, 15 Aug 2022 09:28:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:53870) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oNa8Q-0003vU-Uz for guix-patches@gnu.org; Mon, 15 Aug 2022 09:28:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:51541) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oNa8Q-00039l-M0 for guix-patches@gnu.org; Mon, 15 Aug 2022 09:28:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1oNa8Q-00018c-IB for guix-patches@gnu.org; Mon, 15 Aug 2022 09:28: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: Mon, 15 Aug 2022 13:28: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: Maximilian Heisinger Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.16605700444312 (code B ref 57181); Mon, 15 Aug 2022 13:28:02 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Aug 2022 13:27:24 +0000 Received: from localhost ([127.0.0.1]:41284 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNa7o-00017U-02 for submit@debbugs.gnu.org; Mon, 15 Aug 2022 09:27:24 -0400 Received: from mail-ej1-f65.google.com ([209.85.218.65]:36704) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNa7i-00017D-La for 57181@debbugs.gnu.org; Mon, 15 Aug 2022 09:27:22 -0400 Received: by mail-ej1-f65.google.com with SMTP id fy5so13534422ejc.3 for <57181@debbugs.gnu.org>; Mon, 15 Aug 2022 06:27:18 -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=nbfWErX7lv8n4APcaXonAPkKSVYsiEGsvvOEw694bvA=; b=FvcCsRB0Zljbj0oa+fDVUGrDZ49gYBDHVvef1xqCQF+KIls40nL9xID+YpCYeZh2is umxemOQijbE38xP5XOI/vUETRdK8bUXxH7zdxyBK1UeVrz6xMVlYdI/bcHUmbrJWITlr OnGBDS+lo+s4dW6ql2h70SlqR36hHrKVQCbl5BsLfwZnxi+AWfjMf5TzJmKk8BpGSpm2 aJxyCUuzGcfuy0sofgVeAlVfNgFBWsgMR9hKeFk37nuHZXKIQWkAnvIFZsCqkS5i7Mzj 2TgoJFS92SJh1Kk95Vxj7ExBzPqPZ01tM1utVARRcu9f2T78pKEmXWT6tffudJv09O3l MFPQ== 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=nbfWErX7lv8n4APcaXonAPkKSVYsiEGsvvOEw694bvA=; b=R4r0SAxwRF1+OMBbNyy6jkKjutH2/PRqC5hjvMid4Sje9UFdKBsl1vrTkF2KxPpuwi 8JQtBdf7jeeh0k0RJd1T28HUmhRJXfwMhORcbjjkMPivx/pRpIMwhMh0Rp6O0xsuDctL K+C1j88nl4FLQQcKy2t+MwWFqe+5UOHp0ZIQza3KBPANGQ4TLed07mSld47a5LFlznD5 zJ4sTWwM/x+ZHtcJ+iBz1EW9T2M/tmw3t0/JuE5h7bcO23oMwqozo2fOq+Dju+/RY0Tn 6KxU5E9nd2wz8Jw3QgSwlKjhAbX69QeH6vTjE93+uKU153uJmJFAbQsviTYUCSkdE29d 2A4g== X-Gm-Message-State: ACgBeo0xyxiaBvszz7D4knm5JZD81auBHM7A8/mStXW8SG2WDN/iB9v3 NHJCndQ+/gBZSx6zOXLLVus= X-Google-Smtp-Source: AA6agR6OjrITajdIoQdbfPp2RsiY92k+0jpfYwQjI8QPWNv9aItsvv/ioSliC4YkPqo6amRJaX7odQ== X-Received: by 2002:a17:907:94c3:b0:730:9641:8dd8 with SMTP id dn3-20020a17090794c300b0073096418dd8mr10685280ejc.586.1660570032781; Mon, 15 Aug 2022 06:27:12 -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 wi2-20020a170906fd4200b007308bebce51sm4126696ejb.171.2022.08.15.06.27.12 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 Aug 2022 06:27:12 -0700 (PDT) Message-ID: <742d924abc9cfa0b2073c053e229e8ee437704ce.camel@gmail.com> From: Liliana Marie Prikler Date: Mon, 15 Aug 2022 15:27:11 +0200 In-Reply-To: <132482353.134362.1660560630571@ox93.mailbox.org> References: <1dbd4bac9403ed4dd17de75dfc2d210daf2d2ea3.camel@gmail.com> <1840023126.104586.1660505267957@ox93.mailbox.org> <4349f97ccc76a0ee579442c3a4f50b4ba2f4f34c.camel@gmail.com> <132482353.134362.1660560630571@ox93.mailbox.org> 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=1660570091; 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=nbfWErX7lv8n4APcaXonAPkKSVYsiEGsvvOEw694bvA=; b=aHE84P7qj4sNKMGVc8ADJzjb8Ik7IZjpmBGO5Z4RtQfFR0XY07LC+LcMzL0EdFrOx3vz0X Go653yHrfOiz368l36eGzf0KMfQ3FfgnsF+q03LnKgeXt9IWjXaRZ0q71a+yRvW1046j6V hJd1nGB2LSi/STJ2kjQE8Nna05TMml5gwIVoF6K9yPUNB1N8HLVobHa7kimdKw0DWXm9zj BZMxc04qXuBBaT1Sn6wHZ4hO6b+oyLXuVel/GUOLsozgLRB/69ATEdl1Wvue0emQcXnnPx B72kE5JHQoTwo4Rn5qwgUZcZaODgmYwCKYghXVM+T/dxMhgS4ag75tKhs250BA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1660570091; a=rsa-sha256; cv=none; b=Og232zzFwDSMdTpwX8FXLxM+MBiN7/FvOfB6JdWNVTVQN81GGZu7lQDVXR9z8t/YcawX4b ie3IyI1COvXeqoEu6alrQQl9xnpuIYoMDmhDDqUpFYqkT+4SDXn4baszrLgexqrsnDHWkt XB1NnGu2yY7DDfRMWWFpo0IDubpJBvNRYvS49sWU4B+9SWESRdBm9e7pqFNrXxu7J63jon PU/ke1X9Hs1RTGf6r01y/y2E9O2Qc58C50a6iNYuv855x8P1wvUtVzYiptPh8gkjz67JOQ lP4mlIUNN+hQAyAWN5HPhh6PGt6Ww7FmEYGxyXqtFoYxmwEfSIG4eL5fNwvm3Q== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=FvcCsRB0; 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: 4.54 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=FvcCsRB0; 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: 48FD41EA15 X-Spam-Score: 4.54 X-Migadu-Scanner: scn0.migadu.com X-TUID: LmCUbj2twcr8 Hi, I've pushed kissat with some heavy edits. In particular, I - 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. Am Montag, dem 15.08.2022 um 12:50 +0200 schrieb Maximilian Heisinger: > Hi, > > sorry, doing the correct CC now. > > > Recursive checkout doesn't really sound "mini". > > Oh, there's some history behind the mini...  CryptoMiniSat adds some > stuff commonly needed in cryptography to MiniSat, which is a common > base for many other SAT solvers. I know about the existence of Minisat, but 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? > The library interfaces mimic this and also > +allow IPASIR-esque incremental use, including assumptions. "Incremental solving" sounds easier to understand. > + (inputs (list zlib boost)) > + (native-inputs (list python python-lit)) If you have a Python interface, you probably also need python in inputs, no? Cheers