From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:46845) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYtzG-000458-FK for guix-patches@gnu.org; Mon, 17 Dec 2018 09:35:19 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYtz5-0002uY-7E for guix-patches@gnu.org; Mon, 17 Dec 2018 09:35:12 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:46738) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gYtz4-0002t1-Dp for guix-patches@gnu.org; Mon, 17 Dec 2018 09:35:03 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gYtz4-0007I8-A9 for guix-patches@gnu.org; Mon, 17 Dec 2018 09:35:02 -0500 Subject: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. Resent-Message-ID: From: Amin Bandali References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> Date: Mon, 17 Dec 2018 09:34:11 -0500 In-Reply-To: <20181217072921.GG3468@macbook41> (Efraim Flashner's message of "Mon, 17 Dec 2018 09:29:21 +0200") Message-ID: <87efag6x3w.fsf@aminb.org> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Efraim Flashner Cc: 33764@debbugs.gnu.org Hi Ludo=E2=80=99, Efraim, Thank you both for the feedback. I=E2=80=99ve responded below. On 2018-12-17 9:29 AM, Efraim Flashner wrote: > On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Court=C3=A8s wrote: >> > (native-inputs >> > - `(("python" ,python-2))) >> > + `(("which" ,(@ (gnu packages base) which)) >> > + ("python" ,python-wrapper))) >>=20 >> Please add #:use-module (gnu packages which) so you don=E2=80=99t have t= o resort >> to the @ notation. Will do for the next version of the patch, thanks. >> > +(define-public python-z3 z3) >>=20 >> Is this variable necessary? Note that this does not create a >> =E2=80=9Cpython-z3=E2=80=9D package. I see! I thought that it /would/ create a python-z3 package; but then again I=E2=80=99m very much a Guix newb :) Since I added a python2-z3, I th= ought I would also add a python-z3 for =E2=80=98symmetry=E2=80=99 in case someone= expects it. Should I then add a (define-public python-z3 (package inherit z3)) if we decide to add the python2-z3 bindings? >> > +(define-public python2-z3 >> > + (package (inherit python-z3) >>=20 >> This definition cannot be in python.scm; it must be in the same file as >> =E2=80=98z3=E2=80=99 or we can get =E2=80=9Cunbound variable=E2=80=9D er= rors while loading either of >> these two modules. Oh I see. If we choose to keep it (add it), I=E2=80=99ll move it to maths.= scm. >> Also, as we=E2=80=99re approaching end-of-life upstream for Python 2.x, = we now >> avoid creating =E2=80=9Cpython2-=E2=80=9D packages, unless we cannot avo= id it for some >> reason. Do you think we could do without this =E2=80=9Cpython2-z3=E2=80= =9D package? >>=20 > > Currently our z3 package builds python2 bindings What Efraim said. Since the current z3 provides python2 bindings, I thought I would preserve that option by adding a python2-z3 in case anyone wants to continue to use the python2 bindings. I=E2=80=99m Cc=E2=80=99ing Marius who=E2=80=99s one of the recent committer= s to the z3 package definition. Marius, any thoughts on whether we should keep the python2 bindings around or do away with them? >> Could you send an updated patch? If you think we really need >> =E2=80=9Cpython2-z3=E2=80=9D, please make it a separate patch. Sure. I=E2=80=99ll send an update patch (or patches) once we figure out wh= ether we should keep the python2 bindings around. > > We should also check that the other packages that use z3 aren't > expecting the python2 bindings when built with the python3 bindings. > Right. grepping through the codebase, I see that only two other packages depend on z3: cubicle (in maths.scm) and yosys (in fpga.scm). cubicle is an ocaml package and doesn=E2=80=99t seem to use the python bind= ings of z3, and yosys seems to only use z3 as an executable, not a library. So, it appears to me that as of now, there are no packages that depend on the python2 bindings of z3. If so, do we drop python2-z3 (and also python-z3) altogether and just switch z3 to python3? Best, amin