forked from teorth/equational_theories
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge remote-tracking branch 'upstream/main' into CM_inf
- Loading branch information
Showing
97 changed files
with
197,417 additions
and
166 deletions.
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,4 @@ | ||
| equational_theories/Generated/TrivialBruteforce/theorems/Apply.lean linguist-generated | ||
| equational_theories/Generated/TrivialBruteforce/theorems/RewriteGoal.lean linguist-generated | ||
| equational_theories/Generated/TrivialBruteforce/theorems/RewriteHypothesis.lean linguist-generated | ||
| equational_theories/Generated/TrivialBruteforce/theorems/RewriteHypothesisAndGoal.lean linguist-generated |
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,128 @@ | ||
| name: Assign Issue on Claim | ||
|
|
||
| on: | ||
| issue_comment: | ||
| types: [created] | ||
|
|
||
| jobs: | ||
| claim_issue: | ||
| if: github.event.comment.body == 'claim' # This ensures the workflow only runs if the comment contains exactly 'claim' | ||
| runs-on: ubuntu-latest | ||
|
|
||
| steps: | ||
| - name: Check if this is an issue, not a pull request | ||
| id: check_issue | ||
| run: | | ||
| if [[ -n "${{ github.event.issue.pull_request }}" ]]; then | ||
| echo "This is a pull request, not an issue." | ||
| exit 0 | ||
| fi | ||
| - name: Check if issue is already assigned | ||
| id: check_assignee | ||
| run: | | ||
| ASSIGNEES_COUNT=$(echo "${{ toJson(github.event.issue.assignees) }}" | jq length) | ||
| if [ "$ASSIGNEES_COUNT" -gt 0 ]; then | ||
| echo "Issue is already assigned." | ||
| exit 0 | ||
| fi | ||
| - name: Assign the issue to the commenter | ||
| run: | | ||
| curl -X POST -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | ||
| -d '{"assignees":["${{ github.event.comment.user.login }}"]}' \ | ||
| https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }} | ||
| - name: Log the assignment result | ||
| run: echo "Issue successfully assigned to ${{ github.event.comment.user.login }}." | ||
|
|
||
| - 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 | ||
| ) | ||
| 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 | ||
| 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: \\"PVT_kwHOAAMKjM4Ao-Sa\\") { ... on ProjectV2 { fields(first: 10) { nodes { ... on ProjectV2SingleSelectField { name id } } } } } }" | ||
| } | ||
| 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 | ||
| echo "Error: Could not retrieve FIELD_ID for Status" | ||
| exit 1 | ||
| else | ||
| echo "FIELD_ID=$FIELD_ID" >> $GITHUB_ENV | ||
| fi | ||
| - name: Retrieve the "Claimed Tasks" option ID | ||
| id: find_claimed_tasks_id | ||
| run: | | ||
| QUERY=$(cat <<EOF | ||
| { | ||
| "query": "{ node(id: \\"PVT_kwHOAAMKjM4Ao-Sa\\") { ... on ProjectV2 { fields(first: 10) { nodes { ... on ProjectV2SingleSelectField { name options { id name } } } } } } }" | ||
| } | ||
| 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" | ||
| CLAIMED_TASKS_ID=$(echo "$RESPONSE" | jq -r '.data.node.fields.nodes[] | select(.name == "Status") | .options[] | select(.name == "Claimed Tasks").id') | ||
| if [ -z "$CLAIMED_TASKS_ID" ]; then | ||
| echo "Error: Could not retrieve 'Claimed Tasks' ID" | ||
| exit 1 | ||
| else | ||
| echo "CLAIMED_TASKS_ID=$CLAIMED_TASKS_ID" >> $GITHUB_ENV | ||
| fi | ||
| - name: Move task to "Claimed Tasks" column | ||
| run: | | ||
| QUERY=$(cat <<EOF | ||
| { | ||
| "query": "mutation { updateProjectV2ItemFieldValue(input: { projectId: \\"PVT_kwHOAAMKjM4Ao-Sa\\", itemId: \\"$ITEM_ID\\", fieldId: \\"$FIELD_ID\\", value: { singleSelectOptionId: \\"$CLAIMED_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 'Claimed Tasks' column." |
This file was deleted.
Oops, something went wrong.
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,140 @@ | ||
| name: Remove Assignment on Disclaim | ||
|
|
||
| on: | ||
| issue_comment: | ||
| types: [created] | ||
|
|
||
| jobs: | ||
| disclaim_issue: | ||
| if: github.event.comment.body == 'disclaim' # This ensures the workflow only runs if the comment contains exactly 'disclaim' | ||
| runs-on: ubuntu-latest | ||
|
|
||
| steps: | ||
| - name: Check if this is an issue, not a pull request | ||
| id: check_issue | ||
| run: | | ||
| if [[ -n "${{ github.event.issue.pull_request }}" ]]; then | ||
| echo "This is a pull request, not an issue." | ||
| exit 0 | ||
| fi | ||
| - name: Get issue details | ||
| id: 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 | ||
| continue-on-error: true | ||
|
|
||
| - 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) | ||
| if [ -z "$ASSIGNED" ]; then | ||
| echo "not_assigned=true" >> $GITHUB_ENV | ||
| else | ||
| echo "not_assigned=false" >> $GITHUB_ENV | ||
| fi | ||
| - name: Remove the user from the assignees | ||
| if: env.not_assigned == 'false' | ||
| run: | | ||
| curl -X DELETE -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | ||
| -d '{"assignees":["${{ github.event.comment.user.login }}"]}' \ | ||
| https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/assignees | ||
| - name: Log the unassignment result | ||
| if: env.not_assigned == 'false' | ||
| run: echo "User ${{ github.event.comment.user.login }} has been unassigned from the issue." | ||
|
|
||
| - 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 | ||
| ) | ||
| 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 | ||
| 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: \\"PVT_kwHOAAMKjM4Ao-Sa\\") { ... on ProjectV2 { fields(first: 10) { nodes { ... on ProjectV2SingleSelectField { name id } ... on ProjectV2IterationField { name id } } } } } }" | ||
| } | ||
| 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 | ||
| echo "Error: Could not retrieve FIELD_ID for Status" | ||
| exit 1 | ||
| else | ||
| echo "FIELD_ID=$FIELD_ID" >> $GITHUB_ENV | ||
| fi | ||
| - name: Retrieve the "Unclaimed Outstanding Tasks" option ID | ||
| id: find_unclaimed_tasks_id | ||
| run: | | ||
| QUERY=$(cat <<EOF | ||
| { | ||
| "query": "{ node(id: \\"PVT_kwHOAAMKjM4Ao-Sa\\") { ... on ProjectV2 { fields(first: 10) { nodes { ... on ProjectV2SingleSelectField { name options { id name } } } } } } }" | ||
| } | ||
| 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" | ||
| UNCLAIMED_TASKS_ID=$(echo "$RESPONSE" | jq -r '.data.node.fields.nodes[] | select(.name == "Status") | .options[] | select(.name == "Unclaimed Outstanding Tasks").id') | ||
| if [ -z "$UNCLAIMED_TASKS_ID" ]; then | ||
| echo "Error: Could not retrieve 'Unclaimed Outstanding Tasks' ID" | ||
| exit 1 | ||
| else | ||
| echo "UNCLAIMED_TASKS_ID=$UNCLAIMED_TASKS_ID" >> $GITHUB_ENV | ||
| fi | ||
| - name: Move task to "Unclaimed Outstanding Tasks" column | ||
| run: | | ||
| QUERY=$(cat <<EOF | ||
| { | ||
| "query": "mutation { updateProjectV2ItemFieldValue(input: { projectId: \\"PVT_kwHOAAMKjM4Ao-Sa\\", itemId: \\"$ITEM_ID\\", fieldId: \\"$FIELD_ID\\", value: { singleSelectOptionId: \\"$UNCLAIMED_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 'Unclaimed Outstanding Tasks' column." |
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.