Stats
Actions
Tags
From lean-prover
After every Edit/Write tool call, runs a bash script that suggests progressive disclosure of file contents to reduce context window usage. Executes bash, reads/writes files.
1 event · 2 hooks
Safety signals detected in this hook configuration
Where this hook configuration is defined
Defined in hooks/hooks.json
Event handlers and matchers — expand Raw Configuration for the full JSON
EditFILE_PATH=$(echo "$CLAUDE_TOOL_INPUT" | jq -r '.file_path // empty'); if [[ "$FILE_PATH" == *.lean ]] && [[ "$FILE_PATH" != *.lake/* ]]; then DIR=$(dirname "$FILE_PATH"); while [[ "$DIR" != "/" ]]; do if [[ -f "$DIR/lakefile.toml" ]]; then cd "$DIR" && BUILD=$(lake build 2>&1); SORRY=$(echo "$BUILD" | grep -c "uses .sorry." || true); ERROR=$(echo "$BUILD" | grep -c "error:" || true); if [[ $ERROR -eq 0 ]]; then echo "lake build ok — $SORRY sorry remaining"; else echo "lake build failed ($ERROR errors)"; echo "$BUILD" | grep -A 2 'error:' | head -20; fi; break; fi; DIR=$(dirname "$DIR"); done; fiWriteFILE_PATH=$(echo "$CLAUDE_TOOL_INPUT" | jq -r '.file_path // empty'); if [[ "$FILE_PATH" == *.lean ]] && [[ "$FILE_PATH" != *.lake/* ]]; then DIR=$(dirname "$FILE_PATH"); while [[ "$DIR" != "/" ]]; do if [[ -f "$DIR/lakefile.toml" ]]; then cd "$DIR" && BUILD=$(lake build 2>&1); SORRY=$(echo "$BUILD" | grep -c "uses .sorry." || true); ERROR=$(echo "$BUILD" | grep -c "error:" || true); if [[ $ERROR -eq 0 ]]; then echo "lake build ok — $SORRY sorry remaining"; else echo "lake build failed ($ERROR errors)"; echo "$BUILD" | grep -A 2 'error:' | head -20; fi; break; fi; DIR=$(dirname "$DIR"); done; finpx claudepluginhub psychquant/psychquant-claude-plugins --plugin lean-prover