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. 

PS:
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.

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

> Hi Leo,
> 
> Am 25.09.2014 um 10:50 schrieb Leo Freitas <leo.freitas at newcastle.ac.uk>:
> 
>> 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.