brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2024-11-09 10:40:34 -05:00
Code Issues Projects Releases Packages Wiki Activity

Added medium syndication metadata

Browse source
This commit is contained in:
Brandon Rozek 2023-02-18 13:12:02 -05:00
parent 79329aae66
commit 387dd491b1
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
30 changed files with 175 additions and 134 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
content/blog/codeinbeamer.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Code in LaTex Beamer" date: 2022-01-26 23:11:37-05:00
date: 2022-01-26T23:11:37-05:00
draft: false draft: false
tags: ["LaTex"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: d91f704bb53a
tags:
- LaTex
title: Code in LaTex Beamer
--- ---
I commonly use the [`listings` package](/blog/latexcode/) to showcase code in my LaTex documents. I tried doing the same in my Beamer slidedecks and I ran into an issue where the LaTex source code failed to compile. After digging around, I figured out its because every slide or frame that includes code (or any verbatim environment) needs to be marked as `fragile`. A minimal example is presented below: I commonly use the [`listings` package](/blog/latexcode/) to showcase code in my LaTex documents. I tried doing the same in my Beamer slidedecks and I ran into an issue where the LaTex source code failed to compile. After digging around, I figured out its because every slide or frame that includes code (or any verbatim environment) needs to be marked as `fragile`. A minimal example is presented below:
@ -32,5 +34,4 @@ I commonly use the [`listings` package](/blog/latexcode/) to showcase code in my
\end{lstlisting} \end{lstlisting}
\end{frame} \end{frame}
\end{document} \end{document}
``` ```

10
content/blog/codeoutputlatex.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Code alongside Output in LaTex" date: 2022-01-27 09:15:10-05:00
date: 2022-01-27T09:15:10-05:00
draft: false draft: false
tags: ["LaTex"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: c4d061953056
tags:
- LaTex
title: Code alongside Output in LaTex
--- ---
Working on a tool paper, I had the desire to share code alongside its output. With a combination of the `listings`, `caption`, and `color` packages, we can get a result that's nice looking. Working on a tool paper, I had the desire to share code alongside its output. With a combination of the `listings`, `caption`, and `color` packages, we can get a result that's nice looking.
@ -147,4 +149,4 @@ print(factorial(5))
\end{document} \end{document}
``` ```

11
content/blog/dafny-3-3-countermodel.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Dafny v3.3 Show Countermodel" date: 2022-02-04 19:43:12-05:00
date: 2022-02-04T19:43:12-05:00
draft: false draft: false
tags: ["Formal Methods"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: b1976dcfde09
tags:
- Formal Methods
title: Dafny v3.3 Show Countermodel
--- ---
*Warning: `extractcounterexample` is a new flag in Dafny and the command to extract it will likely change* *Warning: `extractcounterexample` is a new flag in Dafny and the command to extract it will likely change*
@ -102,5 +104,4 @@ Running Dafny again will produce:
Dafny program verifier finished with 2 verified, 0 errors Dafny program verifier finished with 2 verified, 0 errors
Compiled assembly into example3.dll Compiled assembly into example3.dll
Program compiled successfully Program compiled successfully
``` ```

13
content/blog/dafny-loops.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Reasoning through Loops in Dafny" date: 2022-02-05 00:22:58-05:00
date: 2022-02-05T00:22:58-05:00
draft: false draft: false
tags: ["Formal Methods"]
math: true math: true
medium_enabled: true medium_enabled: true
medium_post_id: c0e16f8cd368
tags:
- Formal Methods
title: Reasoning through Loops in Dafny
--- ---
Dafny treats loops like a black box. It could be annoying the first time you experience this and have no clue why the code is not verifying properly. There are two properties that Dafny needs you to prove: partial correctness and termination. Together these form *total correctness*. Dafny treats loops like a black box. It could be annoying the first time you experience this and have no clue why the code is not verifying properly. There are two properties that Dafny needs you to prove: partial correctness and termination. Together these form *total correctness*.
@ -111,7 +113,4 @@ method fact(x: int) returns (y: int)
y := y * z; y := y * z;
} }
} }
``` ```

11
content/blog/docker-secrets.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Docker Secrets" date: 2022-02-04 23:59:13-05:00
date: 2022-02-04T23:59:13-05:00
draft: false draft: false
tags: ["Containers"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 58cc9e00b1a7
tags:
- Containers
title: Docker Secrets
--- ---
I try to keep secrets such as passwords and keys out in their own separate files so that I can `.gitignore` them and commit the rest of my configuration. With `docker-compose` we can do that with the `env_file` field. Here is an example with a postgres configuration: I try to keep secrets such as passwords and keys out in their own separate files so that I can `.gitignore` them and commit the rest of my configuration. With `docker-compose` we can do that with the `env_file` field. Here is an example with a postgres configuration:
@ -26,5 +28,4 @@ Then in `Volumes/database/docker.env` I can have a file with the secrets as key-
POSTGRES_USER=user POSTGRES_USER=user
POSTGRES_PASSWORD=389ed93045c84cc0828c4310e6ef76ce POSTGRES_PASSWORD=389ed93045c84cc0828c4310e6ef76ce
POSTGRES_DB=database POSTGRES_DB=database
``` ```

10
content/blog/finding-cool-people-on-mastodon.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Finding Cool People on Mastodon" date: 2022-05-15 20:39:35-04:00
date: 2022-05-15T20:39:35-04:00
draft: false draft: false
tags: ["Mastodon"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 50c97fc8aa3c
tags:
- Mastodon
title: Finding Cool People on Mastodon
--- ---
Mastodon is a cool federated micro-blogging platform that can serve as an alternative to Twitter. One of its primary features is that it shows what they call toots from only people you follow in reverse-chronological order. Nowadays, large tech companies employ recommendation engines to surface content from users (you don't even need to follow) in a non-chronological order driven by the number of interactions users similar to you had with the content. The lack of recommendation engine in Mastodon can be a blessing as low-quality emotional content tends to drive more interactions. However, this can also be a curse as cool new people don't naturally surface in your feed. The following are the techniques I employ to consistently seek out cool new people: Mastodon is a cool federated micro-blogging platform that can serve as an alternative to Twitter. One of its primary features is that it shows what they call toots from only people you follow in reverse-chronological order. Nowadays, large tech companies employ recommendation engines to surface content from users (you don't even need to follow) in a non-chronological order driven by the number of interactions users similar to you had with the content. The lack of recommendation engine in Mastodon can be a blessing as low-quality emotional content tends to drive more interactions. However, this can also be a curse as cool new people don't naturally surface in your feed. The following are the techniques I employ to consistently seek out cool new people:
@ -85,4 +87,4 @@ The last resource that I'll share is https://fediverse.info. This is like the tr
## Conclusion ## Conclusion
The lack of recommendation engine has driven the Mastodon community to create new and novel ways of discovering new people. It wouldn't surprise me if within the year a whole new set of tools are made available to us. Though I have to say, the default of not showing unfollowed accounts in our feeds is really nice. It means that our Mastodon experience is truly unique to us, and that we can curate them to our liking. The lack of recommendation engine has driven the Mastodon community to create new and novel ways of discovering new people. It wouldn't surprise me if within the year a whole new set of tools are made available to us. Though I have to say, the default of not showing unfollowed accounts in our feeds is really nice. It means that our Mastodon experience is truly unique to us, and that we can curate them to our liking.

7
content/blog/finding-cuda-errors.md
View file

@ -1,10 +1,11 @@
--- ---
title: "Finding Cuda Errors" date: 2022-03-08 10:53:43-05:00
date: 2022-03-08T10:53:43-05:00
draft: false draft: false
tags: []
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: a07f460ce553
tags: []
title: Finding Cuda Errors
--- ---
When cuda fails, it fails silently. To combat this, I have gotten into a habit of checking for a failed status for every cuda memory allocation, kernel execution etc. The following is a C++ macro I wrote that checks if a previous cuda call has failed and then prints the current line and file of the macro. When cuda fails, it fails silently. To combat this, I have gotten into a habit of checking for a failed status for every cuda memory allocation, kernel execution etc. The following is a C++ macro I wrote that checks if a previous cuda call has failed and then prints the current line and file of the macro.

8
content/blog/git-bisect-broken-builds.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Which commit broke the build? Using Git Bisect" date: 2022-05-03 01:15:55-04:00
date: 2022-05-03T01:15:55-04:00
draft: false draft: false
tags: ["Git"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 1ef72415ab75
tags:
- Git
title: Which commit broke the build? Using Git Bisect
--- ---
Lets imagine a scenario where in the latest merge a test Lets imagine a scenario where in the latest merge a test

11
content/blog/git-diff-by-words.md
View file

@ -1,15 +1,16 @@
--- ---
title: "Git Diff by Words" date: 2022-02-04 21:23:30-05:00
date: 2022-02-04T21:23:30-05:00
draft: false draft: false
tags: ["Git"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 1fa7eb8ae0f5
tags:
- Git
title: Git Diff by Words
--- ---
When working in LaTex it is often more useful to see the changes by words as opposed to lines. Luckily, it's pretty easy to view this in the terminal. When working in LaTex it is often more useful to see the changes by words as opposed to lines. Luckily, it's pretty easy to view this in the terminal.
```bash ```bash
git diff --color-words git diff --color-words
``` ```

11
content/blog/git-partial-clones.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Git Partial Clones" date: 2022-02-07 17:07:08-05:00
date: 2022-02-07T17:07:08-05:00
draft: false draft: false
tags: ["Git"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 95d4bd60af72
tags:
- Git
title: Git Partial Clones
--- ---
I recently was introduced to [Sparse Directories in SVN](https://svnbook.red-bean.com/en/1.8/svn.advanced.sparsedirs.html). In SVN, you can initially clone a repository and have it be empty until you checkout the specific files needed. I wondered if I can do the same with `git`. For the *tl;dr* skip to the conclusion section. I recently was introduced to [Sparse Directories in SVN](https://svnbook.red-bean.com/en/1.8/svn.advanced.sparsedirs.html). In SVN, you can initially clone a repository and have it be empty until you checkout the specific files needed. I wondered if I can do the same with `git`. For the *tl;dr* skip to the conclusion section.
@ -119,5 +121,4 @@ You can even set it so that a specific folder is shown at the root of your direc
```bash ```bash
git sparse-checkout set FOLDERNAME git sparse-checkout set FOLDERNAME
``` ```

9
content/blog/intensional-logic-extends-first-order.md
View file

@ -1,10 +1,11 @@
--- ---
title: "Intensional Logic Extends First Order" date: 2022-02-26 20:33:38-05:00
date: 2022-02-26T20:33:38-05:00
draft: false draft: false
tags: []
math: true math: true
medium_enabled: true medium_enabled: true
medium_post_id: 8e07b68aa8f5
tags: []
title: Intensional Logic Extends First Order
--- ---
The second brightest object in the sky is known as the morgensteorra (morning star) and æfensteorra (evening star). Later on this object became known as Venus. [(Wikipedia)](https://en.wikipedia.org/wiki/Venus_in_culture) The second brightest object in the sky is known as the morgensteorra (morning star) and æfensteorra (evening star). Later on this object became known as Venus. [(Wikipedia)](https://en.wikipedia.org/wiki/Venus_in_culture)
@ -21,4 +22,4 @@ In first order logic, we can then deduce the following:
$$ $$
B(\text{morgensteorra} = \text{venus}) B(\text{morgensteorra} = \text{venus})
$$ $$
But does that make sense? It is possible to hold a belief that Venus is the evening star while not holding a belief that Venus is the morning star. Therefore, we cannot treat belief as a traditional relation symbol. Issues like these give birth to intensional reasoning and from that modal logic. But does that make sense? It is possible to hold a belief that Venus is the evening star while not holding a belief that Venus is the morning star. Therefore, we cannot treat belief as a traditional relation symbol. Issues like these give birth to intensional reasoning and from that modal logic.

10
content/blog/junit-script.md
View file

@ -1,10 +1,12 @@
--- ---
title: "JUnit Script" date: 2022-02-26 20:02:53-05:00
date: 2022-02-26T20:02:53-05:00
draft: false draft: false
tags: ["Java"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 7ca070e54955
tags:
- Java
title: JUnit Script
--- ---
Running a JUnit test on the terminal is a little annoying. Here is a quick script to make it easier, make it executable and drop it in [`~/.local/bin`](/blog/customexec/) for easy use. Running a JUnit test on the terminal is a little annoying. Here is a quick script to make it easier, make it executable and drop it in [`~/.local/bin`](/blog/customexec/) for easy use.
@ -32,4 +34,4 @@ java -cp "$JUNIT_PATH":. org.junit.runner.JUnitCore "$1"
``` ```
Replacing `JUNIT_PATH` with the location of the `junit4.jar` on your system. Replacing `JUNIT_PATH` with the location of the `junit4.jar` on your system.

10
content/blog/latexlistlabels.md
View file

@ -1,10 +1,12 @@
--- ---
title: "LaTex List Labels" date: 2022-01-16 23:17:51-05:00
date: 2022-01-16T23:17:51-05:00
draft: false draft: false
tags: ["LaTex"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: b978cbe10da3
tags:
- LaTex
title: LaTex List Labels
--- ---
A quick tip that I recently learned is that the symbols in a LaTex list item is changeable. In fact, the following technique works for both the `enumerate` and `itemize` environments. A quick tip that I recently learned is that the symbols in a LaTex list item is changeable. In fact, the following technique works for both the `enumerate` and `itemize` environments.
@ -22,4 +24,4 @@ A quick tip that I recently learned is that the symbols in a LaTex list item is
\end{enumerate} \end{enumerate}
``` ```
![](/files/images/blog/202201162357.svg) ![](/files/images/blog/202201162357.svg)

10
content/blog/multicolumnbeamerslide.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Multi-Column slides in Beamer" date: 2022-01-26 23:29:31-05:00
date: 2022-01-26T23:29:31-05:00
draft: false draft: false
tags: ["LaTex"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: cd19b12d502f
tags:
- LaTex
title: Multi-Column slides in Beamer
--- ---
When creating slides in LaTex Beamer, it can be frustrating to not have the easy ability to drag text boxes around. Luckily, creating a multi-column layout in Beamer is not difficult! Below is an example of a two column slide layout, where the left side is a bulleted list, and the right side is an image: When creating slides in LaTex Beamer, it can be frustrating to not have the easy ability to drag text boxes around. Luckily, creating a multi-column layout in Beamer is not difficult! Below is an example of a two column slide layout, where the left side is a bulleted list, and the right side is an image:
@ -40,4 +42,4 @@ When creating slides in LaTex Beamer, it can be frustrating to not have the easy
\end{document} \end{document}
``` ```
![](/files/images/blog/202201262338.svg) ![](/files/images/blog/202201262338.svg)

10
content/blog/networkx-random-sample-graph.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Networkx Random Sample Graph" date: 2022-04-07 19:48:12-04:00
date: 2022-04-07T19:48:12-04:00
draft: false draft: false
tags: ["Python"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: e5c5330cc9a7
tags:
- Python
title: Networkx Random Sample Graph
--- ---
I've been working on several algorithms in `networkx`. In order to speed up testing, especially on large graphs, I've been randomly sampling portions of the original graph. The best way I've found to do this is through the following python snippet: I've been working on several algorithms in `networkx`. In order to speed up testing, especially on large graphs, I've been randomly sampling portions of the original graph. The best way I've found to do this is through the following python snippet:
@ -24,4 +26,4 @@ random_nodes = random.sample(list(G.nodes), SAMPLE_SIZE)
G_sample = G.subgraph(random_nodes) G_sample = G.subgraph(random_nodes)
``` ```
However, only considering the nodes when sampling makes it highly likely that the subgraph will significantly less edges. This results in a mostly disconnected subgraph and a loss of information. Sampling the edges prevents this issue at the expense of not capturing single nodes not connected to anything else. However, only considering the nodes when sampling makes it highly likely that the subgraph will significantly less edges. This results in a mostly disconnected subgraph and a loss of information. Sampling the edges prevents this issue at the expense of not capturing single nodes not connected to anything else.

10
content/blog/networkxtree.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Tree-based Plots in NetworkX" date: 2022-01-02 20:36:41-05:00
date: 2022-01-02T20:36:41-05:00
draft: false draft: false
tags: ["Python"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: c8cffb5c4078
tags:
- Python
title: Tree-based Plots in NetworkX
--- ---
A graph in D3 and NetworkX can be represented as a JSON file. A graph in D3 and NetworkX can be represented as a JSON file.
@ -51,4 +53,4 @@ plt.show()
Given the JSON from the top of the post it'll produce: Given the JSON from the top of the post it'll produce:
![image-20220103000837137](/files/images/blog/20220103000837137.png) ![image-20220103000837137](/files/images/blog/20220103000837137.png)

9
content/blog/nginx-gzip.md
View file

@ -1,10 +1,11 @@
--- ---
title: "Reducing Network Bandwidth in Nginx with Gzip" date: 2022-02-04 20:06:50-05:00
date: 2022-02-04T20:06:50-05:00
draft: false draft: false
tags: []
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: ebd510dbf691
tags: []
title: Reducing Network Bandwidth in Nginx with Gzip
--- ---
Browsers that support gzip compression send the header `Accept-Encoding: gzip` in its request and if the webserver supports gzip, then it can send the website data back compressed. Though recently I learned that this isn't setup by default in `nginx`! This post will go over the configuration you'll need to add to `/etc/nginx/nginx.conf` in order to support `gzip` compression. From my experience, enabling `gzip` compression reduced network traffic by 1/4. Browsers that support gzip compression send the header `Accept-Encoding: gzip` in its request and if the webserver supports gzip, then it can send the website data back compressed. Though recently I learned that this isn't setup by default in `nginx`! This post will go over the configuration you'll need to add to `/etc/nginx/nginx.conf` in order to support `gzip` compression. From my experience, enabling `gzip` compression reduced network traffic by 1/4.
@ -54,4 +55,4 @@ What each of the commands do:
| `gzip_buffers` | Sets the `*number*` and `*size*` of buffers used to compress a response. By default, the buffer size is equal to one memory page. This is either 4K or 8K, depending on a platform. | | `gzip_buffers` | Sets the `*number*` and `*size*` of buffers used to compress a response. By default, the buffer size is equal to one memory page. This is either 4K or 8K, depending on a platform. |
| `gzip_http_version` | Sets the minimum HTTP version of a request required to compress a response. | | `gzip_http_version` | Sets the minimum HTTP version of a request required to compress a response. |
| `gzip_min_length` | Sets the minimum length of a response that will be gzipped. The length is determined only from the “Content-Length” response header field. | | `gzip_min_length` | Sets the minimum length of a response that will be gzipped. The length is determined only from the “Content-Length” response header field. |
| `gzip_types` | Enables gzipping of responses for the specified MIME types in addition to “`text/html`”. The special value “`*`” matches any MIME type (0.8.29). Responses with the “`text/html`” type are always compressed. | | `gzip_types` | Enables gzipping of responses for the specified MIME types in addition to “`text/html`”. The special value “`*`” matches any MIME type (0.8.29). Responses with the “`text/html`” type are always compressed. |

10
content/blog/non-root-systemd-scripts.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Non-Root Systemd Scripts" date: 2022-03-15 23:55:19-04:00
date: 2022-03-15T23:55:19-04:00
draft: false draft: false
tags: ["Linux"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: f527d0f12fb8
tags:
- Linux
title: Non-Root Systemd Scripts
--- ---
I know of two ways to run systemd services not as root. They both have their pros and cons associated with them. I know of two ways to run systemd services not as root. They both have their pros and cons associated with them.
@ -105,4 +107,4 @@ From [FreeDesktop](https://www.freedesktop.org/software/systemd/man/loginctl.htm
For a multi-user system, one can argue that linger is not a good property to have because users can then have a lot of processes spawned and persistent even if they are not using the system. In that case, having an admin individually add systemd unit files using the first approach makes sense. For a multi-user system, one can argue that linger is not a good property to have because users can then have a lot of processes spawned and persistent even if they are not using the system. In that case, having an admin individually add systemd unit files using the first approach makes sense.
The second approach has the benefit that the admin only has to set the linger property of the user once, and then the user can create as many systemd unit services as they'd like. The second approach has the benefit that the admin only has to set the linger property of the user once, and then the user can create as many systemd unit services as they'd like.

10
content/blog/openmpi-fedora.md
View file

@ -1,10 +1,12 @@
--- ---
title: "OpenMPI on Fedora" date: 2022-05-03 00:52:38-04:00
date: 2022-05-03T00:52:38-04:00
draft: false draft: false
tags: ["Fedora"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 1c0c98b99e8a
tags:
- Fedora
title: OpenMPI on Fedora
--- ---
To use use the OpenMPI compilers (mpicc, mpic++, etc.) and mpirun To use use the OpenMPI compilers (mpicc, mpic++, etc.) and mpirun
@ -33,4 +35,4 @@ module load mpi/openmpi-x86_64
Finally, with these changes you can use the compiler Finally, with these changes you can use the compiler
tools and runner. Do note that you'll have to source tools and runner. Do note that you'll have to source
and load the OpenMPI module for every shell you open and load the OpenMPI module for every shell you open
unless you add it within `$HOME/.bashrc`. unless you add it within `$HOME/.bashrc`.

9
content/blog/permission-denied-writing-privileged-locations.md
View file

@ -1,10 +1,11 @@
--- ---
title: "Permission Denied: Writing to Privileged Locations" date: 2022-04-07 20:09:40-04:00
date: 2022-04-07T20:09:40-04:00
draft: false draft: false
tags: []
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 7d133254be3f
tags: []
title: 'Permission Denied: Writing to Privileged Locations'
--- ---
Perhaps you've tried something like the following: Perhaps you've tried something like the following:
@ -27,4 +28,4 @@ Instead consider the following:
echo "hi" | sudo tee /etc/test echo "hi" | sudo tee /etc/test
``` ```
The command `tee` takes whatever is in standard in, and writes it to the filename specified. Since we applied `sudo ` to the `tee` command, it now has the necessary permissions to write to a privileged location. The command `tee` takes whatever is in standard in, and writes it to the filename specified. Since we applied `sudo ` to the `tee` command, it now has the necessary permissions to write to a privileged location.

15
content/blog/program-verification-hoare-logic-dafny.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Program Verification with Hoare Logic and Dafny" date: 2022-02-05 00:06:42-05:00
date: 2022-02-05T00:06:42-05:00
draft: false draft: false
tags: ["Formal Methods"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 4cf20da7d8a4
tags:
- Formal Methods
title: Program Verification with Hoare Logic and Dafny
--- ---
In the recitations that I'm giving for [Principles of Software](/ta/spring2022/csci2600/), we are going over reasoning through code using Hoare Logic and the program verifier Dafny. Microsoft Research designed Dafny to be similar to writing imperative code. The main difference is that you need to supply (pre/post)-conditions and the code to verify. Here's an example of how to reason about a simple statement by hand: In the recitations that I'm giving for [Principles of Software](/ta/spring2022/csci2600/), we are going over reasoning through code using Hoare Logic and the program verifier Dafny. Microsoft Research designed Dafny to be similar to writing imperative code. The main difference is that you need to supply (pre/post)-conditions and the code to verify. Here's an example of how to reason about a simple statement by hand:
@ -55,9 +57,4 @@ method abs(x: int) returns (y: int)
assert y == x; assert y == x;
} }
} }
``` ```

10
content/blog/proving-loop-invariants.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Loop Invariants" date: 2022-02-26 19:17:21-05:00
date: 2022-02-26T19:17:21-05:00
draft: false draft: false
tags: ["Formal Methods"]
math: true math: true
medium_enabled: true medium_enabled: true
medium_post_id: 395dbef73491
tags:
- Formal Methods
title: Loop Invariants
--- ---
Loop invariants are one of the more complicated concepts in Hoare Logic. One might say that we can simply unroll the loop, but there are many loops where we don't know the number of iterations in advanced. Therefore, we often consider what is called the loop invariant. These are statements that are true before, during, and after the loop. A useful loop invariant in combination of the negation of the loop condition can also prove some postcondition. Lets look at a multiplication example Loop invariants are one of the more complicated concepts in Hoare Logic. One might say that we can simply unroll the loop, but there are many loops where we don't know the number of iterations in advanced. Therefore, we often consider what is called the loop invariant. These are statements that are true before, during, and after the loop. A useful loop invariant in combination of the negation of the loop condition can also prove some postcondition. Lets look at a multiplication example
@ -89,4 +91,4 @@ $$
(x_n == a * p_n) \wedge (p \ge b) \wedge (p \le b) \\\\ (x_n == a * p_n) \wedge (p \ge b) \wedge (p \le b) \\\\
\implies (x_n == a * p_n) \wedge (p == b) \\\\ \implies (x_n == a * p_n) \wedge (p == b) \\\\
\implies (x_n == a * b) \checkmark \\ \implies (x_n == a * b) \checkmark \\
$$ $$

10
content/blog/rclone.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Rclone: The Swiss Army Knife of Cloud Storage" date: 2022-04-10 22:05:46-04:00
date: 2022-04-10T22:05:46-04:00
draft: false draft: false
tags: ["Backup"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: ee4c7c4d2966
tags:
- Backup
title: 'Rclone: The Swiss Army Knife of Cloud Storage'
--- ---
[Rclone](https://rclone.org/) is a terminal application that manages remote storage. It supports the standard remote filesystem protocols such as S3, (S)FTP, WebDAV as well as easy to use integration with cloud providers such as Amazon S2, Backblaze B2, Google Drive, and others. We can even perform regular backups using [Restic](https://restic.net/) with Rclone underneath. With all these features, it's easy to configure all remote storage within Rclone and then synchronize the configuration file across machines. [Rclone](https://rclone.org/) is a terminal application that manages remote storage. It supports the standard remote filesystem protocols such as S3, (S)FTP, WebDAV as well as easy to use integration with cloud providers such as Amazon S2, Backblaze B2, Google Drive, and others. We can even perform regular backups using [Restic](https://restic.net/) with Rclone underneath. With all these features, it's easy to configure all remote storage within Rclone and then synchronize the configuration file across machines.
@ -221,4 +223,4 @@ WantedBy=default.target
## Conclusion ## Conclusion
This is just the tip of the iceburg when it comes to Rclone! Another popular feature is automatically [encrypting](https://rclone.org/crypt/) files uploaded to cloud storage. Once you have everything configured to your liking, you can synchronize the file under `~/.config/rclone/rclone.conf` across all your machines. This is just the tip of the iceburg when it comes to Rclone! Another popular feature is automatically [encrypting](https://rclone.org/crypt/) files uploaded to cloud storage. Once you have everything configured to your liking, you can synchronize the file under `~/.config/rclone/rclone.conf` across all your machines.

11
content/blog/rebuildkernelakmod.md
View file

@ -1,10 +1,13 @@
--- ---
title: "Rebuild Kernel Modules with Akmods" date: 2022-02-04 19:37:04-05:00
date: 2022-02-04T19:37:04-05:00
draft: false draft: false
tags: ["Linux", "Fedora"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: ab0e2a2ce3b3
tags:
- Linux
- Fedora
title: Rebuild Kernel Modules with Akmods
--- ---
Akmods is the Fedora/Red Hat way of managing kernel modules. In Ubuntu, this is `dkms`. If you're like me and force reboot shortly after performing an update, then you might have not given akmods enough time to compile any extra kernel modules (for example: Nvidia). This meant that I had to boot into an older kernel to try to fix the problem.... Akmods is the Fedora/Red Hat way of managing kernel modules. In Ubuntu, this is `dkms`. If you're like me and force reboot shortly after performing an update, then you might have not given akmods enough time to compile any extra kernel modules (for example: Nvidia). This meant that I had to boot into an older kernel to try to fix the problem....
@ -26,4 +29,4 @@ to trigger the rebuild.
Though the better solution is to avoid this problem to begin with. Though the better solution is to avoid this problem to begin with.
If you `reboot` not as root, then systemd will check to see if If you `reboot` not as root, then systemd will check to see if
any process is inhibiting the poweroff. If that's the case, any process is inhibiting the poweroff. If that's the case,
wait patiently and don't type `sudo reboot`. wait patiently and don't type `sudo reboot`.

10
content/blog/rootless-docker-compose-podman.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Rootless Docker-Compose with Podman" date: 2022-01-29 20:21:11-05:00
date: 2022-01-29T20:21:11-05:00
draft: false draft: false
tags: ["Containers"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: d31b7e2a688c
tags:
- Containers
title: Rootless Docker-Compose with Podman
--- ---
One of the benefits of Podman over Docker is that it can run daemon-less and without root. However, `docker-compose` is by far my favorite way to create and maintain containers. Luckily, the Podman folks emulated the Docker CLI so that `docker-compose` works well with Podman! One of the benefits of Podman over Docker is that it can run daemon-less and without root. However, `docker-compose` is by far my favorite way to create and maintain containers. Luckily, the Podman folks emulated the Docker CLI so that `docker-compose` works well with Podman!
@ -71,4 +73,4 @@ Now we can run `docker-compose`!
docker-compose ps docker-compose ps
``` ```
[^1]: https://bugzilla.redhat.com/show_bug.cgi?id=2125878 [^1]: https://bugzilla.redhat.com/show_bug.cgi?id=2125878

11
content/blog/s3-fuse.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Mount Object Storage Locally using S3 Fuse" date: 2022-02-04 23:39:25-05:00
date: 2022-02-04T23:39:25-05:00
draft: false draft: false
tags: ["Storage"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: a6add7081378
tags:
- Storage
title: Mount Object Storage Locally using S3 Fuse
--- ---
On most cloud providers, object storage is cheaper than paying for the equivalent size in block storage. Using FUSE, we can mount S3 compatible object storage with the command `s3fs`. Do note, that there are a few downsides with mounting object storage as documented on their [README](https://github.com/s3fs-fuse/s3fs-fuse/blob/master/README.md): On most cloud providers, object storage is cheaper than paying for the equivalent size in block storage. Using FUSE, we can mount S3 compatible object storage with the command `s3fs`. Do note, that there are a few downsides with mounting object storage as documented on their [README](https://github.com/s3fs-fuse/s3fs-fuse/blob/master/README.md):
@ -61,5 +63,4 @@ To mount automatically during reboot, add the following to `/etc/fstab`:
bucketname /mnt/mountpoint fuse.s3fs _netdev,allow_other,url=https://us-east-1.linodeobjects.com 0 0 bucketname /mnt/mountpoint fuse.s3fs _netdev,allow_other,url=https://us-east-1.linodeobjects.com 0 0
``` ```
After editing `/etc/fstab` you can run `sudo mount -a` in order for it to load and mount any new entries. After editing `/etc/fstab` you can run `sudo mount -a` in order for it to load and mount any new entries.

11
content/blog/snap-flatpak-aliases.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Aliases for Snaps and Flatpaks" date: 2022-02-04 20:29:04-05:00
date: 2022-02-04T20:29:04-05:00
draft: false draft: false
tags: ["Linux"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 5f51916cafd3
tags:
- Linux
title: Aliases for Snaps and Flatpaks
--- ---
Sometimes snap packages and flatpaks come with unmemorable names to run their commands. Luckily for snap packages, you can easily alias them. For example, to rename the .NET executable to `dotnet` run. Sometimes snap packages and flatpaks come with unmemorable names to run their commands. Luckily for snap packages, you can easily alias them. For example, to rename the .NET executable to `dotnet` run.
@ -34,5 +36,4 @@ done
# main # main
launch_app "${1}" launch_app "${1}"
``` ```

12
content/blog/socks5proxy.md
View file

@ -1,10 +1,13 @@
--- ---
title: "Configuring a SOCKS5 Proxy" date: 2022-01-03 10:41:09-05:00
date: 2022-01-03T10:41:09-05:00
draft: false draft: false
tags: ["Networking", "SSH"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: ed506a09a2b2
tags:
- Networking
- SSH
title: Configuring a SOCKS5 Proxy
--- ---
A SOCKS5 proxy allows you to have network traffic as if it was coming from the proxy server as opposed to your local client. You can easily set it up using SSH from your local machine. A SOCKS5 proxy allows you to have network traffic as if it was coming from the proxy server as opposed to your local client. You can easily set it up using SSH from your local machine.
@ -31,5 +34,4 @@ To do this you will need proxychains installed. On Ubuntu, the package is called
``` ```
socks5 127.0.0.1 1337 socks5 127.0.0.1 1337
``` ```

9
content/blog/termtosvg.md
View file

@ -1,10 +1,11 @@
--- ---
title: "Terminal Output To SVG Animations" date: 2022-01-17 10:14:22-05:00
date: 2022-01-17T10:14:22-05:00
draft: false draft: false
tags: []
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: ad8c533610b5
tags: []
title: Terminal Output To SVG Animations
--- ---
With [`termtosvg`](https://github.com/nbedos/termtosvg) made by Nicolas Bedo we can make SVG animations from terminal output in the style of [asciinema](https://asciinema.org/). To install use [pipx](/blog/managepythonapps/). With [`termtosvg`](https://github.com/nbedos/termtosvg) made by Nicolas Bedo we can make SVG animations from terminal output in the style of [asciinema](https://asciinema.org/). To install use [pipx](/blog/managepythonapps/).
@ -53,4 +54,4 @@ termtosvg -s
Here is an example of an animation I made with this tool: Here is an example of an animation I made with this tool:
![](/files/images/blog/202201171031.svg) ![](/files/images/blog/202201171031.svg)

10
content/blog/why-i-pesos-from-mastodon.md
View file

@ -1,10 +1,12 @@
--- ---
title: "Why I PESOS From Mastodon" date: 2022-05-15 18:36:16-04:00
date: 2022-05-15T18:36:16-04:00
draft: false draft: false
tags: ["Mastodon"]
math: false math: false
medium_enabled: true medium_enabled: true
medium_post_id: 56667e2c305
tags:
- Mastodon
title: Why I PESOS From Mastodon
--- ---
The [IndieWeb movement](https://indieweb.org) is focused on people controlling their own experience on the web. They accomplish this by encouraging everyone to have their own personal website. Followers can then either subscribe to the [RSS feed](https://aboutfeeds.com/) and provide [Webmentions](https://indieweb.org/Webmention) back to the post, or they can interact with the material directly on another website like [Mastodon](https://joinmastodon.org/). The [IndieWeb movement](https://indieweb.org) is focused on people controlling their own experience on the web. They accomplish this by encouraging everyone to have their own personal website. Followers can then either subscribe to the [RSS feed](https://aboutfeeds.com/) and provide [Webmentions](https://indieweb.org/Webmention) back to the post, or they can interact with the material directly on another website like [Mastodon](https://joinmastodon.org/).
@ -26,4 +28,4 @@ The main advantage of PESOS is that my primary interaction with Mastodon is thro
## Disadvantages to PESOS ## Disadvantages to PESOS
The primary way that people are following me is within Mastodon itself as opposed to the RSS feed on my website. This means that if the Mastodon server ever abruptly goes down, then I will lose contact with all of my followers. Mastodon, however, does have some protection against this as a federated network. Mainly the ability to [move your profile](https://docs.joinmastodon.org/user/moving/) from one Mastodon instance to another. This gives me a more secure feeling that Mastodon itself won't shut down in the near future. The primary way that people are following me is within Mastodon itself as opposed to the RSS feed on my website. This means that if the Mastodon server ever abruptly goes down, then I will lose contact with all of my followers. Mastodon, however, does have some protection against this as a federated network. Mainly the ability to [move your profile](https://docs.joinmastodon.org/user/moving/) from one Mastodon instance to another. This gives me a more secure feeling that Mastodon itself won't shut down in the near future.