Skip to content

README.md

Latest commit

 

History

History
67 lines (56 loc) · 3.39 KB

README.md

File metadata and controls

67 lines (56 loc) · 3.39 KB
Raw

Weekly whole-pool profiling

The Azure VM captures LeanPool every Monday at 02:00 UTC, using lean-source-profiler's compact source capture. The audited result replaces the public explorer and its date badge. A manual run uses the same service and publication path.

The service has no runtime timeout: a recording can take more than 24 hours. It continues after logout, retries failures after an hour, and resumes an unfinished run after reboot. A job lock prevents overlapping recordings. Each run pins the current LeanPool and profiler commits; retries keep those commits and reuse successfully captured files. Native Lake builds include every source module, including files outside project entry imports. Sources, native module setups, raw recordings and exported summaries are audited before publication. Failed coverage leaves the previous public snapshot intact.

All checkouts, recordings, temporary files and npm downloads live under /data/lean-pool-profile. Existing elan and user cache directories also resolve onto /data. The runner refuses to start with less than 30 GiB free and retains the two most recent successful recordings plus unfinished runs. Builds/captures use the repository's native options. Source timings include instrumentation and VM scheduling overhead; isolated file totals are not a parallel build duration.

Install on this VM

The VM needs elan/Lake, Node.js 20+, npm, Python 3, Git and authenticated GitHub push access to Vilin97/lean-source-profiler. The user service manager must have lingering enabled (loginctl show-user vasil -p Linger). Publishing uses GitHub Pages from that repository's main:docs directory and ordinary pushes; a racing push is retried from current main while preserving unrelated viewer changes.

From the LeanPool checkout:

cx doctor
install -d /data/lean-pool-profile/bin /data/lean-pool-profile/tmp
install -m 755 scripts/weekly-profile/run.py /data/lean-pool-profile/bin/run.py
install -m 644 scripts/weekly-profile/*.service scripts/weekly-profile/*.timer \
  ~/.config/systemd/user/
systemctl --user daemon-reload
systemctl --user enable lean-pool-source-profile-resume.service
systemctl --user enable --now lean-pool-source-profile.timer
systemctl --user start --no-block lean-pool-source-profile.service

The runner owns private checkouts under its data directory and never switches the shared development checkout. Optional environment overrides belong in /data/lean-pool-profile/environment; changing capture scope or configuration requires finishing the current run first.

Monitor or run manually

systemctl --user status lean-pool-source-profile.service
systemctl --user list-timers lean-pool-source-profile.timer
journalctl --user -u lean-pool-source-profile.service -f
cat /data/lean-pool-profile/active.json
# Once capture starts, the current recording also has progress.json and errors.json.
systemctl --user start --no-block lean-pool-source-profile.service

active.json names the run under runs/ and its current stage. Each recording contains its pinned inventory.json, raw captures, source summaries, build receipts, progress and final coverage. Successful publication adds complete.json and records the publication commit. The dataset manifest and coverage audit are public at /pool/manifest.json and /pool/coverage.json.