03.09.2024 19:07, Kirill A. Korinsky пишет:
> Here an updated diff where I've backported patch from upstream which fixed
> crash on OpenBSD as side effect.
Thanks, committed.
On Sat, 31 Aug 2024 21:08:15 +0200,
Klemens Nanni wrote:
>
> You're right, :Q remained from an earlier iteration.
> I dropped it, yielding correct commands now, thanks.
>
Here an updated diff where I've backported patch from upstream which fixed
crash on OpenBSD as side effect.
I also drop testi
31.08.2024 18:10, Kirill A. Korinsky пишет:
> not sure that this :Q is required. If I run it with :Q z3 complains as:
>
> (error "line 1 column 1: unexpected character")
> (error "line 1 column 19: unexpected token used as datatype name")
> (error "line 1 column 20: unexpected characte
On Sat, 31 Aug 2024 16:03:30 +0200,
Klemens Nanni wrote:
>
> 31.08.2024 16:35, Klemens Nanni пишет:
> > 30.08.2024 22:17, Kirill A. Korinsky пишет:
> >> On Tue, 27 Aug 2024 21:59:25 +0200,
> >> Klemens Nanni wrote:
> >>>
> >>> New diff including all the feedback above, you can now hack on the po
31.08.2024 16:35, Klemens Nanni пишет:
> 30.08.2024 22:17, Kirill A. Korinsky пишет:
>> On Tue, 27 Aug 2024 21:59:25 +0200,
>> Klemens Nanni wrote:
>>>
>>> New diff including all the feedback above, you can now hack on the port and
>>> iterate over 'make retest' until it no longer crashes (or you
30.08.2024 22:17, Kirill A. Korinsky пишет:
> On Tue, 27 Aug 2024 21:59:25 +0200,
> Klemens Nanni wrote:
>>
>> New diff including all the feedback above, you can now hack on the port and
>> iterate over 'make retest' until it no longer crashes (or you give up) ;-)
>>
>
> Here an updated version
On Tue, 27 Aug 2024 21:59:25 +0200,
Klemens Nanni wrote:
>
> New diff including all the feedback above, you can now hack on the port and
> iterate over 'make retest' until it no longer crashes (or you give up) ;-)
>
Here an updated version based on yours. Changes:
- improved testing to use sm
Klemens,
Thanks for review and tweak of the diff.
On Tue, 27 Aug 2024 21:59:25 +0200,
Klemens Nanni wrote:
>
> MODPY_RUNDEP=No seems missing unless z3 really needs python at runtime.
>
It has python binding and python API, and can be used from python. Not sure
that it justify it.
> >>
> >> Bu
26.08.2024 21:45, Kirill A. Korinsky пишет:
> ports@,
>
> Here an update version of this diff
VERSION is used once and can be inlined.
PKGNAME not needed as DISTNAME is already lowercase.
One patch had offsets (need 'make update-patches') and could be simplified
to make it obviuos what we patch
On Mon, 26 Aug 2024 21:36:45 +0200,
A Tammy wrote:
>
>
> > After spending some time to dig into the issue which lead to crash, I had
> > discovered that such crash doesn't reproduced if I build z3 wihtout
> > optimization (-O0).
>
>
> This sounds like a bug worthy of telling upstream about.
>
On 8/26/24 2:45 PM, Kirill A. Korinsky wrote:
> ports@,
>
> Here an update version of this diff
>
> On Wed, 21 Aug 2024 00:30:09 +0200,
> Kirill A. Korinsky wrote:
>> ports@,
>>
>> Here is a clean update of math/z3 to the latest release.
>>
>> Changelog:
>> https://github.com/Z3Prover/z3/releas
ports@,
Here an update version of this diff
On Wed, 21 Aug 2024 00:30:09 +0200,
Kirill A. Korinsky wrote:
>
> ports@,
>
> Here is a clean update of math/z3 to the latest release.
>
> Changelog:
> https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0
>
> Tested on -current/amd64.
>
> So the
Frederic Cambus wrote:
> Hi ports@,
>
> Here is a diff to update z3 to 4.8.16.
>
> Some functions have been removed from the library, so a major bump
> is needed.
>
> Comments? OK?
ok op@
I somehow managed to boostrap F* with OCaml using the updated z3. It's
still half broken (not the parts
On Wed Oct 16, 2019 at 02:59:32AM +, wen heping wrote:
> Hi,ports@:
>
>Here is a patch for math/z3 to update to 4.8.6.
>It build well and run well on amd64-current system.
>It defines NO_TEST and no other ports depend on it.
>
> Comments? OK?
> wen
OK rsadowski@
> Index: Makefil
On 2019/06/05 16:10, Remi Pointel wrote:
> > The GH_* stuff in this is broken. If GH_ACCOUNT and GH_PROJECT are
> > present there should always be GH_TAGNAME or GH_COMMIT.
>
> Exactly, attached is the diff using GH_TAGNAME.
>
> I need to set DISTNAME because by default "DISTNAME =
> ${GH_PROJECT}
The GH_* stuff in this is broken. If GH_ACCOUNT and GH_PROJECT are
present there should always be GH_TAGNAME or GH_COMMIT.
Exactly, attached is the diff using GH_TAGNAME.
I need to set DISTNAME because by default "DISTNAME =
${GH_PROJECT}-${GH_TAGNAME:C/^v//}" and PKGNAME because the upper Z o
On 2019/06/04 14:45, Remi Pointel wrote:
> Hi,
>
> this diff updates z3 to latest release.
>
> Ok?
>
> Cheers,
>
> Remi.
> Index: Makefile
> ===
> RCS file: /cvs/ports/math/z3/Makefile,v
> retrieving revision 1.13
> diff -u -p -u
On Tue, Jun 04, 2019 at 02:45:46PM +0200, Remi Pointel wrote:
> this diff updates z3 to latest release.
Brief summay of what changed or why you bumped the major? Or a link?
On Sat Jan 19, 2019 at 10:56:35AM +0100, Remi Pointel wrote:
> Hi,
>
> this is the diff to update z3 to latest release.
>
> Ok?
>
> Cheers,
>
> Remi.
Maybe it's a good idea to move to cmake as build system? Perhaps
consumers more happy with the cmake targets!?
RS
Index: Makefile
OK
În 14 decembrie 2018 15:02:35 EET, Remi Pointel a scris:
>Hi,
>
>this diff updates z3 to latest release.
>
>Ok?
>
>Cheers,
>
>Remi.
Le 10-04-2018 06:26, Matthew Martin a écrit :
Update z3; builds here with clang 6. Enable tests while here.
- Matthew Martin
Hi,
thanks it's commited.
Cheers,
Remi.
21 matches
Mail list logo
