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-bounces at inf.ed.ac.uk on behalf of jrtc27 at jrtc27.com> wrote:

On 13 Nov 2018, at 15:24, Gergely Buday <buday.gergely at 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 at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml