Merge branch 'main' into main

teorth · Oct 10, 2024 · 367b0bc · 367b0bc
2 parents 4679e76 + e430d8d
commit 367b0bc
Show file tree

Hide file tree

Showing 4 changed files with 45 additions and 171 deletions.
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
diff --git a/.github/workflows/03-propose-pr.yml b/.github/workflows/03-propose-pr.yml
@@ -26,14 +26,11 @@ jobs:
         fi
 
     - name: Get issue details
-      id: get_issue
       run: |
         curl -s -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
         https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }} > issue.json
-        cat issue.json
 
     - name: Check if the commenter is assigned to the issue
-      id: check_assignee
       run: |
         COMMENTER="${{ github.event.comment.user.login }}"
         ASSIGNED=$(jq --arg user "$COMMENTER" '.assignees[]?.login | select(. == $user)' issue.json)
@@ -52,30 +49,22 @@ jobs:
     - name: Link PR to the issue
       if: env.not_assigned == 'false'
       run: |
-        # Capture the PR number from the environment variable
         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
         PR_BODY=$(curl -s -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
           https://api.github.com/repos/${{ github.repository }}/pulls/${PR_NUMBER} | jq -r '.body')
 
-        # Add the issue reference to the PR body (to close the issue when the PR is merged)
         NEW_PR_BODY="$PR_BODY\n\nCloses #${{ github.event.issue.number }}"
 
-        # Update the PR body
-        curl -X PATCH -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
+        curl -s -X PATCH -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
+        -H "Content-Type: application/json" \
         -d "{\"body\": \"$NEW_PR_BODY\"}" \
         https://api.github.com/repos/${{ github.repository }}/pulls/${PR_NUMBER}
 
-    - name: Log PR and issue link result
-      if: env.not_assigned == 'false'
-      run: echo "PR ${{ env.pr_number }} has been successfully linked to issue ${{ github.event.issue.number }}."
-
     - name: Retrieve the project ITEM_ID
       id: get_item_id
       run: |
@@ -85,13 +74,11 @@ jobs:
         }
         EOF
         )
-        echo "Sending query: $QUERY"
 
         RESPONSE=$(curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \
           -H "Content-Type: application/json" \
           --data "$QUERY" https://api.github.com/graphql)
 
-        echo "GraphQL Response: $RESPONSE"
         ITEM_ID=$(echo "$RESPONSE" | jq -r '.data.repository.issue.projectItems.nodes[0].id')
 
         if [ -z "$ITEM_ID" ]; then
@@ -110,13 +97,11 @@ jobs:
         }
         EOF
         )
-        echo "Sending query: $QUERY"
 
         RESPONSE=$(curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \
           -H "Content-Type: application/json" \
           --data "$QUERY" https://api.github.com/graphql)
 
-        echo "GraphQL Response: $RESPONSE"
         FIELD_ID=$(echo "$RESPONSE" | jq -r '.data.node.fields.nodes[] | select(.name == "Status").id')
 
         if [ -z "$FIELD_ID" ]; then
@@ -135,13 +120,11 @@ jobs:
         }
         EOF
         )
-        echo "Sending query: $QUERY"
 
         RESPONSE=$(curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \
           -H "Content-Type: application/json" \
           --data "$QUERY" https://api.github.com/graphql)
 
-        echo "GraphQL Response: $RESPONSE"
         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
@@ -159,6 +142,7 @@ jobs:
         }
         EOF
         )
+
         curl -X POST -H "Authorization: Bearer ${{ secrets.PAT_TOKEN }}" \
         -H "Content-Type: application/json" \
         --data "$QUERY" \

diff --git a/equational_theories/Equations/Basic.lean b/equational_theories/Equations/Basic.lean
@@ -9,7 +9,7 @@ viewed and edited, without having to open a very large file.
 
 See `Equations/All.lean` for the remaining ones. Feel free to move individual equations here if
 you do manual proofs about them and you want to import just this file. But don't forget to comment
-out the corresponding copy of the equatoins in `Equations/All.lean` if you do so?
+out the corresponding copy of the equations in `Equations/All.lean` if you do so?
 
 The equations are marked as `abbrev` so that tactics like `decide` will look through the definition.
 -/