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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
