It is my fault: Holmake generates lots of these and is not deleting them after
using them.
I'll fix that forthwith!
Thanks for the issue report,
Michael
On 14/11/18, 02:42, "polyml on behalf of James Clarke"
<polyml-boun...@inf.ed.ac.uk on behalf of jrt...@jrtc27.com> wrote:
On 13 Nov 2018, at 15:24, Gergely Buday <buday.gerg...@uni-eszterhazy.hu>
wrote:
>
> Hi there,
>
> running a CakeML bootstrapping process I got an error
>
> no space left on device
>
> Actually, the disk was not full but consumed all possible inodes:
>
> $ sudo df -i /
> [sudo] password for gbuday:
> Filesystem Inodes IUsed IFree IUse% Mounted on
> /dev/sda1 512064 512064 0 100% /
>
> That was because of 361391 MLTEMPXXXX files in /tmp.
>
> Is that a Poly/ML thing?
MLTEMPXXXX is the pattern used by Poly/ML for its temporary files when you
call
OS.FileSys.tmpName: unit -> string. However, Poly/ML itself is not calling
it
itself, nor is CakeML; it looks like HOL makes a lot of calls, so I would
guess
that Holmake is at fault (if that's the step where you run out of space).
James
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
