From patchwork Fri Feb 5 16:46:41 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Julien Lepiller X-Patchwork-Id: 26922 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id CE32827BC22; Fri, 5 Feb 2021 17:13:00 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.8 required=5.0 tests=BAYES_00,DKIM_SIGNED, MAILING_LIST_MULTI,RCVD_IN_MSPIKE_H4,RCVD_IN_MSPIKE_WL,SPF_HELO_PASS, T_DKIM_INVALID,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.2 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 4174427BC21 for ; Fri, 5 Feb 2021 17:12:59 +0000 (GMT) Received: from localhost ([::1]:35130 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1l84fC-00049Y-Dk for patchwork@mira.cbaines.net; Fri, 05 Feb 2021 12:12:58 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42802) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1l84H8-0002j8-Ci for guix-patches@gnu.org; Fri, 05 Feb 2021 11:48:06 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:33044) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1l84H4-00070y-9U for guix-patches@gnu.org; Fri, 05 Feb 2021 11:48:05 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1l84H4-0006vI-8L for guix-patches@gnu.org; Fri, 05 Feb 2021 11:48:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#46329] [PATCH] Add z3 OCaml bindings Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 05 Feb 2021 16:48:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 46329 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 46329@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.161254363626552 (code B ref -1); Fri, 05 Feb 2021 16:48:02 +0000 Received: (at submit) by debbugs.gnu.org; 5 Feb 2021 16:47:16 +0000 Received: from localhost ([127.0.0.1]:44590 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1l84GJ-0006uB-KO for submit@debbugs.gnu.org; Fri, 05 Feb 2021 11:47:15 -0500 Received: from lists.gnu.org ([209.51.188.17]:54764) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1l84GH-0006u4-PA for submit@debbugs.gnu.org; Fri, 05 Feb 2021 11:47:14 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42604) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1l84GH-00023c-CP for guix-patches@gnu.org; Fri, 05 Feb 2021 11:47:13 -0500 Received: from lepiller.eu ([89.234.186.109]:44540) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1l84GC-0006fI-KF for guix-patches@gnu.org; Fri, 05 Feb 2021 11:47:13 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id fa4cc4af for ; Fri, 5 Feb 2021 16:46:59 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:mime-version:content-type; s=dkim; bh=a12 ZdsekdQ7Q8D378ZFzsYB+dowcX+n9M3bm7SlmjYA=; b=it5NY4PerODFVlC6QQ8 H0Q1kY9evmnBPNL7oShsmm0PdKRWMqb4u3BHz5ruGVuCENaRsEPKdpV+LkP/pr39 l5bkV+GZyOyO//gHhlOlMD1N6HXzXAsVwx5+gCEPnepEjVAiBUzBj1O8OJHIoe+W eA0c07gGareJHou7Vnp858Jqz3R+vF47M9O8dZxZMcQ4ebKbF2FDn5UHWmsgb3Vb VVJ06dpVm8uMmhZunoinIh4dpydiHpGTox3fX6D1NkKg5CVZfH2ofExEgqjBPwg9 2pd2W8VptX8YbfJBYQ7XtBgWlRH1n9akrc7opJGQrDypSfctgK7S4Xv5GI+o9KPm 17w== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 2a61fec0 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Fri, 5 Feb 2021 16:46:58 +0000 (UTC) Date: Fri, 5 Feb 2021 17:46:41 +0100 From: Julien Lepiller Message-ID: <20210205174641.166aec6f@tachikoma.lepiller.eu> X-Mailer: Claws Mail 3.17.8 (GTK+ 2.24.32; x86_64-pc-linux-gnu) MIME-Version: 1.0 Received-SPF: pass client-ip=89.234.186.109; envelope-from=julien@lepiller.eu; helo=lepiller.eu X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action 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+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches Hi Guix! This patch adds the OCaml bindings for the z3 package. I install it to a separate output (but this only saves 3MB, maybe not that important). I'm thinking we could build other bindings too, and it would be nice to separate them also (after all, we probably don't need all of them at the same time :)). One issue is that this package installs the bindings to the Z3 ocaml package. However, in opam, they override the install directory to be z3, so we might have issues with dependents. Do you think I should also override the name of the directory? From 651701f64eaa81baf57634fc36efdab4d263e2b6 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Tue, 2 Feb 2021 22:17:19 +0100 Subject: [PATCH] gnu: z3: Build and install OCaml bindings. * gnu/packages/maths.scm (z3)[outputs]: Add ocaml output. [arguments]: Build and install OCaml bindings. --- gnu/packages/maths.scm | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index eff1480e62..2797bc8ae4 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -116,6 +116,7 @@ #:use-module (gnu packages mpi) #:use-module (gnu packages multiprecision) #:use-module (gnu packages netpbm) + #:use-module (gnu packages ocaml) #:use-module (gnu packages onc-rpc) #:use-module (gnu packages pcre) #:use-module (gnu packages popt) @@ -4741,6 +4742,7 @@ as equations, scalars, vectors, and matrices.") (base32 "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx")))) (build-system gnu-build-system) + (outputs '("out" "ocaml")) (arguments `(#:imported-modules ((guix build python-build-system) ,@%gnu-build-system-modules) @@ -4760,8 +4762,16 @@ as equations, scalars, vectors, and matrices.") (("#include ") "")) #t)) (add-before 'configure 'bootstrap - (lambda _ - (invoke "python" "scripts/mk_make.py"))) + (lambda* (#:key outputs #:allow-other-keys) + (let ((ocaml (assoc-ref outputs "ocaml")) + (out (assoc-ref outputs "out"))) + (setenv "OCAMLFIND_LDCONF" "ignore") + (setenv "OCAMLFIND_DESTDIR" (string-append ocaml "/lib/ocaml/site-lib")) + (mkdir-p (string-append ocaml "/lib/ocaml/site-lib")) + (substitute* "scripts/mk_util.py" + (("LIBZ3 = LIBZ3") + (string-append "LIBZ3 = LIBZ3 + ' -dllpath " out "/lib'"))) + (invoke "python" "scripts/mk_make.py")))) ;; work around gnu-build-system's setting --enable-fast-install ;; (z3's `configure' is a wrapper around the above python file, ;; which fails when passed --enable-fast-install) @@ -4769,6 +4779,7 @@ as equations, scalars, vectors, and matrices.") (lambda* (#:key inputs outputs #:allow-other-keys) (invoke "./configure" "--python" + "--ml" (string-append "--prefix=" (assoc-ref outputs "out")) (string-append "--pypkgdir=" (site-packages inputs outputs))))) (add-after 'configure 'change-directory @@ -4786,7 +4797,11 @@ as equations, scalars, vectors, and matrices.") (invoke "./test-z3" "/a")))))) (native-inputs `(("which" ,which) - ("python" ,python-wrapper))) + ("python" ,python-wrapper) + ("ocaml" ,ocaml) + ("ocaml-findlib" ,ocaml-findlib))) + (inputs + `(("ocaml-zarith" ,ocaml-zarith))) (synopsis "Theorem prover") (description "Z3 is a theorem prover and @dfn{satisfiability modulo theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.") -- 2.30.0