From 7b1bdbab062142c5f8c807d85f97d58854fa7a80 Mon Sep 17 00:00:00 2001 From: Nirmal Thomas Date: Tue, 24 Feb 2026 00:28:32 +0000 Subject: [PATCH] Make uniqueName deterministic for shared constants Replace non-deterministic IO.rand suffix generation with a deterministic approach: count existing matching files in the directory and seed a StdGen RNG with that count. This ensures repeated compilations produce the same filenames for shared constants with duplicate base names. Also removes `partial` since the function is no longer recursive. --- KLR/Compile.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/KLR/Compile.lean b/KLR/Compile.lean index 311ef673..4ca83113 100644 --- a/KLR/Compile.lean +++ b/KLR/Compile.lean @@ -30,11 +30,15 @@ open Pass (CompileResult) private partial def uniqueName (dst : String) (base : String) : IO String := do let fName := s!"{dst}/{base}.npy" - if ← FilePath.pathExists (FilePath.mk fName) then - let suffix ← IO.rand 0 (2^64 - 1) - uniqueName dst s!"{base}_{suffix}" - else + if !(← FilePath.pathExists (FilePath.mk fName)) then return base + let entries ← System.FilePath.readDir (FilePath.mk dst) + let count := entries.filter (fun e => + e.fileName.startsWith s!"{base}_" && e.fileName.endsWith ".npy") |>.size + let gen := mkStdGen count + let (suffix, _) := RandomGen.next gen + let suffix := suffix % (2^64) + uniqueName dst s!"{base}_{suffix}" private def sharedConstant (outfolder : String)