From 52459149e25cf12e6c65675a545fd1b264c9da57 Mon Sep 17 00:00:00 2001 From: Leonardo Santiago Date: Sat, 1 Jun 2024 19:01:14 -0300 Subject: add deployment workflow --- .github/workflows/hugo.yaml | 80 ++++++++++++++++++++++ blog.org | 4 +- content/_index.md | 2 +- content/about.md | 4 +- content/blog/rust-is-not-about-memory-safety.md | 4 +- public/404.html | 4 +- public/about/index.html | 16 ++--- public/blog/index.html | 14 ++-- public/blog/index.xml | 12 ++-- .../rust-is-not-about-memory-safety/index.html | 18 ++--- public/index.html | 10 +-- public/index.xml | 18 ++--- public/robots.txt | 2 +- public/sitemap.xml | 12 ++-- public/tags/correctness/index.html | 8 +-- public/tags/correctness/index.xml | 8 +-- public/tags/rust/index.html | 8 +-- public/tags/rust/index.xml | 8 +-- 18 files changed, 156 insertions(+), 76 deletions(-) create mode 100644 .github/workflows/hugo.yaml diff --git a/.github/workflows/hugo.yaml b/.github/workflows/hugo.yaml new file mode 100644 index 0000000..25b1b66 --- /dev/null +++ b/.github/workflows/hugo.yaml @@ -0,0 +1,80 @@ +# Sample workflow for building and deploying a Hugo site to GitHub Pages +name: Deploy Hugo site to Pages + +on: + # Runs on pushes targeting the default branch + push: + branches: + - main + + # 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 + +# Default to bash +defaults: + run: + shell: bash + +jobs: + # Build job + build: + runs-on: ubuntu-latest + env: + HUGO_VERSION: 0.126.0 + steps: + - name: Install Hugo CLI + run: | + wget -O ${{ runner.temp }}/hugo.deb https://github.com/gohugoio/hugo/releases/download/v${HUGO_VERSION}/hugo_extended_${HUGO_VERSION}_linux-amd64.deb \ + && sudo dpkg -i ${{ runner.temp }}/hugo.deb + - name: Install Dart Sass + run: sudo snap install dart-sass + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: recursive + fetch-depth: 0 + - name: Setup Pages + id: pages + uses: actions/configure-pages@v4 + - name: Install Node.js dependencies + run: "[[ -f package-lock.json || -f npm-shrinkwrap.json ]] && npm ci || true" + - name: Build with Hugo + env: + # For maximum backward compatibility with Hugo modules + HUGO_ENVIRONMENT: production + HUGO_ENV: production + TZ: America/Los_Angeles + run: | + hugo \ + --gc \ + --minify \ + --baseURL "${{ steps.pages.outputs.base_url }}/" + - name: Upload artifact + uses: actions/upload-pages-artifact@v3 + with: + path: ./public + + # 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 + diff --git a/blog.org b/blog.org index 5f0cfba..c1b8267 100644 --- a/blog.org +++ b/blog.org @@ -30,7 +30,7 @@ if you feel like smugly responding to any of my posts (or just want to kindly se - [[https://www.linkedin.com/in/leonardo-ribeiro-santiago/][linkedin]] - [[https://github.com/o-santi][github]] -this blog was built using emacs' excelent org-mode and [[https://github.com/gohugoio/hugo][hugo]] (with the [[https://github.com/janraasch/hugo-bearblog][bearblog theme]]). +this blog was built using emacs' excelent org-mode and [[https://github.com/gohugoio/hugo][hugo]] (with the [[https://github.com/janraasch/hugo-bearblog][bearblog theme]]), and it's source code is openly available [[https://github.com/o-santi/blog][here]]. * blog :PROPERTIES: @@ -92,7 +92,7 @@ what the regex example makes clear is that the key to correctness is to make you you, as the programmer, is then in charge of ensuring that the resulting regex program actually solves the problem you have at hands. want to match 3 words of 2 digit numbers followed by a capital letter? great, they can do that. want to match balanced parenthesized expressions? sadly, regex is incapable of ever solving that, because that language [[https://en.wikipedia.org/wiki/Pumping_lemma_for_regular_languages#Use_of_the_lemma_to_prove_non-regularity][is not regular]], so no matter how hard you try it will never solve it. -in a way, there's a beauty in how C sidesteps this: it defines one of the possible program outputs as being /undefined/, and it is on the programmers behalf to tightly ensure that the program has 0 paths to /undefined behavior/. in fact, it is probably one of the most [[https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf][well specified languages]], which is what makes it suitable for writing formally verifiable programs [fn::through the use of external tools like Coq's [[https://vst.cs.princeton.edu/veric/][verifiable C series]]]. +in a way, there's a beauty in how C sidesteps this: it defines one of the possible program outputs as being /undefined/, and it is on the programmers behalf to tightly ensure that the program has 0 paths to /undefined behavior/. in fact, it is probably one of the most [[https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf][well specified languages]], which is what makes it suitable for writing formally verifiable programs [fn::through the use of external tools like coq's [[https://vst.cs.princeton.edu/veric/][verifiable C series]]]. the main strength of rust, and where it differs from all mainstream languages, is that it has a very clear focus on program *correctness*. the raison d'être of the borrow checker is statically assuring that all references are pointing to valid memory, such that it is literally impossible for any borrow be null or to point to some freed memory (modulus [[https://github.com/Speykious/cve-rs][implementation errors of course]]). this completely rules out this possibility of bugs from the language we're trying to "parse". remember the C excerpt from above, where i said that the compiler should rule out the program as invalid? well, it is literally impossible to write that sort of program in rust, because one cannot construct a ~NULL~ reference. diff --git a/content/_index.md b/content/_index.md index a4f9a56..ff54223 100644 --- a/content/_index.md +++ b/content/_index.md @@ -2,7 +2,7 @@ title = "home" author = ["santi"] description = "a lower case only blog, purely for aesthetics" -lastmod = 2024-06-01T17:29:17-03:00 +lastmod = 2024-06-01T18:59:08-03:00 draft = false +++ diff --git a/content/about.md b/content/about.md index 5ca6f1b..d5f5fef 100644 --- a/content/about.md +++ b/content/about.md @@ -2,7 +2,7 @@ title = "about" author = ["santi"] description = "a lower case only blog, purely for aesthetics" -lastmod = 2024-06-01T17:29:17-03:00 +lastmod = 2024-06-01T18:59:08-03:00 draft = false menu = "main" +++ @@ -17,4 +17,4 @@ if you feel like smugly responding to any of my posts (or just want to kindly se - [linkedin](https://www.linkedin.com/in/leonardo-ribeiro-santiago/) - [github](https://github.com/o-santi) -this blog was built using emacs' excelent org-mode and [hugo](https://github.com/gohugoio/hugo) (with the [bearblog theme](https://github.com/janraasch/hugo-bearblog)). +this blog was built using emacs' excelent org-mode and [hugo](https://github.com/gohugoio/hugo) (with the [bearblog theme](https://github.com/janraasch/hugo-bearblog)), and it's source code is openly available [here](https://github.com/o-santi/blog). diff --git a/content/blog/rust-is-not-about-memory-safety.md b/content/blog/rust-is-not-about-memory-safety.md index e794a39..d73e4ab 100644 --- a/content/blog/rust-is-not-about-memory-safety.md +++ b/content/blog/rust-is-not-about-memory-safety.md @@ -2,7 +2,7 @@ title = "rust is not about memory safety" author = ["santi"] description = "a lower case only blog, purely for aesthetics" -lastmod = 2024-06-01T17:29:17-03:00 +lastmod = 2024-06-01T18:59:08-03:00 tags = ["rust", "correctness"] draft = false +++ @@ -91,4 +91,4 @@ i really think software developers should strive for that kind of resilience, wh [^fn:1]: formally they are defined as a sequence of tokens in certain alphabet that the automata closures over. normally we think of "words" as the whole program that we're parsing. [^fn:2]: the excellent software foundations book [explains thoroughly](https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html) how one might formally write one possible regex matcher, and prove that the implementation is correct -[^fn:3]: through the use of external tools like Coq's [verifiable C series](https://vst.cs.princeton.edu/veric/) +[^fn:3]: through the use of external tools like coq's [verifiable C series](https://vst.cs.princeton.edu/veric/) diff --git a/public/404.html b/public/404.html index 8568043..3155f08 100644 --- a/public/404.html +++ b/public/404.html @@ -1,7 +1,7 @@ - + @@ -11,7 +11,7 @@ - + diff --git a/public/about/index.html b/public/about/index.html index 44fd5dc..694346a 100644 --- a/public/about/index.html +++ b/public/about/index.html @@ -1,7 +1,7 @@ - + @@ -11,15 +11,15 @@ - + - - + + @@ -31,9 +31,9 @@ - - - + + +