Merge branch 'sync-20240201' into sync-priv-20240201

This commit is contained in:
Jason Wen
2024-02-07 13:48:45 -05:00
816 changed files with 23928 additions and 20061 deletions
+1 -1
View File
@@ -8,4 +8,4 @@ fi
BASE="https://github.com/commaai/openpilot/pull/"
PR_NUM="$(echo $1 | grep -o -E '[0-9]+')"
curl -L $BASE/$PR_NUM.patch | git apply
curl -L $BASE/$PR_NUM.patch | git apply -3
+39
View File
@@ -0,0 +1,39 @@
#!/bin/bash
set -ex
DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >/dev/null && pwd)"
cd $DIR
# git clone --mirror
SRC=/tmp/openpilot.git/
OUT=/tmp/smallpilot/
echo "starting size $(du -hs .git/)"
rm -rf $OUT
cd $SRC
git remote update
# copy contents
#rsync -a --exclude='.git/' $DIR $OUT
cp -r $SRC $OUT
cd $OUT
# remove all tags
git tag -l | xargs git tag -d
# remove non-master branches
BRANCHES="release2 release3 devel master-ci nightly"
for branch in $BRANCHES; do
git branch -D $branch
git branch -D ${branch}-staging || true
done
#git gc
git reflog expire --expire=now --all
git gc --prune=now
git gc --aggressive --prune=now
echo "new one is $(du -hs .)"
+16
View File
@@ -0,0 +1,16 @@
#!/bin/bash
set -e
if [ $# -eq 0 ]; then
echo "usage: $0 <pull-request-number>"
exit 1
fi
BASE="https://github.com/commaai/openpilot/pull/"
PR_NUM="$(echo $1 | grep -o -E '[0-9]+')"
BRANCH=tmp-pr${PR_NUM}
git branch -D -f $BRANCH || true
git fetch -u -f origin pull/$PR_NUM/head:$BRANCH
git switch $BRANCH
git reset --hard FETCH_HEAD
+1 -1
View File
@@ -13,7 +13,7 @@ for d in ["cereal", "common", "scripts", "selfdrive", "tools"]:
if f.endswith(".py"):
pyf.append(os.path.join(root, f))
imps = set()
imps: set[str] = set()
class Analyzer(ast.NodeVisitor):
def visit_Import(self, node):
+27
View File
@@ -0,0 +1,27 @@
#!/bin/bash
function fail {
echo $1 >&2
exit 1
}
function retry {
local n=1
local max=3 # 3 retries before failure
local delay=5 # delay between retries, 5 seconds
while true; do
echo "Running command '$@' with retry, attempt $n/$max"
"$@" && break || {
if [[ $n -lt $max ]]; then
((n++))
sleep $delay;
else
fail "The command has failed after $n attempts."
fi
}
done
}
if [[ "${BASH_SOURCE[0]}" == "${0}" ]]; then
retry "$@"
fi