From 091a6860703c2e1e175f4b5e04ae0aefa6be5c77 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 16 Aug 2019 03:29:13 -0700 Subject: [PATCH] Fix list rendering in some posts. --- content/blog/coq_palindrome.md | 3 +++ content/blog/crystal_on_arm.md | 4 +++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/content/blog/coq_palindrome.md b/content/blog/coq_palindrome.md index 6ce1105..a62a40f 100644 --- a/content/blog/coq_palindrome.md +++ b/content/blog/coq_palindrome.md @@ -7,10 +7,12 @@ Going through the Software Foundations textbook, I found an exercise which I rea ### The inductive definition I wasn’t sure at first why the problem said that the inductive definition should have three constructors. I came up with two ways to construct a palindrome: + * An empty list is a palindrome. * Adding the same value to the back and the front of another palindrome makes a longer palindrome. Of course, my definition led to only having palindromes of even length. In order to allow for palindromes of odd length, one more rule is needed (another base case): + * A list with a single value is a palindrome. This translates readily into Coq: @@ -42,6 +44,7 @@ The proof in the other direction took me a significant amount of time. It was cl #### A different kind of induction Coq’s basic induction wouldn’t do. But structural induction doesn’t limit us to a particular definition of a list; it just states that if: + * We can prove that a proposition holds for the primitive values of a type * We can prove that if the proposition holds for the building blocks of a value of the type then the proposition holds for the value built of those blocks diff --git a/content/blog/crystal_on_arm.md b/content/blog/crystal_on_arm.md index d11d1e5..6dd6799 100644 --- a/content/blog/crystal_on_arm.md +++ b/content/blog/crystal_on_arm.md @@ -33,6 +33,7 @@ git checkout 0.27.2 ``` Now, I had the compiler and the source. I was ready to compile the source to get myself a nice ARM Crystal compiler. But how? The official guide specified two options for cross compilation: + * `--cross-compile` - This option is basically a flag. You just add it to the command to enable cross compilation. * `--target=` - This specifies the target architecture you're building for. @@ -43,9 +44,10 @@ gcc -dumpmachine This produced the output `armv7l-unknown-linux-gnueabihf`. This was exactly what I needed to know! Finally, looking through the Makefile in the repository, I found three more flags that are used by default in the process: + * `-D without_openssl` * `-D without_zlib` -* `--release` - for faster compiler +* `--release` - for a faster compiler To compile the compiler, I had to compile the `src/compiler/crystal.cr` file. With all these options, the command came out to be: ```