Unable to write to a file with an offset

Description

I need to be able to write to any part of a file with multiple coroutines in parallel.

AI hallucinated IO.FS.Handle.seek, which would definitely solve the problem if it existed.

Context

I recently wrote an XorEncrypt project in 3 languages:

• Go 1.25.7
• Lean 4.28.0
• Python 3.13.12

2 had the required function:

• Go: func (f *File) WriteAt(b []byte, off int64) (n int, err error)
• Python: def os.pwrite(fd: int, str: bytes, offset: int, /) -> int

All 3 implementations used 1 worker coroutine per available logical CPU core.
Go and Python workers read, calculated, and wrote in parallel. Lean used only pipeline concurrency for its workers: 1 reading coroutine sequentially read to create jobs; those jobs were passed to workers for calculation; 1 writer coroutine sequentially wrote the results.

A recent benchmark with 931 MiB files:
Go : 1760421648 B/s
Lean4 : 1025278972 B/s
Python: 216356205 B/s

Steps to Reproduce

1. Read 21.5. Files, File Handles, and Streams, find no corresponding method exists.
2. Ask multiple AI, all of which hallucinate or say it is impossible.
3. File this bug report if it does not exist; else, 👍🏻 this bug report.

Expected behavior: Lean 4 is the fastest! 🎉

Actual behavior: [Lean 4]'s speed ≤ 0.58241 × Go's speed.

Versions

~/Git/XorEncrypt via 🐹 v1.25.7 via 🐍 v3.13.12 
❯ kinfo
Operating System: NixOS 26.05
KDE Plasma Version: 6.6.2
KDE Frameworks Version: 6.24.0
Qt Version: 6.10.2
Kernel Version: 6.19.6 (64-bit)
Graphics Platform: Wayland
Processors: 20 × 12th Gen Intel® Core™ i9-12900HK
Memory: 64 GiB of RAM (62.5 GiB usable)
Graphics Processor 1: Intel® Iris® Xe Graphics
Graphics Processor 2: NVIDIA GeForce RTX 3050 Ti Laptop GPU

~/Git/XorEncrypt via 🐹 v1.25.7 via 🐍 v3.13.12 
❯ lean --version && lake --version
Lean (version 4.28.0, commit v4.28.0, Release)
Lake version 5.0.0-src+v4.28.0 (Lean version 4.28.0)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the referenced “21.5. Files, File Handles, and Streams” documentation and inspect the existing IO file-handle APIs, especially the absence of IO.FS.Handle.seek. Compare the requested capability with the linked Go WriteAt and Python pwrite behavior. Done means the project has a supported way to write at arbitrary file offsets from concurrent workers, with its API and concurrency behavior documented.