From cae79e37bbbceb40957fd0cf96e59fcf35a0581f Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Fri, 13 Sep 2024 11:18:16 -0500
Subject: [PATCH 1/3] Build GitHub pages

---
 .github/workflows/main.yml | 21 +++++++++++++++++++++
 beginners/Makefile         | 16 +++++++++++++++-
 2 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/main.yml

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
new file mode 100644
index 0000000..e9c93cb
--- /dev/null
+++ b/.github/workflows/main.yml
@@ -0,0 +1,21 @@
+on: [push, pull_request]
+
+name: Build and Deploy
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v4
+
+    - name: Install requirements
+      run: |
+        pip install -r beginners/requirements.txt
+
+    - name: Build GitHub pages
+      run: |
+        cd beginners
+        make github
+
+    
\ No newline at end of file
diff --git a/beginners/Makefile b/beginners/Makefile
index d4bb2cb..7d2445a 100644
--- a/beginners/Makefile
+++ b/beginners/Makefile
@@ -11,8 +11,22 @@ BUILDDIR      = _build
 # Put it first so that "make" without argument is like "make help".
 help:
 	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
+	@echo ""
+	@echo "Use 'make github' to make HTML files for GitHub pages"
 
-.PHONY: help Makefile
+.PHONY: help github Makefile
+
+github:
+	@$(SPHINXBUILD) -M html "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
+	@find _build/html -name "*.html" -exec sed -i 's/_static/static/g; s/_images/images/g' {} +
+	@if [ -d "_build/html/_static" ]; then \
+		rm -rf _build/html/static; \
+		mv _build/html/_static _build/html/static; \
+	fi
+	@if [ -d "_build/html/_images" ]; then \
+		rm -rf _build/html/images; \
+		mv _build/html/_images _build/html/images; \
+	fi
 
 # Catch-all target: route all unknown targets to Sphinx using the new
 # "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).

From cf787579e837c9c653b1b14c1d285dd372db842f Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Fri, 13 Sep 2024 14:06:10 -0500
Subject: [PATCH 2/3] Deploy tutorial on the cvc5 website

---
 .github/workflows/main.yml | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index e9c93cb..8033a87 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -18,4 +18,21 @@ jobs:
         cd beginners
         make github
 
-    
\ No newline at end of file
+    - name: Deploy tutorial on the cvc5 website
+      if: (github.repository == 'cvc5/tutorials') && (github.ref == 'refs/heads/main')
+      env:
+        SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+      run: |
+        ssh-agent -a $SSH_AUTH_SOCK > /dev/null
+        ssh-add - <<< "${{ secrets.CVC5_WEBSITE_TOKEN }}"
+
+        git config --global user.email "webbot@cvc5"
+        git config --global user.name "WebBot"
+        git clone git@github.com:cvc5/cvc5.github.io.git website/
+
+        rm -r website/tutorials/beginners
+        cp -r beginners/_build/html website/tutorials/beginners
+        cd website/
+        git add tutorials/beginners
+        git commit -m "Deploy tutorials from source repo"
+        git push

From 532268e08220ab0912159633d4b6939d85543254 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Fri, 13 Sep 2024 14:59:02 -0500
Subject: [PATCH 3/3] Use cvc5-bot in GH workflow

---
 .github/workflows/main.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 8033a87..9e1b577 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -26,8 +26,8 @@ jobs:
         ssh-agent -a $SSH_AUTH_SOCK > /dev/null
         ssh-add - <<< "${{ secrets.CVC5_WEBSITE_TOKEN }}"
 
-        git config --global user.email "webbot@cvc5"
-        git config --global user.name "WebBot"
+        git config --global user.email "cvc5-bot@users.noreply.github.com"
+        git config --global user.name "cvc5-bot"
         git clone git@github.com:cvc5/cvc5.github.io.git website/
 
         rm -r website/tutorials/beginners