Re: [isabelle] distributed installation + sledgehammer file write permissions

Hi Jasmin,

Many thanks for this, very helpful. 

I had looked at the etc/settings file before, but not for Windows. I think the change to ISABELLE_TMP_PREFIX and ISABELLE_HOME_USER to a suitable directory for CS-support will suffice. Many thanks for pointing it out. 

the whole thing came about because locally they had a last-minute change from a ready Linux-setup to what a new-Windows environment panic! 
As I divorced myself from windows a while ago, was just in a helpless situation to advice support on what to do on short notice. 

Thanks again.

On 25 Sep 2014, at 10:20, Jasmin Christian Blanchette <jasmin.blanchette at> wrote:

> Hi Leo,
> Am 25.09.2014 um 10:50 schrieb Leo Freitas <leo.freitas at>:
>> 2) sledgehammer file write access:
>> This worked to a degree, but say, sledgehammer fails saying SysErr because of a file-write problem. Where is it SH is trying to write to?
> By default, Sledgehammer should be trying to write to
>    ML {* getenv "ISABELLE_TMP" *}
> a subdirectory that is created at startup and removed upon exit. Since this is used not only by Sledgehammer, but also by other Isabelle subsystems, I would recommend trying to find out what goes wrong there. I am not very familiar with Windows or Cygwin, but I presume the Isabelle's System manual ("isabelle doc system") would be a good starting point for investigations.
> As a workaround for Sledgehammer, It is possible to specify another directory by adding
>    declare [[sledgehammer_atp_dest_dir = "/foo/bar/baz"]]
> to the top of your theory file, or in an imported theory. If you already have a theory file with some basic setup for the students, this could go there.
> Regards,
> Jasmin

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.