4kusto/vie - Change KJLCU4X5Z3CZM4AORMWIKOPBWPVTDMLK4LYH7UXBJFUGL7AUQCSQC

add scripts README and clarify perf tooling

Created by 4kusto on February 7, 2026

KJLCU4X5Z3CZM4AORMWIKOPBWPVTDMLK4LYH7UXBJFUGL7AUQCSQC

Dependencies

In channels

main

Change contents

Insertion in scripts/perf_profile.sh at line 2 [4.61]

[4.74]


# Roles:
#   - perf_profile.sh: full perf/c2c profiling for the bench binary.
#   - perf_bench_bin.sh: perf profiling of bench binary (no lake exec overhead).
#   - perf_bench_lake.sh: perf profiling via lake exe (includes lake overhead).
set -euo pipefail

Insertion in scripts/perf_profile.sh at line 26 [4.61]

[2.488]

FLAMEGRAPH_DIR="${FLAMEGRAPH_DIR:-$HOME/.local/bin/FlameGraph}"
STACKCOLLAPSE_BIN="${STACKCOLLAPSE_BIN:-${FLAMEGRAPH_DIR}/stackcollapse-perf.pl}"
FLAMEGRAPH_BIN="${FLAMEGRAPH_BIN:-${FLAMEGRAPH_DIR}/flamegraph.pl}"

Replacement in scripts/perf_profile.sh at line 74 [4.61]

B:BD[2.1273] → [2.1273:1377]

        if command -v stackcollapse-perf.pl &> /dev/null && command -v flamegraph.pl &> /dev/null; then

[2.1273]

[2.1377]

        if { [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; } || \
           { command -v stackcollapse-perf.pl &> /dev/null && command -v flamegraph.pl &> /dev/null; }; then

Replacement in scripts/perf_profile.sh at line 77 [4.61]

B:BD[2.1421] → [2.1421:1563]

            perf script -i "$PERF_DATA" | stackcollapse-perf.pl > "$PERF_FOLDED"
            flamegraph.pl "$PERF_FOLDED" > "$FLAMEGRAPH_SVG"

[2.1421]

[2.1563]

            if [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; then
                perf script -i "$PERF_DATA" | "${STACKCOLLAPSE_BIN}" > "$PERF_FOLDED"
                "${FLAMEGRAPH_BIN}" "$PERF_FOLDED" > "$FLAMEGRAPH_SVG"
            else
                perf script -i "$PERF_DATA" | stackcollapse-perf.pl > "$PERF_FOLDED"
                flamegraph.pl "$PERF_FOLDED" > "$FLAMEGRAPH_SVG"
            fi

Insertion in scripts/perf_profile.sh at line 86 [4.61]

[2.1655]

            echo "Expected in \$FLAMEGRAPH_DIR (default: ${FLAMEGRAPH_DIR})"

File addition: perf_bench_lake.sh (---x------)

[4.19]

#!/bin/bash
set -euo pipefail
# Usage:
#   scripts/perf_bench_lake.sh [iterations]
#
# Environment:
#   BENCH_ARGS         Extra args for benchmark (default: --no-render)
#   PERF_RESULTS_ROOT  Results root dir (default: perf)
#   PERF_RUN_LABEL     Label for run (default: HHMMSS)
#
# Example:
#   BENCH_ARGS="--case search-bloom --lines 800 --line-len 120 --no-render" scripts/perf_bench_lake.sh 2000
ITERATIONS="10000"
BENCH_ARGS="${BENCH_ARGS:---no-render}"
PERF_CASES="${PERF_CASES:-}"
usage() {
  cat <<'USAGE'
Usage:
  scripts/perf_bench_lake.sh [iterations]
  scripts/perf_bench_lake.sh --iterations N
  scripts/perf_bench_lake.sh --case NAME [--case NAME...]
  scripts/perf_bench_lake.sh --cases "case1,case2"
Notes:
  - Cases are passed through to: bench --case <name>
  - Aliases: linear -> search-linear, bloom -> search-bloom
  - Extra bench args via BENCH_ARGS env (default: --no-render)
USAGE
}
case_list=""
iter_set="0"
while [ "$#" -gt 0 ]; do
  case "$1" in
    -n|--iterations)
      ITERATIONS="${2:-}"
      iter_set="1"
      shift 2
      ;;
    --case)
      case_list="${case_list}${2:-},"
      shift 2
      ;;
    --cases)
      PERF_CASES="${2:-}"
      shift 2
      ;;
    -h|--help)
      usage
      exit 0
      ;;
    *)
      if [[ "$1" =~ ^[0-9]+$ ]] && [ "$iter_set" = "0" ]; then
        ITERATIONS="$1"
        iter_set="1"
        shift
      else
        echo "Error: unknown argument '$1'"
        usage
        exit 1
      fi
      ;;
  esac
done
if [ -n "$case_list" ]; then
  case_list="${case_list%,}"
  if [ -n "$PERF_CASES" ]; then
    PERF_CASES="${PERF_CASES},${case_list}"
  else
    PERF_CASES="${case_list}"
  fi
fi
RESULTS_ROOT="${PERF_RESULTS_ROOT:-perf}"
RUN_LABEL="${PERF_RUN_LABEL:-$(date +%H%M%S)}"
DATE_DIR="${RESULTS_ROOT}/$(date +%Y-%m-%d)"
REPORT_DIR="${DATE_DIR}/report"
PERF_DATA="${DATE_DIR}/perf-bench-${RUN_LABEL}.data"
PERF_REPORT="${REPORT_DIR}/perf-bench-${RUN_LABEL}.log"
FLAME_DIR="${DATE_DIR}/flamegraph"
PERF_FOLDED="${FLAME_DIR}/perf-bench-${RUN_LABEL}.folded"
FLAMEGRAPH_SVG="${FLAME_DIR}/flamegraph-bench-${RUN_LABEL}.svg"
FLAMEGRAPH_DIR="${FLAMEGRAPH_DIR:-$HOME/.local/bin/FlameGraph}"
STACKCOLLAPSE_BIN="${STACKCOLLAPSE_BIN:-${FLAMEGRAPH_DIR}/stackcollapse-perf.pl}"
FLAMEGRAPH_BIN="${FLAMEGRAPH_BIN:-${FLAMEGRAPH_DIR}/flamegraph.pl}"
echo "=== ViE perf (lake exe bench) ==="
echo "Iterations: ${ITERATIONS}"
echo "Bench args: ${BENCH_ARGS}"
if [ -n "${PERF_CASES}" ]; then
  echo "Perf cases: ${PERF_CASES}"
fi
echo "Results: ${DATE_DIR}"
# 1. Build bench
echo "Building benchmark..."
lake build bench
# 2. Check for perf
if ! command -v perf &> /dev/null; then
  echo "Error: 'perf' command not found. Please install perf."
  exit 1
fi
# 3. Prepare output directories
mkdir -p "${REPORT_DIR}" "${FLAME_DIR}"
# 4. Run perf record using lake exe bench -- <iterations> <args>
run_one () {
  local label="$1"
  shift
  local -a extra_args=("$@")
  local data="${DATE_DIR}/perf-bench-${label}.data"
  local report="${REPORT_DIR}/perf-bench-${label}.log"
  local folded="${FLAME_DIR}/perf-bench-${label}.folded"
  local svg="${FLAME_DIR}/flamegraph-bench-${label}.svg"
  echo "Running perf record (${label})..."
  perf record -g --call-graph dwarf -o "${data}" -- \
    lake exe bench -- "${ITERATIONS}" "${BENCH_ARGS_ARR[@]}" "${extra_args[@]}"
  echo "Writing report to ${report}"
  perf report -i "${data}" --stdio > "${report}"
  if { [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; } || \
     { command -v stackcollapse-perf.pl &> /dev/null && command -v flamegraph.pl &> /dev/null; }; then
    echo "Generating flamegraph (${label})..."
    if [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; then
      perf script -i "${data}" | "${STACKCOLLAPSE_BIN}" > "${folded}"
      "${FLAMEGRAPH_BIN}" "${folded}" > "${svg}"
    else
      perf script -i "${data}" | stackcollapse-perf.pl > "${folded}"
      flamegraph.pl "${folded}" > "${svg}"
    fi
  else
    echo "Flamegraph tools not found. Skipping flamegraph generation."
    echo "Expected in \$FLAMEGRAPH_DIR (default: ${FLAMEGRAPH_DIR})"
  fi
}
read -r -a BENCH_ARGS_ARR <<< "${BENCH_ARGS}"
if [ -n "${PERF_CASES}" ]; then
  IFS=',' read -r -a CASES_ARR <<< "${PERF_CASES}"
  for c in "${CASES_ARR[@]}"; do
    c_trim="$(echo "${c}" | xargs)"
    if [ -z "${c_trim}" ]; then
      continue
    fi
    case "${c_trim}" in
      linear) norm="search-linear" ;;
      bloom) norm="search-bloom" ;;
      *) norm="${c_trim}" ;;
    esac
    run_one "${RUN_LABEL}-${norm}" --case "${norm}"
  done
else
  run_one "${RUN_LABEL}"
fi
echo "Done."

File addition: perf_bench_bin.sh (---x------)

[4.19]

#!/bin/bash
set -euo pipefail
# Usage:
#   scripts/perf_bench_bin.sh [iterations]
#
# Environment:
#   BENCH_ARGS         Extra args for benchmark (default: --no-render)
#   BENCH_EXE          Path to bench binary (default: .lake/build/bin/bench)
#   PERF_RESULTS_ROOT  Results root dir (default: perf)
#   PERF_RUN_LABEL     Label for run (default: HHMMSS)
#   FLAMEGRAPH_DIR     Flamegraph tools dir (default: $HOME/.local/bin/Flamegraph)
#
# Example:
#   BENCH_ARGS="--case search-bloom --lines 800 --line-len 120 --no-render" scripts/perf_bench_bin.sh 2000
ITERATIONS="10000"
BENCH_ARGS="${BENCH_ARGS:---no-render}"
PERF_CASES="${PERF_CASES:-}"
usage() {
  cat <<'USAGE'
Usage:
  scripts/perf_bench_bin.sh [iterations]
  scripts/perf_bench_bin.sh --iterations N
  scripts/perf_bench_bin.sh --case NAME [--case NAME...]
  scripts/perf_bench_bin.sh --cases "case1,case2"
Notes:
  - Cases are passed through to: bench --case <name>
  - Aliases: linear -> search-linear, bloom -> search-bloom
  - Extra bench args via BENCH_ARGS env (default: --no-render)
USAGE
}
case_list=""
iter_set="0"
while [ "$#" -gt 0 ]; do
  case "$1" in
    -n|--iterations)
      ITERATIONS="${2:-}"
      iter_set="1"
      shift 2
      ;;
    --case)
      case_list="${case_list}${2:-},"
      shift 2
      ;;
    --cases)
      PERF_CASES="${2:-}"
      shift 2
      ;;
    -h|--help)
      usage
      exit 0
      ;;
    *)
      if [[ "$1" =~ ^[0-9]+$ ]] && [ "$iter_set" = "0" ]; then
        ITERATIONS="$1"
        iter_set="1"
        shift
      else
        echo "Error: unknown argument '$1'"
        usage
        exit 1
      fi
      ;;
  esac
done
if [ -n "$case_list" ]; then
  case_list="${case_list%,}"
  if [ -n "$PERF_CASES" ]; then
    PERF_CASES="${PERF_CASES},${case_list}"
  else
    PERF_CASES="${case_list}"
  fi
fi
BENCH_EXE="${BENCH_EXE:-.lake/build/bin/bench}"
RESULTS_ROOT="${PERF_RESULTS_ROOT:-perf}"
RUN_LABEL="${PERF_RUN_LABEL:-$(date +%H%M%S)}"
DATE_DIR="${RESULTS_ROOT}/$(date +%Y-%m-%d)"
REPORT_DIR="${DATE_DIR}/report"
PERF_DATA="${DATE_DIR}/perf-bench-bin-${RUN_LABEL}.data"
PERF_REPORT="${REPORT_DIR}/perf-bench-bin-${RUN_LABEL}.log"
FLAME_DIR="${DATE_DIR}/flamegraph"
PERF_FOLDED="${FLAME_DIR}/perf-bench-bin-${RUN_LABEL}.folded"
FLAMEGRAPH_SVG="${FLAME_DIR}/flamegraph-bench-bin-${RUN_LABEL}.svg"
FLAMEGRAPH_DIR="${FLAMEGRAPH_DIR:-$HOME/.local/bin/FlameGraph}"
STACKCOLLAPSE_BIN="${STACKCOLLAPSE_BIN:-${FLAMEGRAPH_DIR}/stackcollapse-perf.pl}"
FLAMEGRAPH_BIN="${FLAMEGRAPH_BIN:-${FLAMEGRAPH_DIR}/flamegraph.pl}"
echo "=== ViE perf (bench binary) ==="
echo "Iterations: ${ITERATIONS}"
echo "Bench args: ${BENCH_ARGS}"
if [ -n "${PERF_CASES}" ]; then
  echo "Perf cases: ${PERF_CASES}"
fi
echo "Bench exe:  ${BENCH_EXE}"
echo "Results: ${DATE_DIR}"
# 1. Build bench
echo "Building benchmark..."
lake build bench
if [ ! -x "${BENCH_EXE}" ]; then
  echo "Error: bench executable not found at ${BENCH_EXE}"
  exit 1
fi
# 2. Check for perf
if ! command -v perf &> /dev/null; then
  echo "Error: 'perf' command not found. Please install perf."
  exit 1
fi
# 3. Prepare output directories
mkdir -p "${REPORT_DIR}" "${FLAME_DIR}"
# 4. Run perf record against the bench binary (no lake exec overhead)
run_one () {
  local label="$1"
  shift
  local -a extra_args=("$@")
  local data="${DATE_DIR}/perf-bench-bin-${label}.data"
  local report="${REPORT_DIR}/perf-bench-bin-${label}.log"
  local folded="${FLAME_DIR}/perf-bench-bin-${label}.folded"
  local svg="${FLAME_DIR}/flamegraph-bench-bin-${label}.svg"
  echo "Running perf record (${label})..."
  perf record -g --call-graph dwarf -o "${data}" -- \
    "${BENCH_EXE}" "${ITERATIONS}" "${BENCH_ARGS_ARR[@]}" "${extra_args[@]}"
  echo "Writing report to ${report}"
  perf report -i "${data}" --stdio > "${report}"
  if { [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; } || \
     { command -v stackcollapse-perf.pl &> /dev/null && command -v flamegraph.pl &> /dev/null; }; then
    echo "Generating flamegraph (${label})..."
    if [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; then
      perf script -i "${data}" | "${STACKCOLLAPSE_BIN}" > "${folded}"
      "${FLAMEGRAPH_BIN}" "${folded}" > "${svg}"
    else
      perf script -i "${data}" | stackcollapse-perf.pl > "${folded}"
      flamegraph.pl "${folded}" > "${svg}"
    fi
  else
    echo "Flamegraph tools not found. Skipping flamegraph generation."
    echo "Expected in \$FLAMEGRAPH_DIR (default: ${FLAMEGRAPH_DIR})"
  fi
}
read -r -a BENCH_ARGS_ARR <<< "${BENCH_ARGS}"
if [ -n "${PERF_CASES}" ]; then
  IFS=',' read -r -a CASES_ARR <<< "${PERF_CASES}"
  for c in "${CASES_ARR[@]}"; do
    c_trim="$(echo "${c}" | xargs)"
    if [ -z "${c_trim}" ]; then
      continue
    fi
    case "${c_trim}" in
      linear) norm="search-linear" ;;
      bloom) norm="search-bloom" ;;
      *) norm="${c_trim}" ;;
    esac
    run_one "${RUN_LABEL}-${norm}" --case "${norm}"
  done
else
  run_one "${RUN_LABEL}"
fi
echo "Done."

File addition: README.md (----------)

[4.19]

# Scripts
This directory contains perf profiling helpers for the `bench` executable.
## Quick Summary
- `perf_bench_bin.sh`: perf record for the bench binary directly (no lake overhead).
- `perf_bench_lake.sh`: perf record via `lake exe bench` (includes lake overhead).
- `perf_profile.sh`: heavier profiling (perf and optional c2c) with reports and flamegraph.
## Common Output
All scripts write to `perf/YYYY-MM-DD/`:
- `report/`: perf report logs
- `flamegraph/`: folded stacks and SVG flamegraphs
- `c2c/`: cache-to-cache reports (when enabled)
## perf_bench_bin.sh
Purpose: fast perf capture of the bench binary.
Usage examples:
```bash
./scripts/perf_bench_bin.sh --iterations 10000 --case linear
./scripts/perf_bench_bin.sh --cases linear,bloom --iterations 20000
```
Key options:
- `--iterations N`
- `--case NAME` or `--cases NAME,NAME`
- `--no-render` is passed to the bench by default (override with `PERF_BENCH_ARGS`).
## perf_bench_lake.sh
Purpose: perf capture through `lake exe bench` (measures lake overhead too).
Usage examples:
```bash
./scripts/perf_bench_lake.sh --iterations 10000 --case linear
./scripts/perf_bench_lake.sh --cases linear,bloom --iterations 20000
```
Key options match `perf_bench_bin.sh`.
## perf_profile.sh
Purpose: heavier profiling (perf report + optional c2c) and flamegraph.
Usage examples:
```bash
./scripts/perf_profile.sh 10000
PERF_MODE=both ./scripts/perf_profile.sh 10000
PERF_MODE=c2c ./scripts/perf_profile.sh 10000
```
## Flamegraph Tools
By default, scripts look in:
- `$HOME/.local/bin/FlameGraph`
You can override with:
- `FLAMEGRAPH_DIR=/path/to/FlameGraph`
- `STACKCOLLAPSE_BIN=/path/to/stackcollapse-perf.pl`
- `FLAMEGRAPH_BIN=/path/to/flamegraph.pl`
## Environment Variables
- `PERF_RESULTS_ROOT`: results directory root (default: `perf`)
- `PERF_RUN_LABEL`: label for the run (default: `HHMMSS`)
- `PERF_BENCH_ARGS`: extra args passed to the bench executable
- `PERF_MODE`: for `perf_profile.sh` only (`perf`, `c2c`, `both`)
## Notes
- `perf` may require elevated permissions depending on your kernel settings.
- If you see a permissions error, check `kernel.perf_event_paranoid`.

Insertion in ViE/Types.lean at line 131 [6.22248]
[3.6835]
[5.72]
```
  searchBloomBuildLeafBits : Bool
```

Insertion in ViE/Types.lean at line 236 [6.22248]

[7.1567]

[8.6794]


  def recomputeMissingEol (buf : FileBuffer) : FileBuffer :=
    let len := buf.table.length
    let missing := if len == 0 then false else !buf.table.endsWithNewline
    { buf with missingEol := missing }

Replacement in ViE/State/Layout.lean at line 99 [6.42444]

B:BD[6.45479] → [9.4988:5098]

      let newBuffers := ws.buffers.map fun b => if b.id == v.bufferId then FileBuffer.clearCache (f b) else b

[6.45479]

[9.5098]

      let newBuffers := ws.buffers.map fun b =>
        if b.id == v.bufferId then
          let updated := FileBuffer.recomputeMissingEol (f b)
          FileBuffer.clearCache updated
        else b

Replacement in ViE/State/Edit.lean at line 23 [6.48173]

B:BD[6.48778] → [8.19313:19376]

  s'.setCursor { cursor with col := ⟨cursor.col.val + 1⟩ }

[6.48778]

[6.48820]

  let delta := ViE.Unicode.charWidth c
  s'.setCursor { cursor with col := ⟨cursor.col.val + delta⟩ }

Insertion in ViE/State/Config.lean at line 30 [6.53268]
[3.23147]
[6.53849]
```
  searchBloomBuildLeafBits := true
```

Replacement in ViE/IO.lean at line 36 [6.72280]

B:BD[6.73326] → [6.73326:73377]

    let newBuffer ← loadBufferByteArray filename

[6.73326]

[6.73377]

    let newBuffer ← loadBufferByteArrayWithConfig filename state.config

Replacement in ViE/Data/PieceTable.lean at line 8 [6.73967]

B:BD[6.74217] → [6.74217:74282]

def PieceTable.fromByteArray (bytes : ByteArray) : PieceTable :=

[6.74217]

[6.74282]

def PieceTable.fromByteArray (bytes : ByteArray) (buildLeafBits : Bool := true) : PieceTable :=

Replacement in ViE/Data/PieceTable.lean at line 10 [6.73967]

B:BD[6.74308] → [4.1961:2103]

    { original := bytes, addBuffers := #[], tree := PieceTree.empty, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }

[6.74308]

[6.74383]

    { original := bytes, addBuffers := #[], tree := PieceTree.empty, bloomBuildLeafBits := buildLeafBits,
      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }

Replacement in ViE/Data/PieceTable.lean at line 39 [6.73967]

B:BD[6.75467] → [3.26968:27178]

    let tmpPt : PieceTable := { original := bytes, addBuffers := #[], tree := PieceTree.empty, undoStack := [], redoStack := [], undoStackCount := 0, redoStackCount := 0, undoLimit := 100, lastInsert := none }

[6.75467]

[3.27178]

    let tmpPt : PieceTable := {
      original := bytes, addBuffers := #[], tree := PieceTree.empty, bloomBuildLeafBits := buildLeafBits,
      undoStack := [], redoStack := [], undoStackCount := 0, redoStackCount := 0, undoLimit := 100, lastInsert := none
    }

Replacement in ViE/Data/PieceTable.lean at line 44 [6.73967]

∅:D[3.27228] → [4.2467:2598]

B:BD[6.75511] → [4.2467:2598]

    { original := bytes, addBuffers := #[], tree := tree, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }

[3.27228]

[6.75575]

    { original := bytes, addBuffers := #[], tree := tree, bloomBuildLeafBits := buildLeafBits,
      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }

Replacement in ViE/Data/PieceTable.lean at line 48 [6.73967]

B:BD[6.75613] → [6.75613:75704]

def PieceTable.fromString (s : String) : PieceTable :=
  PieceTable.fromByteArray s.toUTF8

[6.75613]

[6.75704]

def PieceTable.fromString (s : String) (buildLeafBits : Bool := true) : PieceTable :=
  PieceTable.fromByteArray s.toUTF8 buildLeafBits

Replacement in ViE/Data/PieceTable/Tree.lean at line 190 [6.77490]
B:BD[3.32926] → [3.32926:32960]
```
  if !ViE.BloomBuildLeafBits then
```
[3.32926]
[3.32960]
```
  if !pt.bloomBuildLeafBits then
```

Replacement in ViE/Data/PieceTable/Tree.lean at line 696 [6.77490]

B:BD[3.44137] → [3.44137:44237]

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat)

[3.44137]

[3.44237]

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (_cacheMax : Nat)

Insertion in ViE/Data/PieceTable/Tree.lean at line 727 [6.77490]
[3.45341]
[3.45341]
```
        let overlap := pattern.size - 1
```
Replacement in ViE/Data/PieceTable/Tree.lean at line 736 [6.77490]
B:BD[3.45752] → [3.45752:45794]
```
            | ViE.PieceTree.leaf _ _ _ =>
```
[3.45752]
[3.45794]
```
            | ViE.PieceTree.leaf _ _ m =>
```

Replacement in ViE/Data/PieceTable/Tree.lean at line 739 [6.77490]

B:BD[3.45944] → [3.45944:45990]

                if remain < pattern.size then

[3.45944]

[3.45990]

                let globalStart := baseOffset + relStart
                let available := total - globalStart
                let readLen := min (remain + overlap) available
                if readLen < pattern.size then

Replacement in ViE/Data/PieceTable/Tree.lean at line 745 [6.77490]

B:BD[3.46050] → [3.46050:47187]

                  match node with
                  | ViE.PieceTree.leaf pieces _ m =>
                      let (bits, cache, order) :=
                        if bloomIsEmpty m.bits then
                          leafBloomBitsWithCache pieces pt baseOffset cache order cacheMax
                        else
                          (m.bits, cache, order)
                      if !bloomMayContain bits hashes then
                        (none, cache, order)
                      else
                        let bytes := getBytes node relStart remain pt
                        match findPatternInBytes bytes pattern 0 with
                        | some idx => (some (baseOffset + relStart + idx), cache, order)
                        | none => (none, cache, order)
                  | _ => (none, cache, order)
            | ViE.PieceTree.internal children _ _ =>
                let rec loop (i : Nat) (offset : Nat)
                  (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
                  : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
                  if i >= children.size then

[3.46050]

[3.47187]

                  let crossesBoundary := readLen > remain
                  if !crossesBoundary && !bloomMayContain m.bits hashes then

Replacement in ViE/Data/PieceTable/Tree.lean at line 749 [6.77490]

B:BD[3.47251] → [3.47251:47508]

                    let child := children[i]!
                    let childLen := length child
                    let childEnd := offset + childLen
                    if childEnd <= startOffset then
                      loop (i + 1) childEnd cache order

[3.47251]

[3.47508]

                    let bytes := getBytes t globalStart readLen pt
                    match findPatternInBytes bytes pattern 0 with
                    | some idx => (some (globalStart + idx), cache, order)
                    | none => (none, cache, order)
            | ViE.PieceTree.internal children _ m =>
                if !bloomMayContain m.bits hashes then
                  (none, cache, order)
                else
                  let rec loop (i : Nat) (offset : Nat)
                    (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
                    : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
                    if i >= children.size then
                      (none, cache, order)

Replacement in ViE/Data/PieceTable/Tree.lean at line 763 [6.77490]

B:BD[3.47533] → [3.47533:47807]

                      match searchNode child offset cache order with
                      | (some res, cache, order) => (some res, cache, order)
                      | (none, cache, order) => loop (i + 1) childEnd cache order
                loop 0 baseOffset cache order

[3.47533]

[3.47807]

                      let child := children[i]!
                      let childLen := length child
                      let childEnd := offset + childLen
                      if childEnd <= startOffset then
                        loop (i + 1) childEnd cache order
                      else
                        match searchNode child offset cache order with
                        | (some res, cache, order) => (some res, cache, order)
                        | (none, cache, order) => loop (i + 1) childEnd cache order
                  loop 0 baseOffset cache order

Replacement in ViE/Data/PieceTable/Tree.lean at line 777 [6.77490]

B:BD[3.48042] → [3.48042:48142]

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat)

[3.48042]

[3.48142]

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (_cacheMax : Nat)

Insertion in ViE/Data/PieceTable/Tree.lean at line 807 [6.77490]
[3.49283]
[3.49283]
```
      let overlap := pattern.size - 1
```
Replacement in ViE/Data/PieceTable/Tree.lean at line 816 [6.77490]
B:BD[3.49657] → [3.49657:49697]
```
          | ViE.PieceTree.leaf _ _ _ =>
```
[3.49657]
[3.49697]
```
          | ViE.PieceTree.leaf _ _ m =>
```

Replacement in ViE/Data/PieceTable/Tree.lean at line 818 [6.77490]

B:BD[3.49763] → [3.49763:49807]

              if relEnd < pattern.size then

[3.49763]

[3.49807]

              let globalEnd := baseOffset + relEnd
              let globalStart := if baseOffset > overlap then baseOffset - overlap else 0
              let readLen := globalEnd - globalStart
              if readLen < pattern.size then

Replacement in ViE/Data/PieceTable/Tree.lean at line 824 [6.77490]

B:BD[3.49863] → [3.49863:51273]

                match node with
                | ViE.PieceTree.leaf pieces _ m =>
                    let (bits, cache, order) :=
                      if bloomIsEmpty m.bits then
                        leafBloomBitsWithCache pieces pt baseOffset cache order cacheMax
                      else
                        (m.bits, cache, order)
                    if !bloomMayContain bits hashes then
                      (none, cache, order)
                    else
                      let bytes := getBytes node 0 relEnd pt
                      match findLastPatternInBytes bytes pattern with
                      | some idx => (some (baseOffset + idx), cache, order)
                      | none => (none, cache, order)
                | _ => (none, cache, order)
          | ViE.PieceTree.internal children _ _ =>
              let spans : Array (ViE.PieceTree × Nat) := Id.run do
                let mut acc : Array (ViE.PieceTree × Nat) := #[]
                let mut offset := baseOffset
                for child in children do
                  acc := acc.push (child, offset)
                  offset := offset + length child
                return acc
              let rec loop (i : Nat)
                (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
                : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
                if i >= spans.size then

[3.49863]

[3.51273]

                let crossesBoundary := globalStart < baseOffset
                if !crossesBoundary && !bloomMayContain m.bits hashes then

Replacement in ViE/Data/PieceTable/Tree.lean at line 828 [6.77490]

B:BD[3.51333] → [3.51333:51526]

                  let j := spans.size - 1 - i
                  let (child, childOffset) := spans[j]!
                  if childOffset >= end0 then
                    loop (i + 1) cache order

[3.51333]

[3.51526]

                  let bytes := getBytes t globalStart readLen pt
                  match findLastPatternInBytes bytes pattern with
                  | some idx =>
                      let pos := globalStart + idx
                      if pos < end0 then (some pos, cache, order) else (none, cache, order)
                  | none => (none, cache, order)
          | ViE.PieceTree.internal children _ m =>
              if !bloomMayContain m.bits hashes then
                (none, cache, order)
              else
                let spans : Array (ViE.PieceTree × Nat) := Id.run do
                  let mut acc : Array (ViE.PieceTree × Nat) := #[]
                  let mut offset := baseOffset
                  for child in children do
                    acc := acc.push (child, offset)
                    offset := offset + length child
                  return acc
                let rec loop (i : Nat)
                  (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
                  : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
                  if i >= spans.size then
                    (none, cache, order)

Replacement in ViE/Data/PieceTable/Tree.lean at line 851 [6.77490]

B:BD[3.51549] → [3.51549:51873]

                    match searchNode child childOffset cache order with
                    | (some res, cache, order) =>
                        if res < end0 then (some res, cache, order) else loop (i + 1) cache order
                    | (none, cache, order) => loop (i + 1) cache order
              loop 0 cache order

[3.51549]

[3.51873]

                    let j := spans.size - 1 - i
                    let (child, childOffset) := spans[j]!
                    if childOffset >= end0 then
                      loop (i + 1) cache order
                    else
                      match searchNode child childOffset cache order with
                      | (some res, cache, order) =>
                          if res < end0 then (some res, cache, order) else loop (i + 1) cache order
                      | (none, cache, order) => loop (i + 1) cache order
                loop 0 cache order

Deletion in ViE/Data/PieceTable/Piece.lean at line 51 [6.93514]

B:BD[3.52059] → [3.52059:52158]

/-- Build full bloom bits for leaf nodes (startup cost). -/
def BloomBuildLeafBits : Bool := false

Insertion in ViE/Data/PieceTable/Piece.lean at line 87 [6.93514]
[4.19665]
[4.19665]
```
  bloomBuildLeafBits : Bool := true
```

Replacement in ViE/Command/Explorer.lean at line 63 [6.108658]

B:BD[10.1409] → [10.1409:1521]

  let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some s!"preview://{title}") content with dirty := false }

[10.1409]

[10.1521]

  let buildLeafBits := state.config.searchBloomBuildLeafBits
  let buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some s!"preview://{title}") content buildLeafBits with dirty := false }

Replacement in ViE/Command/Explorer.lean at line 109 [6.108658]

B:BD[9.16591] → [9.16591:16664]

  let loaded ← ViE.loadPreviewBufferByteArray resolved previewMaxBytes

[9.16591]

[9.16664]

  let loaded ← ViE.loadPreviewBufferByteArrayWithConfig resolved previewMaxBytes state.config

Replacement in ViE/Command/Explorer.lean at line 185 [6.108658]

B:BD[10.4610] → [10.4610:4723]

            let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some "preview://") content with dirty := false }

[10.4610]

[10.4723]

            let buildLeafBits := s1.config.searchBloomBuildLeafBits
            let buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some "preview://") content buildLeafBits with dirty := false }

Replacement in ViE/Command/Explorer.lean at line 193 [6.108658]

B:BD[9.18951] → [9.18951:19062]

          let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some "preview://") content with dirty := false }

[9.18951]

[9.19062]

          let buildLeafBits := s1.config.searchBloomBuildLeafBits
          let buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some "preview://") content buildLeafBits with dirty := false }

Replacement in ViE/Buffer/Manager.lean at line 14 [6.117838]

∅:D[9.31652] → [6.118155:118239]

B:BD[6.118155] → [6.118155:118239]

    let buf : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer id filename content

[9.31652]

[9.31653]

    let buildLeafBits := state.config.searchBloomBuildLeafBits
    let buf : FileBuffer := ViE.Buffer.fileBufferFromTextBufferWithConfig id filename content buildLeafBits

Replacement in ViE/Buffer/Manager.lean at line 46 [6.117838]

B:BD[6.119102] → [6.119102:119163]

      let loadedBuf ← ViE.loadBufferByteArray resolvedPath

[6.119102]

[6.119163]

      let loadedBuf ← ViE.loadBufferByteArrayWithConfig resolvedPath state.config

Insertion in ViE/Buffer/LowIO.lean at line 9 [6.119821]

[6.119948]

def emptyBuffer (filename : Option String) (buildLeafBits : Bool) : FileBuffer := {
  id := 0
  filename := filename
  dirty := false
  table := PieceTable.fromString "" buildLeafBits
  missingEol := false
  cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
}
def bufferFromData (filename : String) (data : ByteArray) (buildLeafBits : Bool) : FileBuffer :=
  let missingEol := data.size > 0 && data[data.size - 1]! != 10
  let table := PieceTable.fromByteArray data buildLeafBits
  {
    id := 0
    filename := some filename
    dirty := false
    table := table
    missingEol := missingEol
    cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
  }

Replacement in ViE/Buffer/LowIO.lean at line 36 [6.119821]

B:BD[6.120167] → [6.120167:120337]

B:BD[6.120337] → [11.16695:16812]

∅:D[12.3727] → [6.120337:120347]

∅:D[11.16812] → [6.120337:120347]

∅:D[8.28610] → [6.120337:120347]

B:BD[6.120337] → [6.120337:120347]

        return {
          id := 0
          filename := some filename
          dirty := false
          table := PieceTable.fromString ""
          missingEol := false
          cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
        }

[6.120167]

[6.120347]

        return emptyBuffer (some filename) true

Replacement in ViE/Buffer/LowIO.lean at line 40 [6.119821]

B:BD[6.120440] → [6.120440:120782]

B:BD[6.120782] → [11.16813:16930]

∅:D[12.3779] → [6.120782:120792]

∅:D[11.16930] → [6.120782:120792]

∅:D[8.28648] → [6.120782:120792]

B:BD[6.120782] → [6.120782:120792]


        -- Check if file ends with newline (POSIX compliance)
        let missingEol := data.size > 0 && data[data.size - 1]! != 10
        let table := PieceTable.fromByteArray data
        return {
          id := 0
          filename := some filename
          dirty := false
          table := table
          missingEol := missingEol
          cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
        }

[6.120440]

[6.120792]

        return bufferFromData filename data true

Replacement in ViE/Buffer/LowIO.lean at line 43 [6.119821]

B:BD[6.120850] → [6.120850:121008]

B:BD[6.121008] → [11.16931:17046]

∅:D[12.3829] → [6.121008:121016]

∅:D[11.17046] → [6.121008:121016]

∅:D[8.28684] → [6.121008:121016]

B:BD[6.121008] → [6.121008:121016]

      return {
        id := 0
        filename := some filename
        dirty := false
        table := PieceTable.fromString ""
        missingEol := false
        cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
      }

[6.120850]

[6.121016]

      return emptyBuffer (some filename) true

Replacement in ViE/Buffer/LowIO.lean at line 46 [6.119821]

B:BD[6.121066] → [6.121066:121212]

B:BD[6.121212] → [11.17047:17160]

∅:D[12.3877] → [6.121212:121218]

∅:D[11.17160] → [6.121212:121218]

∅:D[8.28718] → [6.121212:121218]

B:BD[6.121212] → [6.121212:121218]

    return {
      id := 0
      filename := some filename
      dirty := false
      table := PieceTable.fromString ""
      missingEol := false
      cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
    }

[6.121066]

[6.121218]

    return emptyBuffer (some filename) true
def loadBufferByteArrayWithConfig (filename : String) (config : EditorConfig) : IO FileBuffer := do
  let buildLeafBits := config.searchBloomBuildLeafBits
  try
    let path := System.FilePath.mk filename
    if ← path.pathExists then
      if ← path.isDir then
        return emptyBuffer (some filename) buildLeafBits
      else
        let data ← IO.FS.readBinFile filename
        return bufferFromData filename data buildLeafBits
    else
      return emptyBuffer (some filename) buildLeafBits
  catch _ =>
    return emptyBuffer (some filename) buildLeafBits

Replacement in ViE/Buffer/LowIO.lean at line 68 [6.119821]

B:BD[9.32935] → [9.32935:33232]

        return {
          id := 0
          filename := some filename
          dirty := false
          table := PieceTable.fromString ""
          missingEol := false
          cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
        }

[9.32935]

[9.33232]

        return emptyBuffer (some filename) true

Replacement in ViE/Buffer/LowIO.lean at line 72 [6.119821]

B:BD[9.33363] → [9.33363:33767]

        let missingEol := data.size > 0 && data[data.size - 1]! != 10
        let table := PieceTable.fromByteArray data
        return {
          id := 0
          filename := some filename
          dirty := false
          table := table
          missingEol := missingEol
          cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
        }

[9.33363]

[9.33767]

        return bufferFromData filename data true

Replacement in ViE/Buffer/LowIO.lean at line 74 [6.119821]

B:BD[9.33776] → [9.33776:34057]

      return {
        id := 0
        filename := some filename
        dirty := false
        table := PieceTable.fromString ""
        missingEol := false
        cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
      }

[9.33776]

[9.34057]

      return emptyBuffer (some filename) true
  catch _ =>
    return emptyBuffer (some filename) true
def loadPreviewBufferByteArrayWithConfig (filename : String) (maxBytes : Nat) (config : EditorConfig) : IO FileBuffer := do
  let buildLeafBits := config.searchBloomBuildLeafBits
  try
    let path := System.FilePath.mk filename
    if ← path.pathExists then
      if ← path.isDir then
        return emptyBuffer (some filename) buildLeafBits
      else
        let data ← IO.FS.withFile filename IO.FS.Mode.read fun handle =>
          handle.read (USize.ofNat maxBytes)
        return bufferFromData filename data buildLeafBits
    else
      return emptyBuffer (some filename) buildLeafBits

Replacement in ViE/Buffer/LowIO.lean at line 92 [6.119821]

B:BD[9.34070] → [9.34070:34335]

    return {
      id := 0
      filename := some filename
      dirty := false
      table := PieceTable.fromString ""
      missingEol := false
      cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
    }

[9.34070]

[9.34335]

    return emptyBuffer (some filename) buildLeafBits

Insertion in ViE/Buffer/Content.lean at line 63 [6.121265]

[6.122663]

/-- Create/Update FileBuffer from TextBuffer with bloom config. -/
def fileBufferFromTextBufferWithConfig (id : Nat) (filename : Option String) (content : TextBuffer) (buildLeafBits : Bool) : FileBuffer :=
  let fullString := String.intercalate "\n" (content.toList.map lineToString)
  let table := PieceTable.fromString fullString buildLeafBits
  {
    id := id
    filename := filename
    dirty := true -- Assume dirty if created from manual content
    table := table
    missingEol := false -- Default
    cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
  }

Replacement in ViE/App.lean at line 114 [6.125244]

B:BD[6.128270] → [6.128270:128316]

    | some fname => loadBufferByteArray fname

[6.128270]

[6.128316]

    | some fname => loadBufferByteArrayWithConfig fname config.settings

Replacement in ViE/App.lean at line 119 [6.125244]

B:BD[6.128411] → [6.128411:128453]

        table := PieceTable.fromString ""

[6.128411]

[6.128453]

        table := PieceTable.fromString "" config.settings.searchBloomBuildLeafBits

Insertion in Test.lean at line 17 [5.10091]
[12.4127]
[10.7713]
```
import Test.PieceTable.Search
import Test.MissingEol
```
Insertion in Test.lean at line 40 [5.10091]
[12.4277]
[5.10312]
```
  Test.PieceTable.Search.test
  Test.MissingEol.test
```

File addition: Search.lean (----------)

[12.6120]

import ViE.Data.PieceTable
import Test.Utils
open ViE
namespace Test.PieceTable.Search
open Test.Utils
def makeBoundaryTable : PieceTable :=
  let n := ViE.NodeCapacity + 1
  let startIdx := n / 2 - 1
  let chars := Id.run do
    let mut cs := Array.replicate n 'x'
    cs := cs.set! startIdx 'a'
    cs := cs.set! (startIdx + 1) 'b'
    cs := cs.set! (startIdx + 2) 'c'
    return cs
  let s := String.ofList chars.toList
  let bytes := s.toUTF8
  let pieces := (Array.range n).map fun i =>
    { source := BufferSource.original
      start := i
      length := 1
      lineBreaks := 0
      charCount := 1 }
  let tmp : PieceTable := {
    original := bytes
    addBuffers := #[]
    tree := PieceTree.empty
    undoStack := []
    redoStack := []
    undoStackCount := 0
    redoStackCount := 0
    undoLimit := 100
    lastInsert := none
  }
  let tree := PieceTree.fromPieces pieces tmp
  { tmp with tree := tree }
def testCrossLeafSearch : IO Unit := do
  IO.println "testCrossLeafSearch..."
  let pt := makeBoundaryTable
  let n := ViE.NodeCapacity + 1
  let startIdx := n / 2 - 1
  let pattern := "abc".toUTF8
  let (r1, _, _) := PieceTree.searchNext pt.tree pt pattern 0 64 true (Lean.RBMap.empty) #[] 16
  assertEqual "searchNext bloom across leaf" (some startIdx) r1
  let total := pt.tree.length
  let (r2, _, _) := PieceTree.searchPrev pt.tree pt pattern total 64 true (Lean.RBMap.empty) #[] 16
  assertEqual "searchPrev bloom across leaf" (some startIdx) r2
def testCrossLeafSearchNearBoundary : IO Unit := do
  IO.println "testCrossLeafSearchNearBoundary..."
  let pt := makeBoundaryTable
  let n := ViE.NodeCapacity + 1
  let startIdx := n / 2 - 1
  let pattern := "abc".toUTF8
  let startOffset := startIdx - 1
  let (r1, _, _) := PieceTree.searchNext pt.tree pt pattern startOffset 64 true (Lean.RBMap.empty) #[] 16
  assertEqual "searchNext from near boundary" (some startIdx) r1
  let startExclusive := startIdx + pattern.size
  let (r2, _, _) := PieceTree.searchPrev pt.tree pt pattern startExclusive 64 true (Lean.RBMap.empty) #[] 16
  assertEqual "searchPrev to near boundary" (some startIdx) r2
def test : IO Unit := do
  IO.println "Starting PieceTable Search Test..."
  testCrossLeafSearch
  testCrossLeafSearchNearBoundary
  IO.println "PieceTable Search Test passed!"
end Test.PieceTable.Search

File addition: MissingEol.lean (----------)

[5.10364]

import ViE.State.Config
import ViE.State.Layout
import ViE.Data.PieceTable
import Test.Utils
open ViE
namespace Test.MissingEol
open Test.Utils
def testMissingEol : IO Unit := do
  IO.println "testMissingEol..."
  let s := ViE.initialState
  let s := s.updateActiveBuffer fun buffer =>
    { buffer with table := PieceTable.fromString "abc\n", dirty := true }
  let buf := s.getActiveBuffer
  assert "missingEol false with trailing newline" (!buf.missingEol)
  let len := buf.table.length
  let s := s.updateActiveBuffer fun buffer =>
    { buffer with table := buffer.table.delete (len - 1) 1 (len - 1), dirty := true }
  let buf2 := s.getActiveBuffer
  assert "missingEol true after deleting newline" buf2.missingEol
  let s := ViE.initialState
  let s := s.updateActiveBuffer fun buffer =>
    { buffer with table := PieceTable.fromString "abc", dirty := true }
  let buf3 := s.getActiveBuffer
  assert "missingEol true without newline" buf3.missingEol
  let len2 := buf3.table.length
  let s := s.updateActiveBuffer fun buffer =>
    { buffer with table := buffer.table.insert len2 "\n" len2, dirty := true }
  let buf4 := s.getActiveBuffer
  assert "missingEol false after adding newline" (!buf4.missingEol)
def test : IO Unit := do
  IO.println "Starting MissingEol Test..."
  testMissingEol
  IO.println "MissingEol Test passed!"
end Test.MissingEol

Insertion in Test/CursorReproduction.lean at line 52 [4.26434]

[4.27797]

  -- Scenario: Wide character insert moves cursor by display width
  let s := ViE.initialState
  let wide := Char.ofNat 0x3042 -- Hiragana A (wide)
  let s := s.insertChar wide
  let cursor := s.getCursor
  if cursor.col.val != 2 then
     IO.println s!"[FAIL] Wide char cursor mismatch. Expected 2, got {cursor.col.val}"
     assert "Wide char cursor" false
  else
     IO.println "[PASS] Wide char cursor correct"

Insertion in Test/Benchmark.lean at line 6 [4.29255]
[4.29363]
[4.29363]
```
import ViE.State.Search
import ViE.Data.PieceTable.Tree
```

Replacement in Test/Benchmark.lean at line 15 [4.29255]

B:BD[4.29449] → [4.29449:29624]

def makeBenchConfig : Config := {
  settings := ViE.defaultConfig
  commands := ViE.Command.defaultCommandMap
  bindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap
}

[4.29449]

[4.29624]

def makeBenchConfig (buildLeafBits : Option Bool := none) : Config :=
  let base := ViE.defaultConfig
  let settings :=
    match buildLeafBits with
    | some v => { base with searchBloomBuildLeafBits := v }
    | none => base
  {
    settings := settings
    commands := ViE.Command.defaultCommandMap
    bindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap
  }
structure BenchOptions where
  iterations : Nat := 1000
  render : Bool := true
  cases : List String := []
  textLines : Nat := 200
  lineLen : Nat := 80
  warmup : Nat := 0
  buildLeafBits : Option Bool := none
  listOnly : Bool := false
def parseArgs (args : List String) : BenchOptions :=
  let rec loop (opts : BenchOptions) (args : List String) : BenchOptions :=
    match args with
    | [] => opts
    | "--no-render" :: rest => loop { opts with render := false } rest
    | "--case" :: name :: rest => loop { opts with cases := opts.cases ++ [name] } rest
    | "--lines" :: n :: rest =>
        match n.toNat? with
        | some v => loop { opts with textLines := v } rest
        | none => loop opts rest
    | "--line-len" :: n :: rest =>
        match n.toNat? with
        | some v => loop { opts with lineLen := v } rest
        | none => loop opts rest
    | "--warmup" :: n :: rest =>
        match n.toNat? with
        | some v => loop { opts with warmup := v } rest
        | none => loop opts rest
    | "--bloom-leaf-bits" :: rest => loop { opts with buildLeafBits := some true } rest
    | "--no-bloom-leaf-bits" :: rest => loop { opts with buildLeafBits := some false } rest
    | "--list" :: rest => loop { opts with listOnly := true } rest
    | arg :: rest =>
        match arg.toNat? with
        | some v => loop { opts with iterations := v } rest
        | none => loop opts rest
  loop {} args
/-- Simple timer helper -/
def timeCase (label : String) (iterations : Nat) (f : IO Unit) : IO Unit := do
  let t0 ← IO.monoMsNow
  f
  let t1 ← IO.monoMsNow
  let ms := t1 - t0
  let opsPerSec := if ms == 0 then 0 else (iterations * 1000) / ms
  IO.println s!"[bench] {label}: {ms} ms ({opsPerSec} ops/s)"
/-- Build a simple multi-line ASCII buffer for search benchmarks. -/
def buildText (lines : Nat) (lineLen : Nat) : String :=
  let line := String.ofList (List.replicate lineLen 'a')
  String.intercalate "\n" (List.replicate lines line)
/-- Insert a needle in the middle of text for search benchmarks. -/
def buildSearchText (lines : Nat) (lineLen : Nat) (needle : String) : String :=
  let baseLine := String.ofList (List.replicate lineLen 'a')
  let mid := lines / 2
  let leftLen := lineLen / 2
  let rightLen := if lineLen > leftLen + needle.length then lineLen - leftLen - needle.length else 0
  let needleLine :=
    (String.ofList (List.replicate leftLen 'a')) ++
    needle ++
    (String.ofList (List.replicate rightLen 'a'))
  let linesArr := Id.run do
    let mut arr := Array.replicate lines baseLine
    if mid < arr.size then
      arr := arr.set! mid needleLine
    return arr
  String.intercalate "\n" linesArr.toList

Replacement in Test/Benchmark.lean at line 95 [4.29255]

B:BD[4.29625] → [2.2501:2618]

∅:D[2.2618] → [4.29717:29750]

B:BD[4.29717] → [4.29717:29750]

/-- Simulate a heavy editing session. -/
def runBenchmark (iterations : Nat) (render : Bool := true) : IO Unit := do
  let _config := makeBenchConfig

[4.29625]

[4.29750]

/-- Case: Large insert workload (EditorState). -/
def benchInsert (iterations : Nat) : IO Unit := do

Deletion in Test/Benchmark.lean at line 98 [4.29255]

B:BD[4.29782] → [4.29782:29883]


  -- 1. Initial Large Insertion
  IO.println s!"Starting benchmark with {iterations} iterations..."

Replacement in Test/Benchmark.lean at line 103 [4.29255]

B:BD[4.29988] → [4.29988:30077]

  -- 2. Random Access / Movement
  for _ in [0:iterations/10] do
    s := s.moveCursorUp

[4.29988]

[4.30077]

/-- Case: Mixed small edits/movements. -/
def benchEditMix (iterations : Nat) : IO Unit := do
  let mut s := ViE.initialState
  for _ in [0:iterations] do
    s := s.insertChar 'a'

Insertion in Test/Benchmark.lean at line 110 [4.29255]
[4.30129]
[4.30129]
```
    s := s.moveCursorRight
```

Replacement in Test/Benchmark.lean at line 112 [4.29255]

B:BD[4.30130] → [4.30130:30237]

  -- 3. Clipboard (Yank / Paste)
  IO.println "Benchmarking Clipboard..."
  for _ in [0:iterations/100] do

[4.30130]

[4.30237]

/-- Case: Clipboard (yank/paste). -/
def benchClipboard (iterations : Nat) : IO Unit := do
  let mut s := ViE.initialState
  s := s.insertChar 'x'
  for _ in [0:iterations/50] do

Replacement in Test/Benchmark.lean at line 120 [4.29255]

B:BD[4.30287] → [4.30287:30404]

  -- 4. Workgroups (New / Switch / Close)
  IO.println "Benchmarking Workgroups..."
  for i in [0:iterations/500] do

[4.30287]

[4.30404]

/-- Case: Workgroup churn. -/
def benchWorkgroups (iterations : Nat) : IO Unit := do
  let mut s := ViE.initialState
  for i in [0:iterations/200] do

Insertion in Test/Benchmark.lean at line 126 [4.29255]

[4.30491]

  for _ in [0:iterations/200] do
    s := ← ViE.Command.cmdWg ["close"] s

Replacement in Test/Benchmark.lean at line 129 [4.29255]

B:BD[4.30492] → [4.30492:30535]

  -- Close them back (stress test closing)

[4.30492]

[4.30535]

/-- Case: Window splits/cycles. -/
def benchWindows (iterations : Nat) : IO Unit := do
  let mut s := ViE.initialState

Replacement in Test/Benchmark.lean at line 133 [4.29255]

B:BD[4.30568] → [4.30568:30913]

    s := ← ViE.Command.cmdWg ["close"] s
  -- 5. Windows (Split / Cycle / Close)
  IO.println "Benchmarking Windows..."
  -- Note: Limit total windows to avoid extreme UI depth in benchmark
  for _ in [0:iterations/1000] do
    s := ViE.Window.splitWindow s true  -- Vertical split
    s := ViE.Window.splitWindow s false -- Horizontal split

[4.30568]

[4.30913]

    s := ViE.Window.splitWindow s true
    s := ViE.Window.splitWindow s false

Replacement in Test/Benchmark.lean at line 137 [4.29255]
B:BD[4.30973] → [4.30973:31026]
```
  -- Close windows
  for _ in [0:iterations/500] do
```
[4.30973]
[4.31026]
```
  for _ in [0:iterations/200] do
```

Replacement in Test/Benchmark.lean at line 140 [4.29255]

B:BD[4.31067] → [4.31067:31167]

  -- 6. Undo / Redo stress
  IO.println "Benchmarking Undo/Redo..."
  for _ in [0:iterations/20] do

[4.31067]

[4.31167]

/-- Case: Undo/Redo stress. -/
def benchUndoRedo (iterations : Nat) : IO Unit := do
  let mut s := ViE.initialState
  for i in [0:iterations] do
    s := s.insertChar 'a'
    if i % 50 == 0 then
      s := s.commitEdit
  for _ in [0:iterations/10] do

Insertion in Test/Benchmark.lean at line 149 [4.29255]
[4.31183]
[4.31183]
```
  for _ in [0:iterations/10] do
    s := s.redo
```

Replacement in Test/Benchmark.lean at line 152 [4.29255]

B:BD[4.31184] → [4.31184:31248]

B:BD[4.31248] → [2.2619:2666]

  -- 7. Render Simulation (Crucial for B+ tree traversal check)
  if render then
    let _ ← ViE.UI.render s

[4.31184]

[4.31345]

/-- Case: Search workload (PieceTable). -/
def benchSearch (iterations : Nat) (useBloom : Bool) (lines lineLen : Nat) (buildLeafBits : Bool) (cacheMax : Nat) : IO Unit := do
  let needle := "needle"
  let text := buildSearchText lines lineLen needle
  let pt := PieceTable.fromString text buildLeafBits
  let pattern := needle.toUTF8
  let mut offset := 0
  let mut cache : Lean.RBMap Nat ByteArray compare := Lean.RBMap.empty
  let mut order : Array Nat := #[]
  for _ in [0:iterations] do
    let (res, cache', order') := PieceTree.searchNext pt.tree pt pattern offset searchChunkSize useBloom cache order cacheMax
    cache := cache'
    order := order'
    offset := match res with
      | some r => r + 1
      | none => 0
/-- Case: Render workload. -/
def benchRender (iterations : Nat) : IO Unit := do
  let mut s := ViE.initialState
  for _ in [0:iterations/20] do
    s := s.insertChar 'a'
  let _ ← ViE.UI.render s

Insertion in Test/Benchmark.lean at line 177 [4.29255]

[4.31346]

def availableCases : List String :=
  [ "insert", "edit", "clipboard", "workgroups", "windows", "undo", "search-bloom", "search-linear", "render" ]
/-- Run benchmark cases. -/
def runBenchmark (opts : BenchOptions) : IO Unit := do
  let buildLeafBits := opts.buildLeafBits.getD ViE.defaultConfig.searchBloomBuildLeafBits
  let config := makeBenchConfig (some buildLeafBits)
  let cacheMax := config.settings.searchBloomCacheMax
  let cases := if opts.cases.isEmpty then availableCases else opts.cases
  IO.println s!"Starting benchmark: iter={opts.iterations}, render={opts.render}"
  if opts.warmup > 0 then
    IO.println s!"Warmup: {opts.warmup} iterations"
    for _ in [0:opts.warmup] do
      let mut s := ViE.initialState
      s := s.insertChar 'a'
      let _ ← pure s
  for c in cases do
    match c with
    | "insert" => timeCase "insert" opts.iterations (benchInsert opts.iterations)
    | "edit" => timeCase "edit" opts.iterations (benchEditMix opts.iterations)
    | "clipboard" => timeCase "clipboard" opts.iterations (benchClipboard opts.iterations)
    | "workgroups" => timeCase "workgroups" opts.iterations (benchWorkgroups opts.iterations)
    | "windows" => timeCase "windows" opts.iterations (benchWindows opts.iterations)
    | "undo" => timeCase "undo/redo" opts.iterations (benchUndoRedo opts.iterations)
    | "search-bloom" =>
        timeCase "search-bloom" opts.iterations (benchSearch opts.iterations true opts.textLines opts.lineLen buildLeafBits cacheMax)
    | "search-linear" =>
        timeCase "search-linear" opts.iterations (benchSearch opts.iterations false opts.textLines opts.lineLen buildLeafBits cacheMax)
    | "render" =>
        if opts.render then
          timeCase "render" opts.iterations (benchRender opts.iterations)
        else
          IO.println "[bench] render skipped (--no-render)"
    | other =>
        IO.println s!"[bench] Unknown case: {other}"

Insertion in Test/Benchmark.lean at line 220 [4.29255]
[4.31402]
[4.31402]
```
/-- CLI entrypoint. -/
```

Replacement in Test/Benchmark.lean at line 222 [4.29255]

B:BD[4.31448] → [4.31448:31506]

B:BD[4.31506] → [2.2667:2855]

  let iter := args[0]? |>.bind String.toNat? |>.getD 1000
  let noRender := args.any (fun a => a == "--no-render")
  let render := !noRender
  -- Run benchmark; rendering can be disabled with --no-render.
  ViE.Benchmark.runBenchmark iter render

[4.31448]

  let opts := ViE.Benchmark.parseArgs args
  if opts.listOnly then
    IO.println "Available cases:"
    IO.println (String.intercalate ", " ViE.Benchmark.availableCases)
  else
    ViE.Benchmark.runBenchmark opts

add scripts README and clarify perf tooling

Dependencies

In channels

Change contents

Insertion in scripts/perf_profile.sh at line 2 [4.61]

Insertion in scripts/perf_profile.sh at line 26 [4.61]

Replacement in scripts/perf_profile.sh at line 74 [4.61]

Replacement in scripts/perf_profile.sh at line 77 [4.61]

Insertion in scripts/perf_profile.sh at line 86 [4.61]

File addition: perf_bench_lake.sh (---x------)

File addition: perf_bench_bin.sh (---x------)

File addition: README.md (----------)

Insertion in ViE/Types.lean at line 131 [6.22248]

Insertion in ViE/Types.lean at line 236 [6.22248]

Replacement in ViE/State/Layout.lean at line 99 [6.42444]

Replacement in ViE/State/Edit.lean at line 23 [6.48173]

Insertion in ViE/State/Config.lean at line 30 [6.53268]

Replacement in ViE/IO.lean at line 36 [6.72280]

Replacement in ViE/Data/PieceTable.lean at line 8 [6.73967]

Replacement in ViE/Data/PieceTable.lean at line 10 [6.73967]

Replacement in ViE/Data/PieceTable.lean at line 39 [6.73967]

Replacement in ViE/Data/PieceTable.lean at line 44 [6.73967]

Replacement in ViE/Data/PieceTable.lean at line 48 [6.73967]

Replacement in ViE/Data/PieceTable/Tree.lean at line 190 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 696 [6.77490]

Insertion in ViE/Data/PieceTable/Tree.lean at line 727 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 736 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 739 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 745 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 749 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 763 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 777 [6.77490]

Insertion in ViE/Data/PieceTable/Tree.lean at line 807 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 816 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 818 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 824 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 828 [6.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 851 [6.77490]

Deletion in ViE/Data/PieceTable/Piece.lean at line 51 [6.93514]

Insertion in ViE/Data/PieceTable/Piece.lean at line 87 [6.93514]

Replacement in ViE/Command/Explorer.lean at line 63 [6.108658]

Replacement in ViE/Command/Explorer.lean at line 109 [6.108658]

Replacement in ViE/Command/Explorer.lean at line 185 [6.108658]

Replacement in ViE/Command/Explorer.lean at line 193 [6.108658]

Replacement in ViE/Buffer/Manager.lean at line 14 [6.117838]

Replacement in ViE/Buffer/Manager.lean at line 46 [6.117838]

Insertion in ViE/Buffer/LowIO.lean at line 9 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 36 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 40 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 43 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 46 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 68 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 72 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 74 [6.119821]

Replacement in ViE/Buffer/LowIO.lean at line 92 [6.119821]

Insertion in ViE/Buffer/Content.lean at line 63 [6.121265]

Replacement in ViE/App.lean at line 114 [6.125244]

Replacement in ViE/App.lean at line 119 [6.125244]

Insertion in Test.lean at line 17 [5.10091]

Insertion in Test.lean at line 40 [5.10091]

File addition: Search.lean (----------)

File addition: MissingEol.lean (----------)

Insertion in Test/CursorReproduction.lean at line 52 [4.26434]

Insertion in Test/Benchmark.lean at line 6 [4.29255]

Replacement in Test/Benchmark.lean at line 15 [4.29255]

Replacement in Test/Benchmark.lean at line 95 [4.29255]

Deletion in Test/Benchmark.lean at line 98 [4.29255]

Replacement in Test/Benchmark.lean at line 103 [4.29255]

Insertion in Test/Benchmark.lean at line 110 [4.29255]

Replacement in Test/Benchmark.lean at line 112 [4.29255]

Replacement in Test/Benchmark.lean at line 120 [4.29255]

Insertion in Test/Benchmark.lean at line 126 [4.29255]

Replacement in Test/Benchmark.lean at line 129 [4.29255]

Replacement in Test/Benchmark.lean at line 133 [4.29255]

Replacement in Test/Benchmark.lean at line 137 [4.29255]

Replacement in Test/Benchmark.lean at line 140 [4.29255]

Insertion in Test/Benchmark.lean at line 149 [4.29255]

Replacement in Test/Benchmark.lean at line 152 [4.29255]

Insertion in Test/Benchmark.lean at line 177 [4.29255]

Insertion in Test/Benchmark.lean at line 220 [4.29255]