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
