lakefile.lean

import Lake
open System Lake DSL

/-- Link-time-optimization flags for the shipped library (issue #2806).

    `-flto` lets the final link inline the project-local stopgap externs
    (`c/bytearray_wide_ffi.c`, `c/extend_within_ffi.c`, `c/copy_within_ffi.c`)
    into the hot matcher/decoder loops instead of leaving per-iteration
    cross-object calls — a measured +2–5% end-to-end compress win with
    byte-identical output (LTO is codegen-only). For the bitcode to merge,
    every object must come from the same compiler: the Lean-emitted C
    already compiles with the toolchain's C compiler, and the FFI targets
    below use `buildLeanO` (that same compiler — bundled clang, or
    `LEAN_CC` if set, which must then itself support LTO) instead of the
    system `cc`. `-fno-semantic-interposition` keeps `-fPIC` codegen from
    pessimizing cross-object references. Linux-only: macOS links with the
    system ld64, whose libLTO need not accept the toolchain clang's
    bitcode, and Windows is untested.

    Downstream `require lean-zip` consumers need no flags of their own:
    Lake archives the bitcode with the toolchain `llvm-ar`, and the
    toolchain lld consumes bitcode archive members natively (verified with
    a flag-free downstream package — its executable gets the same
    inlining). Set `LEAN_ZIP_LTO=0` to opt out (e.g. when linking the
    static libs outside Lake with a non-LTO-aware linker, or with a custom
    `LEAN_AR` that cannot index bitcode). Lake caches `run_io` config:
    after toggling the env var, reconfigure with `lake -R build` (or
    remove `.lake`). -/
def ltoFlags : IO (Array String) := do
  if Platform.isWindows || Platform.isOSX then return #[]
  if (← IO.getEnv "LEAN_ZIP_LTO") == some "0" then return #[]
  return #["-flto", "-fno-semantic-interposition"]

/-- Link-side LTO flags: `-flto` marks the link as LTO, `-O3` runs the
    link-time codegen pipeline at the same level as the per-module compiles
    (lld's default is `--lto-O2`). Empty whenever `ltoFlags` is. -/
def ltoLinkFlags : IO (Array String) := do
  let flags ← ltoFlags
  if flags.isEmpty then return #[] else return flags ++ #["-O3"]

/-! The shipped package is the verified library plus the project-local
    stopgap primitives `libcopy_within_ffi` (lean#14158),
    `libextend_within_ffi` (overlapping-match copy),
    `libbytearray_wide_ffi` (lean#14053), and `libinflate_fast_ffi`
    (write-once cursor primitives, issue #2799). Each has a pure-Lean
    reference body and a correspondence proof; no external C library is
    required. The native↔zlib conformance suite lives in the dev-only
    `conformance/` sub-package, so a downstream `require lean-zip` never
    needs system zlib. -/
package «lean-zip» where
  moreLeancArgs := run_io ltoFlags
  moreLinkArgs := run_io ltoLinkFlags
  testDriver := "test"

require zipCommon from git "https://github.com/kim-em/lean-zip-common" @ "4425bab1f9522307d77e8d485bc536149ba31c36"

lean_lib Zip

-- ByteArray.copyWithin primitive (project-local stopgap for lean#14158);
-- no external library, always compiled.
input_file copy_within_ffi.c where
  path := "c" / "copy_within_ffi.c"
  text := true

target copy_within_ffi.o pkg : FilePath := do
  let srcJob ← copy_within_ffi.c.fetch
  let oFile := pkg.buildDir / "c" / "copy_within_ffi.o"
  -- -O2/-DNDEBUG for the same reason as bytearray_wide_ffi (and because a
  -- clang -O0 object carries `optnone`, which would block the LTO inlining).
  -- `buildLeanO` compiles with the toolchain clang so the -flto bitcode
  -- matches the Lean-emitted objects' LLVM version (see `ltoFlags`).
  let hardArgs := #["-O2", "-DNDEBUG"] ++ (← ltoFlags) ++
    if Platform.isWindows then #[] else #["-fPIC"]
  buildLeanO oFile srcJob #[] hardArgs

extern_lib libcopy_within_ffi pkg := do
  let ffiO ← copy_within_ffi.o.fetch
  let name := nameToStaticLib "copy_within_ffi"
  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

-- ByteArray.extendWithin primitive (allocation-free overlapping-match copy);
-- no external library, always compiled.
input_file extend_within_ffi.c where
  path := "c" / "extend_within_ffi.c"
  text := true

target extend_within_ffi.o pkg : FilePath := do
  let srcJob ← extend_within_ffi.c.fetch
  let oFile := pkg.buildDir / "c" / "extend_within_ffi.o"
  -- -O2/-DNDEBUG for the same reason as bytearray_wide_ffi: this is a hot fill
  -- loop whose lean.h helpers only inline away under optimization, and its
  -- bounds are carried by the Lean-side reference body (+ conformance sweeps).
  -- `buildLeanO` + `ltoFlags`: see `copy_within_ffi.o`.
  let hardArgs := #["-O2", "-DNDEBUG"] ++ (← ltoFlags) ++
    if Platform.isWindows then #[] else #["-fPIC"]
  buildLeanO oFile srcJob #[] hardArgs

extern_lib libextend_within_ffi pkg := do
  let ffiO ← extend_within_ffi.o.fetch
  let name := nameToStaticLib "extend_within_ffi"
  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

-- Word-sized little-endian ByteArray readers (project-local stopgap for
-- lean#14053); no external library, always compiled.
input_file bytearray_wide_ffi.c where
  path := "c" / "bytearray_wide_ffi.c"
  text := true

target bytearray_wide_ffi.o pkg : FilePath := do
  let srcJob ← bytearray_wide_ffi.c.fetch
  let oFile := pkg.buildDir / "c" / "bytearray_wide_ffi.o"
  -- -O2 is essential here: these are single-load/store hot-loop primitives
  -- whose lean.h helpers (lean_sarray_cptr, lean_is_exclusive, ...) only
  -- disappear under optimization; without it each "wide" op is a pile of
  -- outlined helper calls and loses to the runtime's own -O2 push/get.
  -- -DNDEBUG matches how the release Lean runtime itself is built: the
  -- lean.h asserts are debug-only checks, and these externs' bounds are
  -- carried by Lean-side proofs (+ the ZipTest/Wide conformance sweeps).
  -- `buildLeanO` + `ltoFlags`: see `copy_within_ffi.o` — with LTO these
  -- single-instruction externs inline into `countMatch`/`hash3` themselves.
  let hardArgs := #["-O2", "-DNDEBUG"] ++ (← ltoFlags) ++
    if Platform.isWindows then #[] else #["-fPIC"]
  buildLeanO oFile srcJob #[] hardArgs

extern_lib libbytearray_wide_ffi pkg := do
  let ffiO ← bytearray_wide_ffi.o.fetch
  let name := nameToStaticLib "bytearray_wide_ffi"
  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

-- Write-once cursor primitives for the fastloop decoder (issue #2799):
-- presize (zero-filled buffer) + copy_within_at (in-place LZ77 copy at a
-- cursor). No external library, always compiled.
input_file inflate_fast_ffi.c where
  path := "c" / "inflate_fast_ffi.c"
  text := true

target inflate_fast_ffi.o pkg : FilePath := do
  let srcJob ← inflate_fast_ffi.c.fetch
  let oFile := pkg.buildDir / "c" / "inflate_fast_ffi.o"
  -- -O2/-DNDEBUG + LTO for the same reason as extend_within_ffi: hot in-place
  -- fill/store whose lean.h helpers only inline away under optimization, bounds
  -- carried by the Lean-side reference body (+ conformance sweeps).
  let hardArgs := #["-O2", "-DNDEBUG"] ++ (← ltoFlags) ++
    if Platform.isWindows then #[] else #["-fPIC"]
  buildLeanO oFile srcJob #[] hardArgs

extern_lib libinflate_fast_ffi pkg := do
  let ffiO ← inflate_fast_ffi.o.fetch
  let name := nameToStaticLib "inflate_fast_ffi"
  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

lean_lib ZipTest where
  globs := #[.submodules `ZipTest]

@[default_target]
lean_exe test where
  root := `ZipTest