From 2d5ee8ba859e392fa52d7f7b3b49b8591530442b Mon Sep 17 00:00:00 2001 From: Maxime Piraux Date: Tue, 10 Oct 2023 10:19:04 +0200 Subject: [PATCH] Create inginious-push.yml --- .github/workflows/inginious-push.yml | 96 ++++++++++++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 .github/workflows/inginious-push.yml diff --git a/.github/workflows/inginious-push.yml b/.github/workflows/inginious-push.yml new file mode 100644 index 0000000..bee7a5e --- /dev/null +++ b/.github/workflows/inginious-push.yml @@ -0,0 +1,96 @@ +name: Push to INGInious +on: + push: + branches: [ "main" ] + pull_request_target: + types: + - closed + +env: + COURSE_ID: missing-semester # Put the INGInious course ID + COURSE_URL: https://dav.inginious.org/missing-semester # Put the WebDAV url of the course + REPO_COURSE_DIR: "." # Put the directory name of the root of the INGinious course in this repo + +jobs: + reset_changes: + name: Reset INGInious changes + if: github.head_ref == 'inginious-remote-changes' && github.event.pull_request.merged == false + runs-on: ubuntu-latest + environment: INGInious WebDAV + steps: + - name: Install dependencies + run: | + sudo apt update + sudo apt install -y davfs2 + - name: Mount course directory + id: mount + env: + WEBDAV_USERNAME: ${{ secrets.WEBDAV_USERNAME }} + WEBDAV_PASSWORD: ${{ secrets.WEBDAV_PASSWORD }} + run: | + mkdir /tmp/webdav + echo -e "$WEBDAV_USERNAME\n$WEBDAV_PASSWORD\n" | sudo mount -t davfs $COURSE_URL /tmp/webdav -o uid=$(id -u),gid=$(id -g) + ls -lah /tmp/webdav + echo "commit_id=$(cat /tmp/webdav/.commit_id)" >> $GITHUB_OUTPUT + - name: Checkout remote commit ID + uses: actions/checkout@v3 + with: + ref: ${{ steps.mount.outputs.commit_id }} + - name: Push using WebDAV + run: | + rsync -rv --exclude ".github" --exclude "lost+found" --exclude ".commit_id" --inplace --cvs-exclude --delete $GITHUB_WORKSPACE/$REPO_COURSE_DIR/ /tmp/webdav/ + sudo umount /tmp/webdav + push_to_inginious: + name: Push to INGInious instance + if: always() && ((github.head_ref == 'inginious-remote-changes' && github.event.pull_request.merged == false) || github.event_name == 'push') + needs: reset_changes + runs-on: ubuntu-latest + environment: INGInious WebDAV + steps: + - name: Install dependencies + run: | + sudo apt update + sudo apt install -y davfs2 + - name: Mount course directory + id: mount + env: + WEBDAV_USERNAME: ${{ secrets.WEBDAV_USERNAME }} + WEBDAV_PASSWORD: ${{ secrets.WEBDAV_PASSWORD }} + run: | + mkdir /tmp/webdav + echo -e "$WEBDAV_USERNAME\n$WEBDAV_PASSWORD\n" | sudo mount -t davfs $COURSE_URL /tmp/webdav -o uid=$(id -u),gid=$(id -g) + ls -lah /tmp/webdav + echo "commit_id=$(cat /tmp/webdav/.commit_id)" >> $GITHUB_OUTPUT + - name: Initialise remote commit ID + if: ${{ steps.mount.outputs.commit_id == '' }} + run: echo "$GITHUB_SHA" > /tmp/webdav/.commit_id + - name: Checkout remote commit ID + uses: actions/checkout@v3 + with: + ref: ${{ steps.mount.outputs.commit_id }} + - name: Copy over remote files + run: | + rm -rf $GITHUB_WORKSPACE/$REPO_COURSE_DIR/* + cp -rf /tmp/webdav/* $GITHUB_WORKSPACE/$REPO_COURSE_DIR + - name: Prepare PR with changes if any + uses: peter-evans/create-pull-request@v4 + id: create-pr + with: + commit-message: INGInious remote changes + title: "Remote changes from INGInious" + branch: inginious-remote-changes + body: "Remote changes not part of the repository. *Closing this PR without merging will reset the remote changes.*" + base: main + delete-branch: true + - name: Abort if remote changes exists + run: exit 1 + if: ${{ steps.create-pr.outputs.pull-request-number != null }} + - name: Checkout event commit + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Push using WebDAV + run: | + rsync -rv --exclude ".github" --exclude "lost+found" --exclude ".commit_id" --inplace --cvs-exclude --delete $GITHUB_WORKSPACE/$REPO_COURSE_DIR/ /tmp/webdav/ + echo "$GITHUB_SHA" > /tmp/webdav/.commit_id + sudo umount /tmp/webdav