The integral closure of a Dedekind domain in a finite separable extension is finite #74
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
| name: Propose PR | |
| on: | |
| issue_comment: | |
| types: [created] | |
| jobs: | |
| propose_pr: | |
| if: github.event.issue.pull_request == null && contains(github.event.comment.body, 'propose') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check if the comment contains "propose #PR_NUMBER" | |
| id: check_propose | |
| env: | |
| COMMENT: ${{ github.event.comment.body }} | |
| run: | | |
| COMMENT_LOWER=$(echo "$COMMENT" | tr '[:upper:]' '[:lower:]') | |
| # Use a refined regex with [[:space:]] to match any whitespace | |
| if [[ "$COMMENT_LOWER" =~ propose[[:space:]]*(pr[[:space:]]*)?\#([0-9]+)[[:space:]]* ]]; then | |
| PR_NUMBER="${BASH_REMATCH[2]}" | |
| echo "pr_number=$PR_NUMBER" >> $GITHUB_ENV | |
| else | |
| echo "The comment does not contain a valid 'propose #PR_NUMBER' format." | |
| exit 1 | |
| fi | |
| - name: Retrieve project ID | |
| id: get_project_id | |
| run: | | |
| QUERY=$(cat <<EOF | |
| { | |
| "query": "{ repository(owner: \\"${{ github.repository_owner }}\\", name: \\"${{ github.event.repository.name }}\\") { projectsV2(first: 10) { nodes { id title } } } }" | |
| } | |
| EOF | |
| ) | |
| RESPONSE=$(curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \ | |
| -H "Content-Type: application/json" \ | |
| --data "$QUERY" https://api.github.com/graphql) | |
| PROJECT_ID=$(echo "$RESPONSE" | jq -r '.data.repository.projectsV2.nodes[] | select(.title == "FLT Project").id') | |
| if [ -z "$PROJECT_ID" ]; then | |
| echo "Error: Could not retrieve project ID" | |
| exit 1 | |
| else | |
| echo "PROJECT_ID=$PROJECT_ID" >> $GITHUB_ENV | |
| fi | |
| - name: Get issue details | |
| run: | | |
| curl -s -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | |
| https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }} > issue.json | |
| - name: Check if the commenter is assigned to the issue | |
| run: | | |
| COMMENTER="${{ github.event.comment.user.login }}" | |
| ASSIGNED=$(jq --arg user "$COMMENTER" '.assignees[]?.login | select(. == $user)' issue.json) | |
| if [ -z "$ASSIGNED" ]; then | |
| echo "not_assigned=true" >> $GITHUB_ENV | |
| else | |
| echo "not_assigned=false" >> $GITHUB_ENV | |
| fi | |
| - name: Notify the user if they are not assigned | |
| if: env.not_assigned == 'true' | |
| run: | | |
| echo "User ${{ github.event.comment.user.login }} is not assigned to this issue, exiting." | |
| exit 0 | |
| - name: Link PR to the issue | |
| if: env.not_assigned == 'false' | |
| run: | | |
| PR_NUMBER="${{ env.pr_number }}" | |
| if [ -z "$PR_NUMBER" ]; then | |
| echo "Error: PR number is not set. Exiting." | |
| exit 1 | |
| fi | |
| # Get the current PR body (ensure newlines are treated properly) | |
| PR_BODY=$(curl -s -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | |
| https://api.github.com/repos/${{ github.repository }}/pulls/${PR_NUMBER} | jq -r '.body') | |
| # Remove unnecessary carriage returns | |
| PR_BODY_CLEAN=$(echo "$PR_BODY" | sed 's/\r//g') | |
| # Append the issue closing reference | |
| NEW_PR_BODY=$(echo -e "${PR_BODY_CLEAN}\n\nCloses #${{ github.event.issue.number }}") | |
| # Prepare the JSON payload (properly escaped for newlines) | |
| PAYLOAD=$(jq -n --arg body "$NEW_PR_BODY" '{body: $body}') | |
| # Update the PR body with the properly formatted content | |
| curl -s -X PATCH -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | |
| -H "Content-Type: application/json" \ | |
| -d "$PAYLOAD" \ | |
| https://api.github.com/repos/${{ github.repository }}/pulls/${PR_NUMBER} | |
| - name: Retrieve the project ITEM_ID | |
| id: get_item_id | |
| run: | | |
| QUERY=$(cat <<EOF | |
| { | |
| "query": "{ repository(owner: \\"${{ github.repository_owner }}\\", name: \\"${{ github.event.repository.name }}\\") { issue(number: ${{ github.event.issue.number }}) { projectItems(first: 10) { nodes { id } } } } }" | |
| } | |
| EOF | |
| ) | |
| RESPONSE=$(curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \ | |
| -H "Content-Type: application/json" \ | |
| --data "$QUERY" https://api.github.com/graphql) | |
| ITEM_ID=$(echo "$RESPONSE" | jq -r '.data.repository.issue.projectItems.nodes[0].id') | |
| if [ -z "$ITEM_ID" ]; then | |
| echo "Error: Could not retrieve ITEM_ID" | |
| exit 1 | |
| else | |
| echo "ITEM_ID=$ITEM_ID" >> $GITHUB_ENV | |
| fi | |
| - name: Retrieve the project FIELD_ID for "Status" | |
| id: get_field_id | |
| run: | | |
| QUERY=$(cat <<EOF | |
| { | |
| "query": "{ node(id: \\"${{ env.PROJECT_ID }}\\") { ... on ProjectV2 { fields(first: 10) { nodes { ... on ProjectV2SingleSelectField { name id } } } } } }" | |
| } | |
| EOF | |
| ) | |
| RESPONSE=$(curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \ | |
| -H "Content-Type: application/json" \ | |
| --data "$QUERY" https://api.github.com/graphql) | |
| FIELD_ID=$(echo "$RESPONSE" | jq -r '.data.node.fields.nodes[] | select(.name == "Status").id') | |
| if [ -z "$FIELD_ID" ]; then | |
| echo "Error: Could not retrieve FIELD_ID for Status" | |
| exit 1 | |
| else | |
| echo "FIELD_ID=$FIELD_ID" >> $GITHUB_ENV | |
| fi | |
| - name: Retrieve the "In Progress" option ID | |
| id: find_in_progress_tasks_id | |
| run: | | |
| QUERY=$(cat <<EOF | |
| { | |
| "query": "{ node(id: \\"${{ env.PROJECT_ID }}\\") { ... on ProjectV2 { fields(first: 10) { nodes { ... on ProjectV2SingleSelectField { name options { id name } } } } } } }" | |
| } | |
| EOF | |
| ) | |
| RESPONSE=$(curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \ | |
| -H "Content-Type: application/json" \ | |
| --data "$QUERY" https://api.github.com/graphql) | |
| IN_PROGRESS_TASKS_ID=$(echo "$RESPONSE" | jq -r '.data.node.fields.nodes[] | select(.name == "Status") | .options[] | select(.name == "In Progress").id') | |
| if [ -z "$IN_PROGRESS_TASKS_ID" ]; then | |
| echo "Error: Could not retrieve 'In Progress' ID" | |
| exit 1 | |
| else | |
| echo "IN_PROGRESS_TASKS_ID=$IN_PROGRESS_TASKS_ID" >> $GITHUB_ENV | |
| fi | |
| - name: Move task to "In Progress" column | |
| run: | | |
| QUERY=$(cat <<EOF | |
| { | |
| "query": "mutation { updateProjectV2ItemFieldValue(input: { projectId: \\"${{ env.PROJECT_ID }}\\", itemId: \\"$ITEM_ID\\", fieldId: \\"$FIELD_ID\\", value: { singleSelectOptionId: \\"$IN_PROGRESS_TASKS_ID\\" } }) { projectV2Item { id } } }" | |
| } | |
| EOF | |
| ) | |
| curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \ | |
| -H "Content-Type: application/json" \ | |
| --data "$QUERY" \ | |
| https://api.github.com/graphql | |
| - name: Log the project card movement result | |
| run: echo "Task successfully moved to 'In Progress' column." |