Thanks for the bug report! I’m about to push a commit that should fix this
issue and keep /tmp clear.
Best wishes,
Michael
From: Gergely Buday <buday.gerg...@uni-eszterhazy.hu>
Date: Wednesday, 14 November 2018 at 12:34
To: "hol-info@lists.sourceforge.net" <hol-info@lists.sourceforge.net>
Subject: [Hol-info] excessive number of MLTEMP files
Hi there,
coming from the Poly/ML list.
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.
James Clarke said on the Poly/ML list that
> 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).
Can I tweak Holmake not to create that much temporary files or to periodically
delete unnecessary ones?
Or, might it be that CakeML bootstrapping does require that much temporary
files?
- Gergely
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
