GNU bug report logs - #46329
[PATCH] Add z3 OCaml bindings

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 46329 in the body.
You can then email your comments to 46329 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: [PATCH] Add z3 OCaml bindings
Date: Fri, 5 Feb 2021 17:46:41 +0100

[Message part 1 (text/plain, inline)]

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?

[0001-gnu-z3-Build-and-install-OCaml-bindings.patch (text/x-patch, attachment)]

Message #8 received at 46329 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 46329 <at> debbugs.gnu.org
Subject: Re: bug#46329: [PATCH] Add z3 OCaml bindings
Date: Fri, 19 Mar 2021 22:06:43 +0100

Hello!

Julien Lepiller <julien <at> lepiller.eu> skribis:

> 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 :)).

It’d be ideal if these could be built separately.  Like, we’d build z3,
and the ocaml-z3 package would depend on z3 (but use the same source
tarball as z3).

Does that seem feasible?

> 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?

I guess it depends on which one is the most widespread convention.

>>From 651701f64eaa81baf57634fc36efdab4d263e2b6 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien <at> lepiller.eu>
> 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.

I think a separate package as outline above would be slightly nicer, but
otherwise this patch LGTM.

Thanks,   :-)
Ludo’.

Message #11 received at 46329 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 46329 <at> debbugs.gnu.org
Subject: [PATCH v2] Add z3 OCaml bindings
Date: Fri, 8 Oct 2021 13:26:18 +0200

[Message part 1 (text/plain, inline)]

Hi!

I finally managed to build a separate package out of z3. It wasn't
easy, because the build system wants to rebuild a z3 and doesn't let
you install only the bindings. I managed to make it do just that: build
the bindings and install them, and link to the existing z3 package.

[0001-gnu-Add-ocaml-z3.patch (text/x-patch, attachment)]

Message #16 received at 46329-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 46329-done <at> debbugs.gnu.org
Subject: Re: [bug#46329] [PATCH v2] Add z3 OCaml bindings
Date: Thu, 28 Oct 2021 00:27:52 +0200

Le Fri, 8 Oct 2021 13:26:18 +0200,
Julien Lepiller <julien <at> lepiller.eu> a écrit :

> Hi!
> 
> I finally managed to build a separate package out of z3. It wasn't
> easy, because the build system wants to rebuild a z3 and doesn't let
> you install only the bindings. I managed to make it do just that:
> build the bindings and install them, and link to the existing z3
> package.

After more than two weeks of silence, pushed to master as
a8c69e22ee2f9e7b487ffe0b567297f28863128d

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.