[isabelle-dev] NEWS: activation of Z3 via "z3_non_commercial" system option

[Makarius]

On Mon, 13 Jan 2014, Lawrence Paulson wrote:

> I get an error here:
>
> ~/isabelle/Repos/src/HOL: isabelle components -a
> ### Missing Isabelle component: "/Users/lp15/.isabelle/contrib/z3-3.2-1"
> Getting "http://isabelle.in.tum.de/components/z3-3.2-1.tar.gz"
> Can't locate LWP/Simple.pm in @INC (@INC contains: /opt/local/lib/perl5/site_perl/5.12.4/darwin-thread-multi-2level /opt/local/lib/perl5/site_perl/5.12.4 /opt/local/lib/perl5/vendor_perl/5.12.4/darwin-thread-multi-2level /opt/local/lib/perl5/vendor_perl/5.12.4 /opt/local/lib/perl5/5.12.4/darwin-thread-multi-2level /opt/local/lib/perl5/5.12.4 /opt/local/lib/perl5/site_perl /opt/local/lib/perl5/vendor_perl .).
> BEGIN failed--compilation aborted.
> ~/isabelle/Repos/src/HOL:

The regular /usr/bin/perl by Apple already provides the critial libwww, 
which is required here (as well as for remote Sledgehammer scripts).

Perl from /opt/local probably comes in via MacPorts, and thus introduces 
the usual uncertainties of such package repositories.  If you want to keep 
that version of perl, you need to saturate its installation.  Via "sudo 
port list", I guess that something like p5-libwww-perl should do it.

Are you actually using the Isabelle.app wrapper from Isabelle2013-2?  It 
retains the original Apple PATH, and thus uses /usr/bin/perl even with 
that MacPorts Perl present.  That might explain, why remote sledgehammer 
works, but "isabelle components -a" with its different PATH didn't.


 	Makarius