KJLCU4X5Z3CZM4AORMWIKOPBWPVTDMLK4LYH7UXBJFUGL7AUQCSQC B7Q32HRFDMDDMQPLBKWS42NWSXLARPAOVZXCDQG2I3J2WVTWNFNQC CNJGJCJZ6LRHHIRSRATSE3D3Z5OQGSSTDMXCPVXSKRQLYJFME6IAC GUD2J453E3UTRJZIEEUUJ3ZIGL72ETUXTO57XQIZ2Y3ZU3C2R55QC 5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC 6W6OJAUT3KLOXXKYR4GA3MG4ACLO2T4KX3SGD2KZDX6MYEZYTPHAC OHL2PRHBX74FZKWZU7IR6RSXA36PDZDROVI4AHTX4SO7VQFQ5RQQC WRBKZMYVNHRWT7TTUGTDJ3TMWZB32QYW5PCLKTTVAJ2YF6OI3LTAC XCVPXP4UBFU25NF6VQC3MEYHHH45RL2UXM5TA6O23NA64FPCCCJQC YILSJ2SNU6DNZVSFL4MD6QSNLQHUNSBSTGGEQCFTWFTRR62IXBWAC NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC U45XPF3YKPXXRJ4MN24T2RV7GOL4FZKQSWX5P5I7WT4HC5XF4FHAC if command -v stackcollapse-perf.pl &> /dev/null && command -v flamegraph.pl &> /dev/null; then
if { [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; } || \{ command -v stackcollapse-perf.pl &> /dev/null && command -v flamegraph.pl &> /dev/null; }; then
perf script -i "$PERF_DATA" | stackcollapse-perf.pl > "$PERF_FOLDED"flamegraph.pl "$PERF_FOLDED" > "$FLAMEGRAPH_SVG"
if [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; thenperf script -i "$PERF_DATA" | "${STACKCOLLAPSE_BIN}" > "$PERF_FOLDED""${FLAMEGRAPH_BIN}" "$PERF_FOLDED" > "$FLAMEGRAPH_SVG"elseperf script -i "$PERF_DATA" | stackcollapse-perf.pl > "$PERF_FOLDED"flamegraph.pl "$PERF_FOLDED" > "$FLAMEGRAPH_SVG"fi
#!/bin/bashset -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 2000ITERATIONS="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 Nscripts/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 ]; docase "$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)usageexit 0;;*)if [[ "$1" =~ ^[0-9]+$ ]] && [ "$iter_set" = "0" ]; thenITERATIONS="$1"iter_set="1"shiftelseecho "Error: unknown argument '$1'"usageexit 1fi;;esacdoneif [ -n "$case_list" ]; thencase_list="${case_list%,}"if [ -n "$PERF_CASES" ]; thenPERF_CASES="${PERF_CASES},${case_list}"elsePERF_CASES="${case_list}"fifiRESULTS_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}" ]; thenecho "Perf cases: ${PERF_CASES}"fiecho "Results: ${DATE_DIR}"# 1. Build benchecho "Building benchmark..."lake build bench# 2. Check for perfif ! command -v perf &> /dev/null; thenecho "Error: 'perf' command not found. Please install perf."exit 1fi# 3. Prepare output directoriesmkdir -p "${REPORT_DIR}" "${FLAME_DIR}"# 4. Run perf record using lake exe bench -- <iterations> <args>run_one () {local label="$1"shiftlocal -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; }; thenecho "Generating flamegraph (${label})..."if [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; thenperf script -i "${data}" | "${STACKCOLLAPSE_BIN}" > "${folded}""${FLAMEGRAPH_BIN}" "${folded}" > "${svg}"elseperf script -i "${data}" | stackcollapse-perf.pl > "${folded}"flamegraph.pl "${folded}" > "${svg}"fielseecho "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}" ]; thenIFS=',' read -r -a CASES_ARR <<< "${PERF_CASES}"for c in "${CASES_ARR[@]}"; doc_trim="$(echo "${c}" | xargs)"if [ -z "${c_trim}" ]; thencontinueficase "${c_trim}" inlinear) norm="search-linear" ;;bloom) norm="search-bloom" ;;*) norm="${c_trim}" ;;esacrun_one "${RUN_LABEL}-${norm}" --case "${norm}"doneelserun_one "${RUN_LABEL}"fiecho "Done."
#!/bin/bashset -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 2000ITERATIONS="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 Nscripts/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 ]; docase "$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)usageexit 0;;*)if [[ "$1" =~ ^[0-9]+$ ]] && [ "$iter_set" = "0" ]; thenITERATIONS="$1"iter_set="1"shiftelseecho "Error: unknown argument '$1'"usageexit 1fi;;esacdoneif [ -n "$case_list" ]; thencase_list="${case_list%,}"if [ -n "$PERF_CASES" ]; thenPERF_CASES="${PERF_CASES},${case_list}"elsePERF_CASES="${case_list}"fifiBENCH_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}" ]; thenecho "Perf cases: ${PERF_CASES}"fiecho "Bench exe: ${BENCH_EXE}"echo "Results: ${DATE_DIR}"# 1. Build benchecho "Building benchmark..."lake build benchif [ ! -x "${BENCH_EXE}" ]; thenecho "Error: bench executable not found at ${BENCH_EXE}"exit 1fi# 2. Check for perfif ! command -v perf &> /dev/null; thenecho "Error: 'perf' command not found. Please install perf."exit 1fi# 3. Prepare output directoriesmkdir -p "${REPORT_DIR}" "${FLAME_DIR}"# 4. Run perf record against the bench binary (no lake exec overhead)run_one () {local label="$1"shiftlocal -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; }; thenecho "Generating flamegraph (${label})..."if [ -x "${STACKCOLLAPSE_BIN}" ] && [ -x "${FLAMEGRAPH_BIN}" ]; thenperf script -i "${data}" | "${STACKCOLLAPSE_BIN}" > "${folded}""${FLAMEGRAPH_BIN}" "${folded}" > "${svg}"elseperf script -i "${data}" | stackcollapse-perf.pl > "${folded}"flamegraph.pl "${folded}" > "${svg}"fielseecho "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}" ]; thenIFS=',' read -r -a CASES_ARR <<< "${PERF_CASES}"for c in "${CASES_ARR[@]}"; doc_trim="$(echo "${c}" | xargs)"if [ -z "${c_trim}" ]; thencontinueficase "${c_trim}" inlinear) norm="search-linear" ;;bloom) norm="search-bloom" ;;*) norm="${c_trim}" ;;esacrun_one "${RUN_LABEL}-${norm}" --case "${norm}"doneelserun_one "${RUN_LABEL}"fiecho "Done."
# ScriptsThis 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 OutputAll 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.shPurpose: 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.shPurpose: 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.shPurpose: heavier profiling (perf report + optional c2c) and flamegraph.Usage examples:```bash./scripts/perf_profile.sh 10000PERF_MODE=both ./scripts/perf_profile.sh 10000PERF_MODE=c2c ./scripts/perf_profile.sh 10000```## Flamegraph ToolsBy 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`.
let newBuffers := ws.buffers.map fun b => if b.id == v.bufferId then FileBuffer.clearCache (f b) else b
let newBuffers := ws.buffers.map fun b =>if b.id == v.bufferId thenlet updated := FileBuffer.recomputeMissingEol (f b)FileBuffer.clearCache updatedelse b
{ original := bytes, addBuffers := #[], tree := PieceTree.empty, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
{ original := bytes, addBuffers := #[], tree := PieceTree.empty, bloomBuildLeafBits := buildLeafBits,undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
let tmpPt : PieceTable := { original := bytes, addBuffers := #[], tree := PieceTree.empty, undoStack := [], redoStack := [], undoStackCount := 0, redoStackCount := 0, undoLimit := 100, lastInsert := none }
let tmpPt : PieceTable := {original := bytes, addBuffers := #[], tree := PieceTree.empty, bloomBuildLeafBits := buildLeafBits,undoStack := [], redoStack := [], undoStackCount := 0, redoStackCount := 0, undoLimit := 100, lastInsert := none}
{ original := bytes, addBuffers := #[], tree := tree, undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
{ original := bytes, addBuffers := #[], tree := tree, bloomBuildLeafBits := buildLeafBits,undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none }
match node with| ViE.PieceTree.leaf pieces _ m =>let (bits, cache, order) :=if bloomIsEmpty m.bits thenleafBloomBitsWithCache pieces pt baseOffset cache order cacheMaxelse(m.bits, cache, order)if !bloomMayContain bits hashes then(none, cache, order)elselet bytes := getBytes node relStart remain ptmatch 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
let crossesBoundary := readLen > remainif !crossesBoundary && !bloomMayContain m.bits hashes then
let child := children[i]!let childLen := length childlet childEnd := offset + childLenif childEnd <= startOffset thenloop (i + 1) childEnd cache order
let bytes := getBytes t globalStart readLen ptmatch 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)elselet 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)
match searchNode child offset cache order with| (some res, cache, order) => (some res, cache, order)| (none, cache, order) => loop (i + 1) childEnd cache orderloop 0 baseOffset cache order
let child := children[i]!let childLen := length childlet childEnd := offset + childLenif childEnd <= startOffset thenloop (i + 1) childEnd cache orderelsematch searchNode child offset cache order with| (some res, cache, order) => (some res, cache, order)| (none, cache, order) => loop (i + 1) childEnd cache orderloop 0 baseOffset cache order
match node with| ViE.PieceTree.leaf pieces _ m =>let (bits, cache, order) :=if bloomIsEmpty m.bits thenleafBloomBitsWithCache pieces pt baseOffset cache order cacheMaxelse(m.bits, cache, order)if !bloomMayContain bits hashes then(none, cache, order)elselet bytes := getBytes node 0 relEnd ptmatch 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 dolet mut acc : Array (ViE.PieceTree × Nat) := #[]let mut offset := baseOffsetfor child in children doacc := acc.push (child, offset)offset := offset + length childreturn acclet 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
let crossesBoundary := globalStart < baseOffsetif !crossesBoundary && !bloomMayContain m.bits hashes then
let j := spans.size - 1 - ilet (child, childOffset) := spans[j]!if childOffset >= end0 thenloop (i + 1) cache order
let bytes := getBytes t globalStart readLen ptmatch findLastPatternInBytes bytes pattern with| some idx =>let pos := globalStart + idxif 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)elselet spans : Array (ViE.PieceTree × Nat) := Id.run dolet mut acc : Array (ViE.PieceTree × Nat) := #[]let mut offset := baseOffsetfor child in children doacc := acc.push (child, offset)offset := offset + length childreturn acclet 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)
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 orderloop 0 cache order
let j := spans.size - 1 - ilet (child, childOffset) := spans[j]!if childOffset >= end0 thenloop (i + 1) cache orderelsematch 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 orderloop 0 cache order
let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some s!"preview://{title}") content with dirty := false }
let buildLeafBits := state.config.searchBloomBuildLeafBitslet buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some s!"preview://{title}") content buildLeafBits with dirty := false }
let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some "preview://") content with dirty := false }
let buildLeafBits := s1.config.searchBloomBuildLeafBitslet buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some "preview://") content buildLeafBits with dirty := false }
let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some "preview://") content with dirty := false }
let buildLeafBits := s1.config.searchBloomBuildLeafBitslet buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some "preview://") content buildLeafBits with dirty := false }
let buf : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer id filename content
let buildLeafBits := state.config.searchBloomBuildLeafBitslet buf : FileBuffer := ViE.Buffer.fileBufferFromTextBufferWithConfig id filename content buildLeafBits
def emptyBuffer (filename : Option String) (buildLeafBits : Bool) : FileBuffer := {id := 0filename := filenamedirty := falsetable := PieceTable.fromString "" buildLeafBitsmissingEol := falsecache := { 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]! != 10let table := PieceTable.fromByteArray data buildLeafBits{id := 0filename := some filenamedirty := falsetable := tablemissingEol := missingEolcache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return emptyBuffer (some filename) true
-- Check if file ends with newline (POSIX compliance)let missingEol := data.size > 0 && data[data.size - 1]! != 10let table := PieceTable.fromByteArray datareturn {id := 0filename := some filenamedirty := falsetable := tablemissingEol := missingEolcache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return bufferFromData filename data true
return {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return emptyBuffer (some filename) true
return {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return emptyBuffer (some filename) truedef loadBufferByteArrayWithConfig (filename : String) (config : EditorConfig) : IO FileBuffer := dolet buildLeafBits := config.searchBloomBuildLeafBitstrylet path := System.FilePath.mk filenameif ← path.pathExists thenif ← path.isDir thenreturn emptyBuffer (some filename) buildLeafBitselselet data ← IO.FS.readBinFile filenamereturn bufferFromData filename data buildLeafBitselsereturn emptyBuffer (some filename) buildLeafBitscatch _ =>return emptyBuffer (some filename) buildLeafBits
return {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return emptyBuffer (some filename) true
let missingEol := data.size > 0 && data[data.size - 1]! != 10let table := PieceTable.fromByteArray datareturn {id := 0filename := some filenamedirty := falsetable := tablemissingEol := missingEolcache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return bufferFromData filename data true
return {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return emptyBuffer (some filename) truecatch _ =>return emptyBuffer (some filename) truedef loadPreviewBufferByteArrayWithConfig (filename : String) (maxBytes : Nat) (config : EditorConfig) : IO FileBuffer := dolet buildLeafBits := config.searchBloomBuildLeafBitstrylet path := System.FilePath.mk filenameif ← path.pathExists thenif ← path.isDir thenreturn emptyBuffer (some filename) buildLeafBitselselet data ← IO.FS.withFile filename IO.FS.Mode.read fun handle =>handle.read (USize.ofNat maxBytes)return bufferFromData filename data buildLeafBitselsereturn emptyBuffer (some filename) buildLeafBits
return {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
return emptyBuffer (some filename) buildLeafBits
/-- 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 := idfilename := filenamedirty := true -- Assume dirty if created from manual contenttable := tablemissingEol := false -- Defaultcache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
import ViE.Data.PieceTableimport Test.Utilsopen ViEnamespace Test.PieceTable.Searchopen Test.Utilsdef makeBoundaryTable : PieceTable :=let n := ViE.NodeCapacity + 1let startIdx := n / 2 - 1let chars := Id.run dolet mut cs := Array.replicate n 'x'cs := cs.set! startIdx 'a'cs := cs.set! (startIdx + 1) 'b'cs := cs.set! (startIdx + 2) 'c'return cslet s := String.ofList chars.toListlet bytes := s.toUTF8let pieces := (Array.range n).map fun i =>{ source := BufferSource.originalstart := ilength := 1lineBreaks := 0charCount := 1 }let tmp : PieceTable := {original := bytesaddBuffers := #[]tree := PieceTree.emptyundoStack := []redoStack := []undoStackCount := 0redoStackCount := 0undoLimit := 100lastInsert := none}let tree := PieceTree.fromPieces pieces tmp{ tmp with tree := tree }def testCrossLeafSearch : IO Unit := doIO.println "testCrossLeafSearch..."let pt := makeBoundaryTablelet n := ViE.NodeCapacity + 1let startIdx := n / 2 - 1let pattern := "abc".toUTF8let (r1, _, _) := PieceTree.searchNext pt.tree pt pattern 0 64 true (Lean.RBMap.empty) #[] 16assertEqual "searchNext bloom across leaf" (some startIdx) r1let total := pt.tree.lengthlet (r2, _, _) := PieceTree.searchPrev pt.tree pt pattern total 64 true (Lean.RBMap.empty) #[] 16assertEqual "searchPrev bloom across leaf" (some startIdx) r2def testCrossLeafSearchNearBoundary : IO Unit := doIO.println "testCrossLeafSearchNearBoundary..."let pt := makeBoundaryTablelet n := ViE.NodeCapacity + 1let startIdx := n / 2 - 1let pattern := "abc".toUTF8let startOffset := startIdx - 1let (r1, _, _) := PieceTree.searchNext pt.tree pt pattern startOffset 64 true (Lean.RBMap.empty) #[] 16assertEqual "searchNext from near boundary" (some startIdx) r1let startExclusive := startIdx + pattern.sizelet (r2, _, _) := PieceTree.searchPrev pt.tree pt pattern startExclusive 64 true (Lean.RBMap.empty) #[] 16assertEqual "searchPrev to near boundary" (some startIdx) r2def test : IO Unit := doIO.println "Starting PieceTable Search Test..."testCrossLeafSearchtestCrossLeafSearchNearBoundaryIO.println "PieceTable Search Test passed!"end Test.PieceTable.Search
import ViE.State.Configimport ViE.State.Layoutimport ViE.Data.PieceTableimport Test.Utilsopen ViEnamespace Test.MissingEolopen Test.Utilsdef testMissingEol : IO Unit := doIO.println "testMissingEol..."let s := ViE.initialStatelet s := s.updateActiveBuffer fun buffer =>{ buffer with table := PieceTable.fromString "abc\n", dirty := true }let buf := s.getActiveBufferassert "missingEol false with trailing newline" (!buf.missingEol)let len := buf.table.lengthlet s := s.updateActiveBuffer fun buffer =>{ buffer with table := buffer.table.delete (len - 1) 1 (len - 1), dirty := true }let buf2 := s.getActiveBufferassert "missingEol true after deleting newline" buf2.missingEollet s := ViE.initialStatelet s := s.updateActiveBuffer fun buffer =>{ buffer with table := PieceTable.fromString "abc", dirty := true }let buf3 := s.getActiveBufferassert "missingEol true without newline" buf3.missingEollet len2 := buf3.table.lengthlet s := s.updateActiveBuffer fun buffer =>{ buffer with table := buffer.table.insert len2 "\n" len2, dirty := true }let buf4 := s.getActiveBufferassert "missingEol false after adding newline" (!buf4.missingEol)def test : IO Unit := doIO.println "Starting MissingEol Test..."testMissingEolIO.println "MissingEol Test passed!"end Test.MissingEol
-- Scenario: Wide character insert moves cursor by display widthlet s := ViE.initialStatelet wide := Char.ofNat 0x3042 -- Hiragana A (wide)let s := s.insertChar widelet cursor := s.getCursorif cursor.col.val != 2 thenIO.println s!"[FAIL] Wide char cursor mismatch. Expected 2, got {cursor.col.val}"assert "Wide char cursor" falseelseIO.println "[PASS] Wide char cursor correct"
def makeBenchConfig : Config := {settings := ViE.defaultConfigcommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}
def makeBenchConfig (buildLeafBits : Option Bool := none) : Config :=let base := ViE.defaultConfiglet settings :=match buildLeafBits with| some v => { base with searchBloomBuildLeafBits := v }| none => base{settings := settingscommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}structure BenchOptions whereiterations : Nat := 1000render : Bool := truecases : List String := []textLines : Nat := 200lineLen : Nat := 80warmup : Nat := 0buildLeafBits : Option Bool := nonelistOnly : Bool := falsedef 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 restloop {} args/-- Simple timer helper -/def timeCase (label : String) (iterations : Nat) (f : IO Unit) : IO Unit := dolet t0 ← IO.monoMsNowflet t1 ← IO.monoMsNowlet ms := t1 - t0let opsPerSec := if ms == 0 then 0 else (iterations * 1000) / msIO.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 / 2let leftLen := lineLen / 2let rightLen := if lineLen > leftLen + needle.length then lineLen - leftLen - needle.length else 0let needleLine :=(String.ofList (List.replicate leftLen 'a')) ++needle ++(String.ofList (List.replicate rightLen 'a'))let linesArr := Id.run dolet mut arr := Array.replicate lines baseLineif mid < arr.size thenarr := arr.set! mid needleLinereturn arrString.intercalate "\n" linesArr.toList
/-- Simulate a heavy editing session. -/def runBenchmark (iterations : Nat) (render : Bool := true) : IO Unit := dolet _config := makeBenchConfig
/-- Case: Large insert workload (EditorState). -/def benchInsert (iterations : Nat) : IO Unit := do
-- 2. Random Access / Movementfor _ in [0:iterations/10] dos := s.moveCursorUp
/-- Case: Mixed small edits/movements. -/def benchEditMix (iterations : Nat) : IO Unit := dolet mut s := ViE.initialStatefor _ in [0:iterations] dos := s.insertChar 'a'
-- 3. Clipboard (Yank / Paste)IO.println "Benchmarking Clipboard..."for _ in [0:iterations/100] do
/-- Case: Clipboard (yank/paste). -/def benchClipboard (iterations : Nat) : IO Unit := dolet mut s := ViE.initialStates := s.insertChar 'x'for _ in [0:iterations/50] do
-- 4. Workgroups (New / Switch / Close)IO.println "Benchmarking Workgroups..."for i in [0:iterations/500] do
/-- Case: Workgroup churn. -/def benchWorkgroups (iterations : Nat) : IO Unit := dolet mut s := ViE.initialStatefor i in [0:iterations/200] do
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 benchmarkfor _ in [0:iterations/1000] dos := ViE.Window.splitWindow s true -- Vertical splits := ViE.Window.splitWindow s false -- Horizontal split
s := ViE.Window.splitWindow s trues := ViE.Window.splitWindow s false
-- 6. Undo / Redo stressIO.println "Benchmarking Undo/Redo..."for _ in [0:iterations/20] do
/-- Case: Undo/Redo stress. -/def benchUndoRedo (iterations : Nat) : IO Unit := dolet mut s := ViE.initialStatefor i in [0:iterations] dos := s.insertChar 'a'if i % 50 == 0 thens := s.commitEditfor _ in [0:iterations/10] do
-- 7. Render Simulation (Crucial for B+ tree traversal check)if render thenlet _ ← ViE.UI.render s
/-- Case: Search workload (PieceTable). -/def benchSearch (iterations : Nat) (useBloom : Bool) (lines lineLen : Nat) (buildLeafBits : Bool) (cacheMax : Nat) : IO Unit := dolet needle := "needle"let text := buildSearchText lines lineLen needlelet pt := PieceTable.fromString text buildLeafBitslet pattern := needle.toUTF8let mut offset := 0let mut cache : Lean.RBMap Nat ByteArray compare := Lean.RBMap.emptylet mut order : Array Nat := #[]for _ in [0:iterations] dolet (res, cache', order') := PieceTree.searchNext pt.tree pt pattern offset searchChunkSize useBloom cache order cacheMaxcache := cache'order := order'offset := match res with| some r => r + 1| none => 0/-- Case: Render workload. -/def benchRender (iterations : Nat) : IO Unit := dolet mut s := ViE.initialStatefor _ in [0:iterations/20] dos := s.insertChar 'a'let _ ← ViE.UI.render s
def availableCases : List String :=[ "insert", "edit", "clipboard", "workgroups", "windows", "undo", "search-bloom", "search-linear", "render" ]/-- Run benchmark cases. -/def runBenchmark (opts : BenchOptions) : IO Unit := dolet buildLeafBits := opts.buildLeafBits.getD ViE.defaultConfig.searchBloomBuildLeafBitslet config := makeBenchConfig (some buildLeafBits)let cacheMax := config.settings.searchBloomCacheMaxlet cases := if opts.cases.isEmpty then availableCases else opts.casesIO.println s!"Starting benchmark: iter={opts.iterations}, render={opts.render}"if opts.warmup > 0 thenIO.println s!"Warmup: {opts.warmup} iterations"for _ in [0:opts.warmup] dolet mut s := ViE.initialStates := s.insertChar 'a'let _ ← pure sfor c in cases domatch 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 thentimeCase "render" opts.iterations (benchRender opts.iterations)elseIO.println "[bench] render skipped (--no-render)"| other =>IO.println s!"[bench] Unknown case: {other}"
let iter := args[0]? |>.bind String.toNat? |>.getD 1000let 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
let opts := ViE.Benchmark.parseArgs argsif opts.listOnly thenIO.println "Available cases:"IO.println (String.intercalate ", " ViE.Benchmark.availableCases)elseViE.Benchmark.runBenchmark opts