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



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





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