llvm dev - Feb 2019 - [cfe-dev] clang in official apt repo built without z3 support

On Tue, 12 Feb 2019, 14:32 Paulo Matos <pmatos at linki.tools wrote:
>
>
> On 12 February 2019 18:59:21 CET, Mikhail Ramalho <
> mikhail.ramalho at gmail.com> wrote:
> >I _think_ there is a problem with the license as well: Z3 is MIT, so
> >clang
> >would have to be released with Z3's license.
>
> I don't think that's a problem. You are not releasing z3 with
clang. This
> is an apt repo.

Well, I'm not an expert, but building clang linked with z3 and offering it
online for people to download seems a lot like a release.

I don't it matters if it's a tar.gz or an apt repo.

You just need to add the correct dependency on the repo and build using 
z3
> support.
>
> >
> >On Tue, 12 Feb 2019, 09:24 Roman Lebedev via cfe-dev
> ><cfe-dev at lists.llvm.org
> >wrote:
> >
> >> On Tue, Feb 12, 2019 at 4:13 PM Paulo Matos via cfe-dev
> >> <cfe-dev at lists.llvm.org> wrote:
> >> >
> >> > Hello,
> >> >
> >> > I am trying to run scan-build with crosscheck with z3 like:
> >> > scan-build-9 -o scan-report_cc -analyzer-config
> >> > 'crosscheck-with-z3=true' make
> >> >
> >> > Unfortunately the packages in then official repo here:
> >> > https://apt.llvm.org/
> >> >
> >> > are build without Z3 support so I get:
> >> > fatal error: error in backend: Clang was not compiled with Z3
> >support,
> >> > rebuild with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON
> >> >
> >> > Is there a reason for this? And is it possible to change it?
> >> The version of z3 in debian is very ancient:
> >> https://tracker.debian.org/pkg/z3    4.4.1-0.4
> >>
> >> LLVM needs 4.7 or something.
> >> There is a bug report:
> >> https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=909494
> >>
> >> This also affects other LLVM-"affiliated" projects, like
alive and
> >souper.
> >>
> >> > Kind regards,
> >> > --
> >> > Paulo Matos
> >> Roman.
> >>
> >> > _______________________________________________
> >> > cfe-dev mailing list
> >> > cfe-dev at lists.llvm.org
> >> > https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
> >> _______________________________________________
> >> cfe-dev mailing list
> >> cfe-dev at lists.llvm.org
> >> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
> >>
>
> --
> Paulo Matos
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20190212/a2d1cc42/attachment.html>

On 12/02/2019 19:49, Mikhail Ramalho wrote:
> 
> 
> On Tue, 12 Feb 2019, 14:32 Paulo Matos <pmatos at linki.tools wrote:
> 
> 
> 
>     On 12 February 2019 18:59:21 CET, Mikhail Ramalho
>     <mikhail.ramalho at gmail.com <mailto:mikhail.ramalho at
gmail.com>> wrote:
>     >I _think_ there is a problem with the license as well: Z3 is MIT,
so
>     >clang
>     >would have to be released with Z3's license.
> 
>     I don't think that's a problem. You are not releasing z3 with
clang.
>     This is an apt repo. 
> 
> 
> Well, I'm not an expert, but building clang linked with z3 and offering
> it online for people to download seems a lot like a release.
> 
> I don't it matters if it's a tar.gz or an apt repo.
> 
Ah, ok you're linking clang with libz3 or so? ...

Still... I am definitely not an expert in licensing but after a quick
lookup on Google, I would say that Apache2 and MIT would not cause a
problem. Anyway, don't quote me on that.

-- 
Paulo Matos

On Tue, 12 Feb 2019, 15:57 Paulo Matos <pmatos at linki.tools wrote:
>
>
> On 12/02/2019 19:49, Mikhail Ramalho wrote:
> >
> >
> > On Tue, 12 Feb 2019, 14:32 Paulo Matos <pmatos at linki.tools
wrote:
> >
> >
> >
> >     On 12 February 2019 18:59:21 CET, Mikhail Ramalho
> >     <mikhail.ramalho at gmail.com <mailto:mikhail.ramalho at
gmail.com>>
> wrote:
> >     >I _think_ there is a problem with the license as well: Z3 is
MIT, so
> >     >clang
> >     >would have to be released with Z3's license.
> >
> >     I don't think that's a problem. You are not releasing z3
with clang.
> >     This is an apt repo.
> >
> >
> > Well, I'm not an expert, but building clang linked with z3 and
offering
> > it online for people to download seems a lot like a release.
> >
> > I don't it matters if it's a tar.gz or an apt repo.
> >
>
> Ah, ok you're linking clang with libz3 or so? ...
>
> Still... I am definitely not an expert in licensing but after a quick
> lookup on Google, I would say that Apache2 and MIT would not cause a
> problem. Anyway, don't quote me on that.
>
AFAIK, the only requirement is to ship Z3's license along with the clang.

I heard that there are other projects under the llvm umbrella with the same
issue (linking against MIT/apache2 libraries) and that they're not released
with llvm because this requirement.

>
> --
> Paulo Matos
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20190212/0a3c371f/attachment.html>