Re: [isabelle-dev] NEWS: activation of Z3 via z3_non_commercial system option
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
[isabelle-dev] NEWS: activation of Z3 via z3_non_commercial system option
* Activation of Z3 now works via z3_non_commercial system option (without requiring restart), instead of former settings variable Z3_NON_COMMERCIAL. The option can be edited in Isabelle/jEdit menu Plugin Options / Isabelle / General. This refers to Isabelle/0c07990363a3. For completeness, the included diff shows the update on the Isabelle component z3-3.2-1, which is relevant for Jasmin when he changes z3 again in the future. The change of z3_non_commercial was already planned for Isabelle2013-2, but did not make it into the release, because I could not make up my mind how much hand-holding the user should get. Right now it is the minimal possible approach to it, without any hand-holding apart from some prose text. I have taken the opportunity to experiment with Pretty.para here: traditionally we have short one-line output that is statically broken, but here the long text might look better with dynamic word-wrapping. The disadvantage is that such output is harder to search formally in log files etc. Makariusdiff -r z3-3.2/etc/settings z3-3.2-1/etc/settings 4,6c4 Z3_HOME=$Z3_COMPONENT/$ISABELLE_PLATFORM # Z3_NON_COMMERCIAL=yes --- Z3_HOME=$Z3_COMPONENT/$ISABELLE_PLATFORM32 Only in z3-3.2/etc: ._settings diff -r z3-3.2/README z3-3.2-1/README 16,19c16,17 Z3_NON_COMMERCIAL=yes in the environment or in $ISABELLE_HOME_USER/etc/settings. --- the Isabelle system option z3_non_commercial to yes (e.g. via the Isabelle/jEdit menu Plugin Options / Isabelle / General). Only in z3-3.2/x86-darwin: z3.dbg ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
