[isabelle-dev] LWP::Simple
Lawrence Paulson
lp15 at cam.ac.uk
Tue Oct 21 13:06:32 CEST 2014
I did not update my machine, but I did delete a lot of big tarballs in order to save disk space. Maybe that broke something.
Mac users may be interested to know that I upgraded to Yosemite on my laptop, but the development version of Isabelle still seems to work fine.
Larry
On 21 Oct 2014, at 08:57, Makarius <makarius at sketis.net> wrote:
> On Mon, 20 Oct 2014, Lawrence Paulson wrote:
>
>> I recently tried to launch the Isabelle development version, but got error messages indicating (in a fairly obscure way) the need to install the Perl module LWP::Simple. Something new here?
>
> Maybe an update of Mac OS X or MacPorts.
>
> The default perl in the PATH needs to provide LWP::Simple, e.g. for "isabelle components" or remote Sledgehammer.
>
> This is one of the rare situations where we still have the IKEA principle: users need to make sure that they have a proper perl installation.
>
>
> Makarius
>
> ----------------------------------------------------------------------------
> http://stop-ttip.org
> ----------------------------------------------------------------------------
More information about the isabelle-dev
mailing list