From c493a81ec6126751b24717fde18c4d7be3f23fb3 Mon Sep 17 00:00:00 2001 From: "Prof. Lorenz" Date: Thu, 16 May 2024 17:00:41 +0300 Subject: [PATCH 1/9] Create jekyll-gh-pages.yml --- .github/workflows/jekyll-gh-pages.yml | 51 +++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 .github/workflows/jekyll-gh-pages.yml diff --git a/.github/workflows/jekyll-gh-pages.yml b/.github/workflows/jekyll-gh-pages.yml new file mode 100644 index 0000000..0ebd768 --- /dev/null +++ b/.github/workflows/jekyll-gh-pages.yml @@ -0,0 +1,51 @@ +# Sample workflow for building and deploying a Jekyll site to GitHub Pages +name: Deploy Jekyll with GitHub Pages dependencies preinstalled + +on: + # Runs on pushes targeting the default branch + push: + branches: ["master"] + + # Allows you to run this workflow manually from the Actions tab + workflow_dispatch: + +# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages +permissions: + contents: read + pages: write + id-token: write + +# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. +# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. +concurrency: + group: "pages" + cancel-in-progress: false + +jobs: + # Build job + build: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + - name: Setup Pages + uses: actions/configure-pages@v5 + - name: Build with Jekyll + uses: actions/jekyll-build-pages@v1 + with: + source: ./ + destination: ./_site + - name: Upload artifact + uses: actions/upload-pages-artifact@v3 + + # Deployment job + deploy: + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + runs-on: ubuntu-latest + needs: build + steps: + - name: Deploy to GitHub Pages + id: deployment + uses: actions/deploy-pages@v4 From cd7ad4030779f2892c4910d978d9fc97d02021da Mon Sep 17 00:00:00 2001 From: "D. H. Lorenz" Date: Thu, 16 May 2024 17:12:25 +0300 Subject: [PATCH 2/9] index --- index.html | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 index.html diff --git a/index.html b/index.html new file mode 100644 index 0000000..0097cce --- /dev/null +++ b/index.html @@ -0,0 +1,7 @@ + + + +

Hello World

+

I'm hosted with GitHub Pages.

+ + From 8d20bc2df0cf815c8ba7006086096d3f531bc9c7 Mon Sep 17 00:00:00 2001 From: "D. H. Lorenz" Date: Thu, 16 May 2024 21:31:02 +0300 Subject: [PATCH 3/9] _config --- _config.yml | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 _config.yml diff --git a/_config.yml b/_config.yml new file mode 100644 index 0000000..12a5e20 --- /dev/null +++ b/_config.yml @@ -0,0 +1,13 @@ +title: PL +description: 236319 Spring 2023, Prof. Lorenz +show_downloads: false +google_analytics: +theme: jekyll-theme-tactile +plugins: + - jekyll-relative-links +relative_links: + enabled: true + collections: true +include: + - README.md +notheme: jekyll-theme-cayman From 6de0532bf9949479cba1ad3bd241741a94cdd825 Mon Sep 17 00:00:00 2001 From: "Prof. Lorenz" Date: Thu, 16 May 2024 21:36:54 +0300 Subject: [PATCH 4/9] Create jekyll-docker.yml --- .github/workflows/jekyll-docker.yml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 .github/workflows/jekyll-docker.yml diff --git a/.github/workflows/jekyll-docker.yml b/.github/workflows/jekyll-docker.yml new file mode 100644 index 0000000..60e5736 --- /dev/null +++ b/.github/workflows/jekyll-docker.yml @@ -0,0 +1,20 @@ +name: Jekyll site CI + +on: + push: + branches: [ "master" ] + pull_request: + branches: [ "master" ] + +jobs: + build: + + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - name: Build the site in the jekyll/builder container + run: | + docker run \ + -v ${{ github.workspace }}:/srv/jekyll -v ${{ github.workspace }}/_site:/srv/jekyll/_site \ + jekyll/builder:latest /bin/bash -c "chmod -R 777 /srv/jekyll && jekyll build --future" From afa67de80720fb568b571dd617a284b8a9b21390 Mon Sep 17 00:00:00 2001 From: "D. H. Lorenz" Date: Thu, 16 May 2024 22:02:42 +0300 Subject: [PATCH 5/9] layout --- _config.yml | 2 +- _includes/footer.html | 1 + _layouts/default.html | 53 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 55 insertions(+), 1 deletion(-) create mode 100644 _includes/footer.html create mode 100644 _layouts/default.html diff --git a/_config.yml b/_config.yml index 12a5e20..37a4ac4 100644 --- a/_config.yml +++ b/_config.yml @@ -1,5 +1,5 @@ title: PL -description: 236319 Spring 2023, Prof. Lorenz +description: 236319 Spring 202x, Prof. Lorenz show_downloads: false google_analytics: theme: jekyll-theme-tactile diff --git a/_includes/footer.html b/_includes/footer.html new file mode 100644 index 0000000..4b9f729 --- /dev/null +++ b/_includes/footer.html @@ -0,0 +1 @@ +D. H. Lorenz diff --git a/_layouts/default.html b/_layouts/default.html new file mode 100644 index 0000000..f6a52c7 --- /dev/null +++ b/_layouts/default.html @@ -0,0 +1,53 @@ + + + + + + + + + + +{% seo %} + {% include head-custom.html %} + + + +
+
+ +
+

{{ page.title | default: site.title | default: site.github.repository_name }}

+

{{ page.description | default: site.description | default: site.github.project_tagline }}

+
+
+ {% if site.show_downloads %} + Download .zip + Download .tar.gz + {% endif %} + {% if site.github.public %} + {% if site.github.is_project_page %} + View on GitHub + {% else %} + View on GitHub + {% endif %} + {% endif %} +
+
+
+ {{ content }} +
+ +
+ {% if site.github.is_project_page %} + {{ site.title | default: site.github.repository_name }} is maintained by {{ site.github.owner_name }}
+ {% endif %} + This page was generated for 236319 Spr 2023. +
+ +
+
+ + From a3630ac5166a53dee9c8396bf3441ff9af913e66 Mon Sep 17 00:00:00 2001 From: "D. H. Lorenz" Date: Sat, 18 May 2024 14:00:24 +0300 Subject: [PATCH 6/9] workflow --- .github/workflows/{jekyll-gh-pages.yml => jekyll-pages.yml} | 1 - 1 file changed, 1 deletion(-) rename .github/workflows/{jekyll-gh-pages.yml => jekyll-pages.yml} (94%) diff --git a/.github/workflows/jekyll-gh-pages.yml b/.github/workflows/jekyll-pages.yml similarity index 94% rename from .github/workflows/jekyll-gh-pages.yml rename to .github/workflows/jekyll-pages.yml index 0ebd768..f55b307 100644 --- a/.github/workflows/jekyll-gh-pages.yml +++ b/.github/workflows/jekyll-pages.yml @@ -1,4 +1,3 @@ -# Sample workflow for building and deploying a Jekyll site to GitHub Pages name: Deploy Jekyll with GitHub Pages dependencies preinstalled on: From af86e74a0f80e942d1141b9760a374885134e246 Mon Sep 17 00:00:00 2001 From: "D. H. Lorenz" Date: Sat, 18 May 2024 14:01:27 +0300 Subject: [PATCH 7/9] docker --- .github/workflows/jekyll-docker.yml | 20 -------------------- 1 file changed, 20 deletions(-) delete mode 100644 .github/workflows/jekyll-docker.yml diff --git a/.github/workflows/jekyll-docker.yml b/.github/workflows/jekyll-docker.yml deleted file mode 100644 index 60e5736..0000000 --- a/.github/workflows/jekyll-docker.yml +++ /dev/null @@ -1,20 +0,0 @@ -name: Jekyll site CI - -on: - push: - branches: [ "master" ] - pull_request: - branches: [ "master" ] - -jobs: - build: - - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v4 - - name: Build the site in the jekyll/builder container - run: | - docker run \ - -v ${{ github.workspace }}:/srv/jekyll -v ${{ github.workspace }}/_site:/srv/jekyll/_site \ - jekyll/builder:latest /bin/bash -c "chmod -R 777 /srv/jekyll && jekyll build --future" From edad33f5fbd7a1099f4af20fb9e9363a5f38d5a4 Mon Sep 17 00:00:00 2001 From: "D. H. Lorenz" Date: Sat, 18 May 2024 14:12:32 +0300 Subject: [PATCH 8/9] error --- Material/Tutorials/sml/errors.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Material/Tutorials/sml/errors.md b/Material/Tutorials/sml/errors.md index b7ae8b0..fc78fe6 100644 --- a/Material/Tutorials/sml/errors.md +++ b/Material/Tutorials/sml/errors.md @@ -103,7 +103,7 @@ fun f (a:{s: int, r: int}) = {s: (#s a), r: (#r a)}; ``` -NOTE: `:` denotes type, we need to use `=` in the returned expression to denote a value. another common error: `{{(#s a), (#r a)}` +NOTE: `:` denotes type, we need to use `=` in the returned expression to denote a value. another common error: `{(#s a), (#r a)}` From 13ea840ae3feecdad86dc18b86f69164af554947 Mon Sep 17 00:00:00 2001 From: "D. H. Lorenz" Date: Sat, 18 May 2024 14:17:24 +0300 Subject: [PATCH 9/9] ind --- index.html | 7 ------- 1 file changed, 7 deletions(-) delete mode 100644 index.html diff --git a/index.html b/index.html deleted file mode 100644 index 0097cce..0000000 --- a/index.html +++ /dev/null @@ -1,7 +0,0 @@ - - - -

Hello World

-

I'm hosted with GitHub Pages.

- -