Skip to content

Commit

Permalink
Merge pull request #89 from hpsim/dev
Browse files Browse the repository at this point in the history
Version 0.4 release
  • Loading branch information
greole authored Jul 12, 2023
2 parents 916b020 + e97799d commit 71e0fc2
Show file tree
Hide file tree
Showing 51 changed files with 3,600 additions and 1,799 deletions.
22 changes: 22 additions & 0 deletions .github/bot-base.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
#!/usr/bin/env bash

set -e

API_HEADER="Accept: application/vnd.github.v3+json"
AUTH_HEADER="Authorization: token $GITHUB_TOKEN"

api_get() {
curl -X GET -s -H "${AUTH_HEADER}" -H "${API_HEADER}" "$1"
}

api_post() {
curl -X POST -s -H "${AUTH_HEADER}" -H "${API_HEADER}" "$1" -d "$2"
}

api_patch() {
curl -X PATCH -s -H "${AUTH_HEADER}" -H "${API_HEADER}" "$1" -d "$2"
}

api_delete() {
curl -X DELETE -s -H "${AUTH_HEADER}" -H "${API_HEADER}" "$1"
}
102 changes: 102 additions & 0 deletions .github/bot-pr-base.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,102 @@
#!/usr/bin/env bash

source .github/bot-base.sh

echo -n "Collecting information on triggering PR"
PR_URL=$(jq -r .pull_request.url "$GITHUB_EVENT_PATH")
if [[ "$PR_URL" == "null" ]]; then
# if this was triggered by an issue comment: get PR and commenter
echo -n .............
PR_URL=$(jq -er .issue.pull_request.url "$GITHUB_EVENT_PATH")
echo -n .
USER_LOGIN=$(jq -er ".comment.user.login" "$GITHUB_EVENT_PATH")
echo -n .
USER_URL=$(jq -er ".comment.user.url" "$GITHUB_EVENT_PATH")
echo -n .
else
# else it was triggered by a PR sync: get PR creator
USER_LOGIN=$(jq -er ".pull_request.user.login" "$GITHUB_EVENT_PATH")
echo -n .
USER_URL=$(jq -er ".pull_request.user.url" "$GITHUB_EVENT_PATH")
echo -n .
fi
echo -n .
PR_JSON=$(api_get $PR_URL)
echo -n .
PR_MERGED=$(echo "$PR_JSON" | jq -r .merged)
echo -n .
PR_NUMBER=$(echo "$PR_JSON" | jq -r .number)
echo -n .
ISSUE_URL=$(echo "$PR_JSON" | jq -er ".issue_url")
echo -n .
BASE_REPO=$(echo "$PR_JSON" | jq -er .base.repo.full_name)
echo -n .
BASE_BRANCH=$(echo "$PR_JSON" | jq -er .base.ref)
echo -n .
HEAD_REPO=$(echo "$PR_JSON" | jq -er .head.repo.full_name)
echo -n .
HEAD_BRANCH=$(echo "$PR_JSON" | jq -er .head.ref)
echo .

BASE_URL="https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/$BASE_REPO"
HEAD_URL="https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/$HEAD_REPO"

JOB_URL="https://github.com/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"

bot_delete_comments_matching() {
local search_matching="$1"
COMMENTS=$(api_get "$ISSUE_URL/comments" | jq -r '.[] | select((.user.login == "peterBot") and (.body | startswith('"\"$search_matching\""'))) | .url')
for URL in $COMMENTS; do
api_delete "$URL" > /dev/null
done
}

bot_comment() {
api_post "$ISSUE_URL/comments" "{\"body\":\"$1\"}" > /dev/null
}

bot_error() {
echo "$1"
bot_comment "Error: $1"
exit 1
}

bot_get_all_changed_files() {
local pr_url="$1"
local pr_files=""
local page="1"
while true; do
# this api allows 100 items per page
# github action uses `bash -e`. The last empty page will leads jq error, use `|| :` to ignore the error.
local pr_page_files=$(api_get "$pr_url/files?&per_page=100&page=${page}" | jq -er '.[] | select(.status != "removed") | .filename' || :)
if [ "${pr_page_files}" = "" ]; then
break
fi
if [ ! "${pr_files}" = "" ]; then
# add the same new line format as jq output
pr_files="${pr_files}"$'\n'
fi
pr_files="${pr_files}${pr_page_files}"
page=$(( page + 1 ))
done
echo "${pr_files}"
}

# collect info on the user that invoked the bot
echo -n "Collecting information on triggering user"
USER_JSON=$(api_get $USER_URL)
echo .

USER_NAME=$(echo "$USER_JSON" | jq -r ".name")
if [[ "$USER_NAME" == "null" ]]; then
USER_NAME=$USER_LOGIN
fi
USER_EMAIL=$(echo "$USER_JSON" | jq -r ".email")
if [[ "$USER_EMAIL" == "null" ]]; then
USER_EMAIL="$USER_LOGIN@users.noreply.github.com"
fi
USER_COMBINED="$USER_NAME <$USER_EMAIL>"

if [[ "$PR_MERGED" == "true" ]]; then
bot_error "PR already merged!"
fi
20 changes: 20 additions & 0 deletions .github/bot-pr-format-base.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
#!/usr/bin/env bash

source .github/bot-pr-base.sh

echo "Retrieving PR file list"
PR_FILES=$(bot_get_all_changed_files ${PR_URL})
NUM=$(echo "${PR_FILES}" | wc -l)
echo "PR has ${NUM} changed files"

TO_FORMAT="$(echo "$PR_FILES" | grep -E $EXTENSION_REGEX || true)"

git remote add fork "$HEAD_URL"
git fetch fork "$HEAD_BRANCH"

git config user.email "[email protected]"
git config user.name "OGLBot"

# checkout current PR head
LOCAL_BRANCH=format-tmp-$HEAD_BRANCH
git checkout -b $LOCAL_BRANCH fork/$HEAD_BRANCH
21 changes: 21 additions & 0 deletions .github/format.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
#!/usr/bin/env bash

cp .github/bot-pr-format-base.sh /tmp
source /tmp/bot-pr-format-base.sh

echo "listing files"
# check for changed files, replace newlines by \n
LIST_FILES=$(git diff --name-only | sed '$!s/$/\\n/' | tr -d '\n')

# format files
clang-format -i $LIST_FILES

echo $LIST_FILES
echo "gonna commit files"
# commit changes if necessary
if [[ "$LIST_FILES" != "" ]]; then
git commit -a -m "Format files
Co-authored-by: $USER_COMBINED"
git push fork "$LOCAL_BRANCH:$HEAD_BRANCH" 2>&1 || bot_error "Cannot push formatted branch, are edits for maintainers allowed?"
fi
149 changes: 0 additions & 149 deletions .github/workflows/build-esi.yml

This file was deleted.

Loading

0 comments on commit 71e0fc2

Please sign in to comment.