introduce model_info type annotation #15
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Commits 0 Open PRs 1 Open PR 2 Open PRs | |
# ------------------------------------------- ---------------------------------------------------- ------------------------------------------------------------------------------------------------------- --------------------------------------------------------- | |
# Neither ahead or behind Nothing Dismiss PRs Dismiss PRs | |
# `documentation-gitbook` is behind Open A PR from `main` into `documentation-gitbook` Determine the directionality, if wrong dismiss and open a PR from `main` into `documentation-gitbook` Dismiss the PR from `documentation-gitbook` into `main` | |
# `documentation-gitbook` is behind Open A PR from `documentation-gitbook` into `main` Determine the directionality, if wrong dismiss and open a PR from `documentation-gitbook` into `main` Dismiss the PR from `main` into `documentation-gitbook` | |
# `documentation-gitbook` is ahead & behind Open 2 PRs Determine the directionality of the missing one and open that Nothing | |
name: Create GitBook Sync PRs | |
on: | |
workflow_dispatch: | |
pull_request: | |
types: | |
- closed | |
push: | |
branches: | |
- documentation-gitbook | |
paths: | |
- documentation/** | |
jobs: | |
create-prs: | |
runs-on: ubuntu-latest | |
if: github.event_name != 'pull_request' || (github.event.pull_request.merged == true && (github.event.pull_request.base.ref == 'main' || github.event.pull_request.base.ref == 'documentation-gitbook')) | |
env: | |
DOCS_BRANCH: documentation-gitbook | |
PR_LABELS: 'documentation,high priority' | |
PR_REVIEWERS: 'alsnhll,jcblemai,MacdonaldJoshuaCaleb,saraloo,shauntruelove,twallema' | |
PR_TITLE: 'Sync GitBook' | |
OWNER: 'HopkinsIDD' | |
REPO: 'flepiMoP' | |
steps: | |
- name: Checkout | |
uses: actions/checkout@v4 | |
with: | |
lfs: true | |
fetch-depth: 0 | |
- name: Determine Commits Ahead/Behind | |
run: | | |
git fetch --all | |
DOCS_AHEAD_MAIN=$( eval "git rev-list --count origin/main..origin/$DOCS_BRANCH -- documentation/" ) | |
DOCS_BEHIND_MAIN=$( eval "git rev-list --count origin/$DOCS_BRANCH..origin/main -- documentation/" ) | |
echo "DOCS_AHEAD_MAIN=$DOCS_AHEAD_MAIN" >> $GITHUB_ENV | |
echo "DOCS_BEHIND_MAIN=$DOCS_BEHIND_MAIN" >> $GITHUB_ENV | |
- name: Create PR If Needed | |
uses: actions/github-script@v7 | |
id: create-pr | |
with: | |
result-encoding: string | |
retries: 5 | |
script: | | |
const { DOCS_AHEAD_MAIN, DOCS_BEHIND_MAIN, DOCS_BRANCH, PR_LABELS, PR_REVIEWERS, PR_TITLE, OWNER, REPO } = process.env | |
const prLabels = PR_LABELS.split(",") | |
const prReviewers = PR_REVIEWERS.split(",") | |
const cc = prReviewers.map(x => "@" + x).join(", ") | |
const docsAheadMain = parseInt(DOCS_AHEAD_MAIN, 10) | |
const docsBehindMain = parseInt(DOCS_BEHIND_MAIN, 10) | |
if (isNaN(docsAheadMain) || isNaN(docsBehindMain)) { | |
throw new Error(`Cannot convert either "${DOCS_AHEAD_MAIN}" or "${DOCS_BEHIND_MAIN}" to integers.`) | |
} | |
const initialResults = await github.rest.search.issuesAndPullRequests({ | |
q: `repo:${OWNER}/${REPO} is:open is:pr in:title '${PR_TITLE}'` | |
}) | |
const count = initialResults.data.total_count | |
if (count > 2) { | |
throw new Error(`There are ${count} open PRs containing '${PR_TITLE}', but this action can only handle 0, 1, or 2 open PRs.`) | |
} | |
console.log(`${DOCS_BRANCH} is ${docsAheadMain} ahead, ${docsBehindMain} behind main. The open PR count is ${count}.`) | |
async function dismissAllPRs() { | |
initialResults.data.items.forEach((item) => { | |
github.rest.pulls.update({ | |
owner: OWNER, | |
repo: REPO, | |
pull_number: item.number, | |
state: "closed" | |
}) | |
}) | |
} | |
async function createPR({ from, to, body }) { | |
let prBody = `cc: ${cc}.` | |
if (body !== null) { | |
prBody = `${body} ${prBody}` | |
} | |
const today = (new Date()).toLocaleDateString() | |
const pr = await github.rest.pulls.create({ | |
owner: OWNER, | |
repo: REPO, | |
head: from, | |
base: to, | |
title: `${today} ${PR_TITLE} From ${from} Into ${to}`, | |
body: prBody | |
}) | |
github.rest.issues.addLabels({ | |
owner: OWNER, | |
repo: REPO, | |
issue_number: pr.data.number, | |
labels: prLabels | |
}) | |
github.rest.pulls.requestReviewers({ | |
owner: OWNER, | |
repo: REPO, | |
pull_number: pr.data.number, | |
reviewers: prReviewers | |
}) | |
return pr.data.number | |
} | |
async function handleSingleDirection({ from, to }) { | |
if (count === 0) { | |
// There isn't the 1 expected PR, open it | |
createPR({ | |
from: from, | |
to: to, | |
body: null | |
}) | |
} else if (count === 1) { | |
// There is a PR open, determine direction | |
let title = initialResults.data.items[0].title | |
if (!title.includes(`${PR_TITLE} From ${from} Into ${to}`)) { | |
// Wrong direction, close & recreate | |
dismissAllPRs() | |
createPR({ | |
from: from, | |
to: to, | |
body: null | |
}) | |
} | |
} else { | |
// There are two PRs open, close the wrong direction | |
initialResults.data.items.forEach((item) => { | |
if (!title.includes(`${PR_TITLE} From ${from} Into ${to}`)) { | |
github.rest.pulls.update({ | |
owner: OWNER, | |
repo: REPO, | |
pull_number: item.number, | |
state: "closed" | |
}) | |
} | |
}) | |
} | |
} | |
if (docsAheadMain > 0 && docsBehindMain > 0) { | |
// Need PRs both ways | |
if (count === 0) { | |
// There are 0 PRs open, open both of them | |
const docsIntoMainPrNumber = await createPR({ | |
from: DOCS_BRANCH, | |
to: "main", | |
body: null | |
}) | |
createPR({ | |
from: "main", | |
to: DOCS_BRANCH, | |
body: `Please merge GH-${docsIntoMainPrNumber} first.` | |
}) | |
} else if (count === 1) { | |
// There is already a PR open in one direction, open the other direction | |
let title = initialResults.data.items[0].title | |
let number = initialResults.data.items[0].number | |
if (title.includes(`${PR_TITLE} From ${DOCS_BRANCH} Into main`)) { | |
// From docs into main already exists, create main into docs | |
createPR({ | |
from: "main", | |
to: DOCS_BRANCH, | |
body: `Please merge GH-${number} first.` | |
}) | |
} else { | |
// From main into docs already exists, create docs into main | |
const docsIntoMainPrNumber = await createPR({ | |
from: DOCS_BRANCH, | |
to: "main", | |
body: null | |
}) | |
github.rest.issues.createComment({ | |
owner: OWNER, | |
repo: REPO, | |
issue_number: number, | |
body: `Please merge GH-${docsIntoMainPrNumber} first.` | |
}) | |
} | |
} | |
} else if (docsAheadMain > 0) { | |
// Need a PR from docs to main | |
handleSingleDirection({ | |
from: DOCS_BRANCH, | |
to: "main" | |
}) | |
} else if (docsBehindMain > 0) { | |
// Need a PR from main to docs | |
handleSingleDirection({ | |
from: "main", | |
to: DOCS_BRANCH | |
}) | |
} else if (count > 0) { | |
// Ahead/behind commits is 0 but there are stale PRs to close | |
dismissAllPRs() | |
} |