[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