Merge pull request #3 from daniel-larraz/gh-workflow

Build and deploy tutorial on the cvc5 website

.github/workflows/main.yml

@@ -0,0 +1,38 @@
+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
+
+    - 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 "[email protected]"
+        git config --global user.name "cvc5-bot"
+        git clone [email protected]: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

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).