diff --git a/NN/API/Data/Sources.lean b/NN/API/Data/Sources.lean index 56533146..1322ab49 100644 --- a/NN/API/Data/Sources.lean +++ b/NN/API/Data/Sources.lean @@ -103,6 +103,25 @@ def Internal.tensorFromFlat else .error s!"{tag}: expected {dims.size} values for shape {dims}, got {values.size}" +/-- +Validate an unboxed flat payload's length before crossing into total tensor code. + +`Tensor.from` on a `FloatArray` wraps the buffer in place, so a payload the NPY loader +decoded unboxed becomes a tensor without a copy or a boxed intermediate. +-/ +def Internal.tensorFromFloatArray + (tag : String) (dims : Shape) (values : FloatArray) : + Except String (Tensor Float dims) := + -- The length is read through the storage instance, which is how the tensor states its shape. + if h : @TorchLean.Storage.size Float TorchLean.instFloatStorage values = dims.size then + .ok <| (Tensor.from values).reshape dims (by + show Spec.Shape.size [@TorchLean.Storage.size Float TorchLean.instFloatStorage values] + = dims.size + simpa [Spec.Shape.size] using h) + else + .error s!"{tag}: expected {dims.size} values for shape {dims}, got \ + {@TorchLean.Storage.size Float TorchLean.instFloatStorage values}" + namespace Internal /-- How a file's physical shape is matched against the requested tensor shape. -/ @@ -134,12 +153,12 @@ def Internal.readNpyTensor (path : System.FilePath) (dims : Shape) if data.shape.toList != dims.toList then pure (.error s!"npy: shape mismatch, expected {dims}, got {data.shape}") else - pure <| Internal.tensorFromFlat "npy" dims data.values + pure <| Internal.tensorFromFloatArray "npy" dims data.values | .leadingPrefix => let res ← readNpyPrefix path dims.toArray match res with | .error e => pure (.error e) - | .ok data => pure <| Internal.tensorFromFlat "npy" dims data.values + | .ok data => pure <| Internal.tensorFromFloatArray "npy" dims data.values /-- Parse a float-encoded class label as a `Nat` in `[0, classes)`. -/ private def finLabelOfFloat (tag : String) (classes : Nat) (x : Float) : diff --git a/NN/Data/IO/Npy.lean b/NN/Data/IO/Npy.lean index bbcaf097..c8349481 100644 --- a/NN/Data/IO/Npy.lean +++ b/NN/Data/IO/Npy.lean @@ -17,7 +17,8 @@ examples use: - NumPy format versions 1 and 2; - little-endian `float32` and `float64` payloads (` acc * n) 1 unless raw.size = count do throw <| formatError tag s!"shape requires {count} elements, got {raw.size}" - let values ← (Array.range count).mapM fun i => + let mut out := FloatArray.emptyWithCapacity count + for i in [0:count] do let idxF := idxFortranOfCIdx shape i - match raw[idxF]? with - | some value => pure value - | none => throw <| formatError tag <| + if idxF < raw.size then + out := out.push (raw[idxF]!) + else + throw <| formatError tag <| s!"Fortran-order index {idxF} is outside the {raw.size}-element payload" - pure values + pure out /-- Safe `ByteArray` indexing. -/ def byteAt? (bs : ByteArray) (i : Nat) : Option UInt8 := @@ -218,7 +255,7 @@ def npyElementBytes (tag descr : String) : Except String Nat := else .error (formatError tag s!"unsupported dtype: {descr}") -/-- Bound each dimension and the shape product before allocating a decoded `Array Float`. -/ +/-- Bound each dimension and the shape product before allocating a decoded payload. -/ def npyElementCount (tag : String) (shape : Array Nat) : Except String Nat := do let limit := (USize.size - 1) / 8 for dim in shape do @@ -246,18 +283,95 @@ def parseNpyHeaderMeta (tag : String) (bs : ByteArray) : Except String NpyHeader let elementCount ← npyElementCount tag shape return { dtype, fortran, shape, dataStart := headerEnd, elementBytes, elementCount } -/-- Read one supported numeric element from an NPY payload. -/ -def readNpyElement (tag descr : String) (bs : ByteArray) (off : Nat) : Except String Float := - if descr = " .ok (Float.ofBits (UInt64.ofNat w)) - | none => .error (formatError tag "invalid float64 data") - else if descr = " .ok (Float32.toFloat (Float32.ofBits (UInt32.ofNat w))) - | none => .error (formatError tag "invalid float32 data") +/-! +### Payload decoding + +`byteAt?` and `readLittleEndian` are the right shape at the file boundary, where a malformed +header has to be reported rather than guessed at. Inside a payload loop they are the wrong shape: +an `Option` per byte and an `Except` per element each cost a heap cell, so decoding an array that +way pays about ten allocations per element and runs an order of magnitude below the rate at which +the same loop can fill a `FloatArray`. + +The functions below decode a payload whose byte range and dtype the caller has already checked. +The dtype is matched once per file rather than once per element, the bytes are read without an +intermediate `Option`, and the result is unboxed. + +The decoders reinterpret stored bits, with the one exception the runtime imposes: `Float.ofBits` +and `Float32.ofBits` return the canonical quiet NaN for every NaN pattern, so a NaN decodes as a +NaN but without its sign or payload. Signed zeros, subnormals, infinities and every finite value +decode to exactly their stored bits. +-/ + +/-- Little-endian `UInt64` at byte offset `o`. Out-of-range bytes read as `0`; callers check +the payload length first, so that fallback is unreachable for accepted files. -/ +@[inline] def uint64LE (bs : ByteArray) (o : Nat) : UInt64 := + (bs.get! o).toUInt64 + ||| ((bs.get! (o + 1)).toUInt64 <<< 8) + ||| ((bs.get! (o + 2)).toUInt64 <<< 16) + ||| ((bs.get! (o + 3)).toUInt64 <<< 24) + ||| ((bs.get! (o + 4)).toUInt64 <<< 32) + ||| ((bs.get! (o + 5)).toUInt64 <<< 40) + ||| ((bs.get! (o + 6)).toUInt64 <<< 48) + ||| ((bs.get! (o + 7)).toUInt64 <<< 56) + +/-- Little-endian `UInt32` at byte offset `o`, with the same precondition as `uint64LE`. -/ +@[inline] def uint32LE (bs : ByteArray) (o : Nat) : UInt32 := + (bs.get! o).toUInt32 + ||| ((bs.get! (o + 1)).toUInt32 <<< 8) + ||| ((bs.get! (o + 2)).toUInt32 <<< 16) + ||| ((bs.get! (o + 3)).toUInt32 <<< 24) + +/-- Decode the half-open element range `[lo, hi)` of a ` 1 + | .tasks n => n + | .auto => (System.Platform.Internal.getHardwareConcurrency ()).toNat + max 1 (min (min (max 1 requested) nBlocks) (totalElements / minElementsPerTask)) /-- Validate a C-order leading prefix and retain only its requested shape and element count. -/ def npyPrefixHeader (tag : String) (hdr : NpyHeader) (expectedShape : Array Nat) : @@ -281,18 +395,75 @@ def npyPrefixHeader (tag : String) (hdr : NpyHeader) (expectedShape : Array Nat) | _, _ => throw <| formatError tag s!"shape mismatch: expected {expectedShape}, got {hdr.shape}" +/-- +Validate that a header describes C-order leading-axis blocks, returning the block count and the +element count per block. + +Fortran-order and scalar arrays are rejected here, before any payload is read: a Fortran-order +file interleaves every leading-axis block across the payload, so neither the contiguity nor the +independence of the blocks holds, and a scalar has no leading axis to cut along. +-/ +def npyBlocksLayout (tag : String) (hdr : NpyHeader) : Except String (Nat × Nat) := do + if hdr.fortran then + throw <| formatError tag "leading-axis block loading requires C-order NPY arrays" + match hdr.shape[0]? with + | some d0 => + let tail := hdr.shape.extract 1 hdr.shape.size + return (d0, tail.foldl (fun acc n => acc * n) 1) + | none => + throw <| formatError tag + "leading-axis block loading requires a leading axis; scalar arrays have none" + /-- Decode a validated full or prefix payload, checking its byte range before reserving values. -/ def decodeNpyPayload (tag : String) (hdr : NpyHeader) (bs : ByteArray) : Except String NpyData := do if hdr.dataStart + hdr.elementCount * hdr.elementBytes > bs.size then throw <| formatError tag "NPY data truncated" - let mut raw : Array Float := Array.mkEmpty hdr.elementCount - for i in [0:hdr.elementCount] do - let value ← readNpyElement tag hdr.dtype bs (hdr.dataStart + i * hdr.elementBytes) - raw := raw.push value + let decode ← rangeDecoder tag hdr.dtype bs hdr.dataStart + let raw := decode 0 hdr.elementCount let values ← if hdr.fortran then reorderFortranToC tag hdr.shape raw else pure raw return { dtype := hdr.dtype, shape := hdr.shape, fortran := false, values } +/-- +Decode a validated C-order payload as one block per leading-axis index, checking its byte range +before reserving values. + +For a C-order array of shape `(d₀, d₁, …, dₖ)` each leading-axis block is physically contiguous, +so the `d₀` blocks are independent and therefore support either sequential or concurrent decoding. +`parallelism` chooses how many tasks that uses; see `resolveTaskCount` for the bounds that apply +to the request. `d₀` is a ceiling on it, so a file with a small leading axis is decoded with at +most that many tasks however many cores are free. +-/ +def decodeNpyBlocks (tag : String) (hdr : NpyHeader) (bs : ByteArray) + (parallelism : Parallelism) : Except String NpyBlocks := do + let (d0, blockSize) ← npyBlocksLayout tag hdr + if hdr.dataStart + hdr.elementCount * hdr.elementBytes > bs.size then + throw <| formatError tag "NPY data truncated" + let decode ← rangeDecoder tag hdr.dtype bs hdr.dataStart + let block : Nat → FloatArray := fun b => decode (b * blockSize) ((b + 1) * blockSize) + let nTasks := resolveTaskCount parallelism d0 hdr.elementCount + let blocks := + if nTasks ≤ 1 then + (Array.range d0).map block + else + -- Blocks are grouped, not handed out one per task: the task count follows the machine and + -- the block count follows the file, and those are independent. + -- + -- `Task.spawn` takes the work as a `Unit → α` closure, which is what keeps the decode + -- inside the task body. Handing a pure expression to an `IO`-level spawn instead lets it + -- be floated out onto the spawning thread, and the fan-out then runs sequentially at + -- exactly the single-threaded rate. + let perTask := (d0 + nTasks - 1) / nTasks + let groups : Array (Task (Array FloatArray)) := + (Array.range nTasks).map fun t => + let lo := t * perTask + let hi := min d0 (lo + perTask) + Task.spawn (fun _ => (Array.range (hi - lo)).map (fun k => block (lo + k))) + -- Regrouping moves one pointer per block, not one double per element, so it carries none + -- of the cost that joining decoded payloads would. + groups.foldl (fun acc g => acc ++ g.get) (Array.emptyWithCapacity d0) + return { dtype := hdr.dtype, shape := hdr.shape, blocks } + /-- Read exactly the requested bytes using bounded allocations, rejecting an early end of file. @@ -349,7 +520,7 @@ This supports large exported tensors kept on disk while a run uses only the firs and trailing dimensions must match exactly; only the leading axis may be larger than requested. The implementation shares header and dtype parsing with `parseNpy`, then decodes only the requested -prefix. This avoids building a full `Array Float` when a command asks for a small leading slice of a +prefix. This avoids building a full payload when a command asks for a small leading slice of a real image or sequence dataset. Only the requested range must be present; unused trailing rows are not checked for truncation. @@ -365,6 +536,27 @@ def parseNpyPrefix let selected ← npyPrefixHeader tag hdr expectedShape decodeNpyPayload tag selected bs +/-- +Parse a C-order `.npy` file into one `FloatArray` per index along the leading axis. + +Use this when the consumer wants the blocks apart anyway: one channel, one band, one batch +element at a time. The blocks are decoded concurrently under the bounds `resolveTaskCount` +describes, and the result does not depend on the task count. + +Use `parseNpy` when the consumer wants a single flat payload instead. That path decodes on +one thread by design. Decoding it concurrently would mean filling several separate arrays +and then copying all of them into one contiguous result, and that final copy walks every +element a second time: it costs several times the concurrent decode it was supposed to +speed up, and it holds the pieces and the result in memory simultaneously. Splitting the +work is only worth it when the pieces are what the caller wanted. + +Fortran-order and scalar arrays are rejected, as `npyBlocksLayout` explains. +-/ +def parseNpyBlocks (tag : String) (bs : ByteArray) + (parallelism : Parallelism := .auto) : Except String NpyBlocks := do + let hdr ← parseNpyHeaderMeta tag bs + decodeNpyBlocks tag hdr bs parallelism + /-- Read validated metadata without reading the payload. @@ -394,6 +586,21 @@ def readNpyPrefix let selected ← npyPrefixHeader "npy" hdr expectedShape ExceptT.mk (readNpyPayload handle selected) +/-- +Read a C-order `.npy` file as one `FloatArray` per index along the leading axis. + +The header is validated for block loading before the payload is read, so a Fortran-order or scalar +file is rejected without reading its payload. The payload itself is read with the same bounded +chunks as `readNpy`, and truncation is rejected. +-/ +def readNpyBlocks (path : System.FilePath) + (parallelism : Parallelism := .auto) : IO (Except String NpyBlocks) := do + _root_.IO.FS.withFile path .read fun handle => ExceptT.run do + let hdr ← ExceptT.mk (readNpyHeaderFromHandle handle) + let _ ← npyBlocksLayout "npy" hdr + let bytes ← ExceptT.mk (readNpyBytes handle (hdr.elementCount * hdr.elementBytes)) + return ← decodeNpyBlocks "npy" { hdr with dataStart := 0 } bytes parallelism + end IO end Data end TorchLean diff --git a/NN/Tests/Data/IO/Npy.lean b/NN/Tests/Data/IO/Npy.lean new file mode 100644 index 00000000..d799616f --- /dev/null +++ b/NN/Tests/Data/IO/Npy.lean @@ -0,0 +1,392 @@ +/- +Copyright (c) 2026 TorchLean +Released under MIT license as described in the file LICENSE. +Authors: TorchLean Team +-/ + +module + +public import NN.Data.IO.Npy + +/-! +# NPY loader tests + +Regression checks for the `.npy` payload decoders. The files are synthesised in memory, so the +expected values are known exactly; the file-backed readers are exercised on the same bytes written +to a scratch fixture. + +Two properties carry the weight here: + +- every decode path agrees bit for bit, not approximately. The decoders reinterpret stored bits + rather than computing, so equality is the honest test and a tolerance would hide exactly the + transcription bugs this is meant to catch; +- the values `==` on `Float` cannot see are checked from their bit patterns: both signed zeros, + both infinities and the extremes of either format exactly, and NaNs as the canonical NaN that + Lean's `Float.ofBits` makes of every NaN pattern, sign and payload included; +- the concurrent leading-axis path agrees with the sequential one, and agrees with itself across + repeated runs. Blocks are decoded on separate tasks and reassembled by index, so a + scheduling-order dependence would show up as a block permutation. +-/ + +@[expose] public section + +namespace NN.Tests.Data.IO.Npy + +open TorchLean.Data.IO +open TorchLean.Data.IO.Internal + +def expect (tag : String) (ok : Bool) : IO Unit := do + unless ok do + throw <| IO.userError s!"npy loader check failed: {tag}" + +/-! ## Synthetic `.npy` construction -/ + +/-- Append a little-endian `UInt64`. -/ +def pushU64LE (ba : ByteArray) (w : UInt64) : ByteArray := Id.run do + let mut out := ba + for k in [0:8] do + out := out.push (UInt8.ofNat ((w >>> (UInt64.ofNat (8 * k))) &&& 0xff).toNat) + pure out + +/-- Append a little-endian `UInt32`. -/ +def pushU32LE (ba : ByteArray) (w : UInt32) : ByteArray := Id.run do + let mut out := ba + for k in [0:4] do + out := out.push (UInt8.ofNat ((w >>> (UInt32.ofNat (8 * k))) &&& 0xff).toNat) + pure out + +/-- Build a version-1 `.npy` header block, padded to the 64-byte alignment NumPy uses. -/ +def header (descr : String) (shape : List Nat) (fortran : Bool) : ByteArray := Id.run do + let dims := + match shape with + | [] => "()" + | [d] => s!"({d},)" + | _ => "(" ++ String.intercalate ", " (shape.map toString) ++ ")" + let order := if fortran then "True" else "False" + let dict := s!"\{'descr': '{descr}', 'fortran_order': {order}, 'shape': {dims}, }" + -- magic (6) + version (2) + length (2) + dict + '\n', padded to a multiple of 64 + let unpadded := 10 + dict.length + 1 + let pad := (64 - unpadded % 64) % 64 + let body := dict ++ String.ofList (List.replicate pad ' ') ++ "\n" + let mut ba := ByteArray.empty + ba := ba.push 0x93 + for c in "NUMPY".toList do ba := ba.push (UInt8.ofNat c.toNat) + ba := ba.push 1 + ba := ba.push 0 + ba := ba.push (UInt8.ofNat (body.length % 256)) + ba := ba.push (UInt8.ofNat (body.length / 256)) + for c in body.toList do ba := ba.push (UInt8.ofNat c.toNat) + pure ba + +/-- A deterministic value for element `i`, spread across exponents so the byte pattern of +each element differs in every byte. -/ +def sample (i : Nat) : Float := + let x := Float.ofNat (i % 9973) + 0.5 + x * Float.exp (Float.ofNat (i % 17) - 8.0) - 3.25 + +/-- A ` acc * n) 1 + let mut ba := header " acc * n) 1 + let mut ba := header " pure a + | .error e => throw <| IO.userError s!"npy loader check failed: {tag}: {e}" + +def isError {α : Type} : Except String α → Bool + | .ok _ => false + | .error _ => true + +/-- Flatten decoded blocks back into one payload, for comparison against `parseNpy`. -/ +def concatBlocks (blocks : Array FloatArray) : FloatArray := Id.run do + let total := blocks.foldl (fun acc b => acc + b.size) 0 + let mut out := FloatArray.emptyWithCapacity total + for b in blocks do + for i in [0:b.size] do + out := out.push (b[i]!) + pure out + +/-! ## Tests -/ + +/-- Every element survives the round trip exactly, for both supported dtypes. -/ +def testRoundTrip : IO Unit := do + let shape := [3, 5, 7] + let count := 105 + let d8 ← ofExcept "f8 parse" (parseNpy "t" (buildF8 shape)) + expect "f8 dtype" (d8.dtype == ">> 63 == 1 + +/-- The canonical quiet NaN: what Lean's `Float.ofBits` returns for every NaN bit pattern. -/ +def canonicalNaN : UInt64 := 0x7ff8000000000000 + +/-- Whether entry `i` of `specialF8` and `specialF4` is a NaN pattern. -/ +def isNaNPattern (i : Nat) : Bool := 4 ≤ i && i < 8 + +/-- The patterns `==` on `Float` cannot see survive every decode path, with one exception the +runtime imposes: a NaN's sign and payload. `Float.ofBits` and `Float32.ofBits` return the +canonical quiet NaN for every NaN pattern, so no decoder over `Float` can keep those bits; what +the decoders preserve, and what is checked here, is that a NaN decodes as a NaN. The canonical +result is pinned so that a change in the runtime shows up here rather than downstream. + +For ` 3.4028e38 && v[8]! < 3.40283e38) + expect "f4 negative largest finite" ((v[9]!).isFinite && v[9]! < -3.4028e38) + expect "f4 smallest subnormal" (v[10]! > 0.0 && v[10]! < 1.5e-45) + expect "f4 negative smallest subnormal" (v[11]! < 0.0 && v[11]! > -1.5e-45) + +/-- The leading-axis blocks are exactly the payload, cut at the leading-axis stride. -/ +def testBlocksMatchFlat (shape : List Nat) (tag : String) : IO Unit := do + let bs := buildF8 shape + let flat ← ofExcept s!"{tag} flat" (parseNpy "t" bs) + let blk ← ofExcept s!"{tag} blocks" (parseNpyBlocks "t" bs) + let d0 := shape.headD 0 + let blockSize := (shape.drop 1).foldl (fun acc n => acc * n) 1 + expect s!"{tag} block count" (blk.blocks.size == d0) + expect s!"{tag} block sizes" (blk.blocks.all (fun b => b.size == blockSize)) + expect s!"{tag} blocks = flat" (faBitsEq (concatBlocks blk.blocks) flat.values) + +/-- Every task count decodes the same payload, bit for bit. + +This is the property that makes the task count a free choice: it may be tuned for a machine +without changing what the loader returns. A block permutation, an off-by-one in the block +grouping, or a torn write would all break it. The sweep deliberately includes counts above +the block count and above the core count, which `resolveTaskCount` clamps. -/ +def testParallelismAgrees : IO Unit := do + -- large enough that `resolveTaskCount` is not clamped to 1 by `minElementsPerTask` + let shape := [8, 137, 131] + let count := shape.foldl (fun acc n => acc * n) 1 + expect "test payload exceeds the sequential threshold" (count / minElementsPerTask >= 2) + let bs := buildF8 shape + let flat ← ofExcept "parallel flat" (parseNpy "t" bs) + let seq ← ofExcept "sequential blocks" (parseNpyBlocks "t" bs .sequential) + expect "sequential = flat" (faBitsEq (concatBlocks seq.blocks) flat.values) + for n in [1, 2, 3, 4, 5, 7, 8, 9, 16, 64] do + let got ← ofExcept s!"tasks {n}" (parseNpyBlocks "t" bs (.tasks n)) + expect s!"tasks {n} block count" (got.blocks.size == seq.blocks.size) + for b in [0:seq.blocks.size] do + expect s!"tasks {n} block {b}" (faBitsEq (got.blocks[b]!) (seq.blocks[b]!)) + let auto ← ofExcept "auto" (parseNpyBlocks "t" bs .auto) + expect "auto block count" (auto.blocks.size == seq.blocks.size) + for b in [0:seq.blocks.size] do + expect s!"auto block {b}" (faBitsEq (auto.blocks[b]!) (seq.blocks[b]!)) + +/-- Repeated concurrent decodes of one payload agree, so the result does not depend on the +order in which tasks happen to finish. -/ +def testConcurrentDeterminism : IO Unit := do + let shape := [8, 137, 131] + let bs := buildF8 shape + let first ← ofExcept "concurrent first" (parseNpyBlocks "t" bs .auto) + for r in [0:8] do + let again ← ofExcept s!"concurrent repeat {r}" (parseNpyBlocks "t" bs .auto) + expect s!"concurrent repeat {r} block count" (again.blocks.size == first.blocks.size) + for b in [0:first.blocks.size] do + expect s!"concurrent repeat {r} block {b}" + (faBitsEq (again.blocks[b]!) (first.blocks[b]!)) + +/-- The task count respects its three bounds: the request, the block count, and the payload +size. In particular a small payload stays on the calling thread whatever is requested. -/ +def testTaskCountBounds : IO Unit := do + let big := 1 <<< 20 + expect "sequential is one task" (resolveTaskCount .sequential 64 big == 1) + expect "never more tasks than blocks" (resolveTaskCount (.tasks 64) 8 big == 8) + expect "honours a request below the block count" (resolveTaskCount (.tasks 4) 64 big == 4) + expect "small payload stays on one thread" (resolveTaskCount (.tasks 64) 64 1024 == 1) + expect "task count is at least one" (resolveTaskCount (.tasks 0) 64 big == 1) + expect "auto is bounded by the block count" (resolveTaskCount .auto 2 big <= 2) + +/-- Fortran-order payloads are still reordered into C order by `parseNpy`. -/ +def testFortranOrder : IO Unit := do + let shape := [2, 3] + -- Fortran storage of [[a b c], [d e f]] is a d b e c f + let cOrder : Array Float := #[1.0, 2.0, 3.0, 4.0, 5.0, 6.0] + let mut ba := header " expect "file rejects fortran order for blocks" false + | .error message => + expect "fortran rejection names the storage order" ((message.splitOn "C-order").length > 1) + IO.FS.writeBinFile path (header " expect "file rejects scalar shape for blocks" false + | .error message => + expect "scalar rejection names the leading axis" + ((message.splitOn "leading axis").length > 1) + +def run : IO Unit := do + IO.println "-- npy loader --" + let fixtureDirectory : System.FilePath := ".lake/build/tmp" + IO.FS.createDirAll fixtureDirectory + testRoundTrip + testSpecialValues fixtureDirectory + testBlocksMatchFlat [4, 6] "2d" + testBlocksMatchFlat [3, 5, 7] "3d" + testBlocksMatchFlat [5] "1d" + testBlocksMatchFlat [3, 0] "empty blocks" + testBlocksMatchFlat [0, 3] "no blocks" + testParallelismAgrees + testConcurrentDeterminism + testTaskCountBounds + testFortranOrder + testRejections + testFileReaders fixtureDirectory + IO.println "npy loader: ok" + +end NN.Tests.Data.IO.Npy diff --git a/NN/Tests/Suite.lean b/NN/Tests/Suite.lean index 77bed1ef..f32c67c1 100644 --- a/NN/Tests/Suite.lean +++ b/NN/Tests/Suite.lean @@ -7,6 +7,7 @@ Authors: TorchLean Team module public import NN.Tests.Backend.Profile +public import NN.Tests.Data.IO.Npy public import NN.Tests.IR.ShapeContracts public import NN.Tests.Verification.Crown public import NN.Tests.Verification.CameraCertificates @@ -64,6 +65,7 @@ def run : IO Unit := do | none => IO.println "== TorchLean: curated tests ==" NN.Tests.Backend.Profile.run + NN.Tests.Data.IO.Npy.run NN.Tests.Verification.Crown.run NN.Tests.Verification.CameraCertificates.run NN.Tests.Verification.CertificateParsing.run