+++ /dev/null
-#+title: sources of aminb.org's pages and posts
-
-#+hugo_base_dir: ..
-#+seq_todo: TODO DRAFT DONE
-#+property: header-args :eval never-export
-#+options: author:nil
-
-#+macro: abbr @@html:<abbr>$1</abbr>@@
-#+macro: span @@html:<span class="$1">$2</span>@@
-
-* Pages
-:PROPERTIES:
-:EXPORT_HUGO_SECTION: /
-:END:
-
-** Home
-:PROPERTIES:
-:EXPORT_FILE_NAME: _index
-:END:
-
-I'm a [[/uw][graduate student]] in the [[https://watform.uwaterloo.ca][WatForm]] group at University of Waterloo,
-supervised by [[https://cs.uwaterloo.ca/~nday/][Dr. Nancy Day]]. Currently, my research focuses on formal
-logic, model checking, and verification.
-
-** CV
-:PROPERTIES:
-:EXPORT_FILE_NAME: cv
-:EXPORT_HUGO_MENU: :menu topnav :weight 10
-:END:
-
-My academic {{{abbr(CV)}}} is available as [[/cv.pdf][cv.pdf]],
-and an outdated professional resume is available as [[/resume.pdf][resume.pdf]] as
-well.
-
-I'm interested in functional programming and functional languages,
-type systems, and formal methods in general. I love writing Haskell
-and I'm looking into Rust and Lean as well. Feel free to [[/contact][drop me a
-line]] if you like to geek out about any of the above.
-
-** DONE Now
-CLOSED: [2018-09-04 Tue 10:53]
-:PROPERTIES:
-:EXPORT_FILE_NAME: now
-:EXPORT_HUGO_AUTO_SET_LASTMOD: t
-:EXPORT_HUGO_MENU: :menu topnav :weight 20
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :customTitle "What I'm doing now"
-:END:
-
-This is my [[https://nownownow.com/about][now page]].
-
-I'm currently a [[/uw][graduate student]] in the Waterloo Formal Methods group
-at University of Waterloo. I just finished my degree’s coursework
-requirements in Fall 2018, and will be focusing on my thesis starting
-this term, Winter 2019.
-
-In my spare time, I write [[https://www.gnu.org/philosophy/free-sw.en.html][free software]] (see my [[/projects][projects]] page), and
-tend to various tasks as a GNU webmaster. I've also been picking up
-the guitar, after giving up on my longtime dream of being a pianist
-(at least for now).
-
-This update was on {{< lastmod >}}.
-
-** DONE Projects
-CLOSED: [2019-01-02 Wed 00:32]
-:PROPERTIES:
-:EXPORT_FILE_NAME: projects
-:EXPORT_HUGO_MENU: :menu topnav :weight 30
-:END:
-
-This page is simply a placeholder to generate a menu item, and my
-server routes this request to cgit.
-
-That said, if you /are/ seeing this page, then something has gone
-wrong; please do get in touch with me!
-
-** DONE Contact
-CLOSED: [2018-09-03 Mon 20:44]
-:PROPERTIES:
-:EXPORT_FILE_NAME: contact
-:EXPORT_HUGO_MENU: :menu topnav :weight 40
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :customTitle "Say hello!"
-:END:
-
-#+macro: xmpp @@html:<a href="xmpp:$1">$1</a>@@
-
-You can contact me via email or through my accounts on various online
-platforms.
-
-*** Primary
-
-Email is my preferred method of communication.
-
-- [[mailto:amin@aminb.org][amin@aminb.org]], personal or general inquiries
-- [[mailto:bandali@gnu.org][bandali@gnu.org]], GNU- or free software-related ([[/gpg][gpg key]])
-- [[mailto:abandali@uwaterloo.ca][abandali@uwaterloo.ca]], academic or UW-related
-
-*** Secondary
-
-- irc: bandali on [[https://freenode.net][freenode]] and [[https://wiki.mozilla.org/IRC][moznet]]
-- xmpp: {{{xmpp(bandali@member.fsf.org)}}}
-- matrix: [[https://matrix.to/#/@bandali:matrix.org][@bandali:matrix.org]]
-- fediverse: [[https://pleroma.site/users/aminb][aminb@pleroma.site]]
-
-*** Other online places
-
-- [[https://git.sr.ht/~bandali][bandali]] on [[https://sr.ht][sr.ht]]
-- [[https://savannah.gnu.org/users/bandali][bandali]] on Savannah
-- [[https://lobste.rs/u/bandali][bandali]] on Lobsters
-- [[https://hackage.haskell.org/user/bandali][bandali]] on Hackage
-- [[https://gitlab.com/bandali][bandali]] on GitLab
-- [[https://keybase.io/bandali][bandali]] on Keybase
-- [[https://news.ycombinator.com/user?id=bandali][bandali]] on HN
-- [[https://www.reddit.com/u/bandali][bandali]] on Reddit
-
-*** Dormant accounts
-
-These are accounts I don't use anymore, unless absolutely necessary.
-
-- [[https://functional.cafe/@a][a]] on functional.cafe
-- [[https://mastodon.social/@aminb][aminb]] on mastodon.social
-- [[https://savannah.gnu.org/users/aminb][aminb]] on Savannah
-- [[https://hackage.haskell.org/user/aminb][aminb]] on Hackage
-- [[https://github.com/aminb][aminb]] on GitHub
-- [[https://www.reddit.com/u/aminb][aminb]] on Reddit
-- [[https://twitter.com/aminban][aminban]] on Twitter
-
-** Colophon
-:PROPERTIES:
-:EXPORT_FILE_NAME: colophon
-:END:
-
-#+macro: light @@html:<label class="light-off-button-inline" for="light-off"></label>@@
-#+macro: ccbysa @@html:<a rel="license" href="//creativecommons.org/licenses/by-sa/4.0/">Creative Commons Attribution-ShareAlike 4.0 International @@{{{ccbysa-img}}}@@html:</a>@@
-#+macro: ccbysa-img @@html:<img alt="Creative Commons Licence" style="border-width:0" src="//i.creativecommons.org/l/by-sa/4.0/80x15.png"/>@@
-
-This is my personal website, previous versions of which I've ran on
-different domains since 2012. I've previously used Octopress, Jekyll,
-a [[https://github.com/aminb/blog-old][custom]] static site generator written in Haskell (kudos to [[https://ruudvanasseldonk.com][Ruud van
-Asseldonk]]), [[https://www.romanzolotarev.com/ssg.html][ssg]] (shout out to [[https://www.romanzolotarev.com][Roman Zolotarev]]), and [[https://orgmode.org/manual/Publishing.html][org-publish]] (see
-also [[https://ambrevar.xyz/blog-architecture/index.html][A blog in pure Org/Lisp]]); but I've since ported it to [[https://ox-hugo.scripter.co/][ox-hugo]], a
-"carefully crafted Org exporter back-end for Hugo" (kudos to [[https://scripter.co][Kaushal
-Modi]]). I've never been happier with my setup.
-
-The sources are available at [[https://aminb.org/projects/aminb.org]].
-The site is automatically generated on each =git push= using the
-[[https://builds.sr.ht][builds.sr.ht]] service (see the [[https://aminb.org/projects/aminb.org/tree/.build.yml][=.build.yml=]] build manifest) and is
-deployed to my server, where it's served using [[https://www.nginx.com][Nginx]] on [[https://www.debian.org][Debian
-GNU/Linux]].
-
-*** Night mode
-
-To toggle night mode, click on {{{light}}}, which is always available
-on the top navigation menu. It saves its state in a browser cookie,
-other than that no JavaScript is required to use this website.
-
-*** Copyright and Licenses
-:PROPERTIES:
-:CUSTOM_ID: copyright
-:END:
-
-The source code for this site is licensed under version 3 (or, at your
-option, any later version) of the [[https://gnu.org/licenses/gpl.html][GNU General Public License]] (see the
-[[https://git.sr.ht/~aminb/aminb.org/tree/COPYING][=COPYING=]] file). The contents of the website are licensed under a
-{{{ccbysa}}} license.
-
-*** i2p angel
-:PROPERTIES:
-:CUSTOM_ID: i2pangel
-:END:
-
-The favicons were derived from [[https://psychosoma.tech][nether]]'s beautiful [[https://psychosoma.tech/me/work/i2pangel.png][i2p angel]], a small
-version of which is displayed on the home page.
-
-** GPG
-:PROPERTIES:
-:EXPORT_FILE_NAME: gpg
-:END:
-
-My [[https://aminb.org/0xA21A020248816103.txt][current key]] is:[fn:1]
-
-#+begin_src txt
-pub rsa4096 2018-10-17 [C] [expires: 2020-10-16]
- BE62 7373 8E61 6D6D 1B3A 08E8 A21A 0202 4881 6103
-uid [ultimate] Amin Bandali <bandali@gnu.org>
-sub rsa4096 2018-10-17 [S] [expires: 2020-10-16]
- 39B3 3C8D 9448 0D2D DCC2 A498 8B44 A0CD C7B9 56F2
-sub rsa4096 2018-10-17 [E] [expires: 2020-10-16]
- 43ED 5F7C F5EC CBDF 2552 FE98 1D52 D14E BCF3 BE08
-sub rsa4096 2018-10-17 [A] [expires: 2020-10-16]
- 70FB 9AAD 5240 2841 2B14 8685 4040 DFEC 6EC1 3F3A
-#+end_src
-
-My [[https://aminb.org/0xD1FBA36627D65876.txt][previous key]], from which I transitioned away, is:
-
-#+begin_src txt
-pub rsa4096 2018-08-05 [C] [expires: 2018-11-16]
- CDDE 75F9 0353 8E71 813C DA27 D1FB A366 27D6 5876
-uid [ultimate] Amin Bandali <amin@gnu.org>
-uid [ultimate] Amin Bandali <amin@aminb.org>
-uid [ultimate] Amin Bandali <mab@gnu.org>
-uid [ultimate] Amin Bandali <aminb@gnu.org>
-sub rsa4096 2018-08-05 [S] [expires: 2018-11-16]
- E14F 56EE 1338 901E A8A8 D2DD 91A9 6FF7 FEF6 BEB4
-sub rsa4096 2018-08-05 [E] [expires: 2018-11-16]
- F9B3 BA24 31A0 9B38 31A3 42EF 1F29 83A9 9A69 D453
-sub rsa4096 2018-08-05 [A] [expires: 2018-11-16]
- 4FB5 D03D A65E 8DA3 39BE 5EDD 6DC3 8F21 4E4B AAA0
-#+end_src
-
-You can obtain my key transition statement signed with both of the
-above keys from https://aminb.org/key-transition-2018-10-17.txt.
-
-*** Older keys
-
-#+begin_src txt
-pub rsa4096 2016-01-31 [SC] [expires: 2019-02-13]
- 500C 1D55 D1EC 1FED E8C0 C8DE 4E05 246A B0BF 7FFB
-uid [ultimate] Amin Bandali <amin@aminb.org>
-uid [ultimate] Amin Bandali <aminb@gnu.org>
-uid [ultimate] Amin Bandali <b@nda.li>
-uid [ultimate] Amin Bandali <me@aminb.org>
-sub rsa4096 2016-01-31 [S] [expires: 2019-02-13]
- 5AC5 0B1B D540 A902 D4B6 2B5C DAE5 4A52 337F 0283
-sub rsa4096 2016-01-31 [E] [expires: 2019-02-13]
- F05B FB25 77C7 5AF6 7783 A66F 3351 056A ACD6 6B1F
-sub rsa4096 2016-01-31 [A] [expires: 2019-02-13]
- C165 6BE2 FDCA D028 0D5A 4314 3A4A C417 58E9 C177
-#+end_src
-
-The key transition statement I'd generated when transitioning away
-from this key is available on
-https://aminb.org/key-transition-2018-08-17.txt.
-
-** Search
-:PROPERTIES:
-:EXPORT_HUGO_SECTION: /
-:EXPORT_FILE_NAME: search
-:EXPORT_HUGO_LAYOUT: search
-:EXPORT_HUGO_OUTPUTS: html json
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :sitemap '((priority . 0.1))
-:END:
-Results from static site search implemented using /Fusejs/, /jquery/
-and /mark.js/. -- [[https://gist.github.com/eddiewebb/735feb48f50f0ddd65ae5606a1cb41ae][Source]]
-
-* Posts
-:PROPERTIES:
-:EXPORT_HUGO_SECTION: post
-:EXPORT_HUGO_AUTO_SET_LASTMOD: t
-:END:
-
-** Arch GNU/Linux on MacBook Air 2013 :arch:macbook:
-:PROPERTIES:
-:EXPORT_FILE_NAME: arch-macbook-air
-:EXPORT_DATE: 2016-11-01
-:EXPORT_OPTIONS: ^:{}
-:EXPORT_HUGO_ALIASES: /2016/11/arch-macbook-air
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :toc true
-:END:
-
-This post summarizes how I install and dual-boot Arch GNU/Linux with
-Full-Disk Encryption alongside macOS. It is not meant to be a
-replacement for the [[https://wiki.archlinux.org/index.php/installation_guide][Installation Guide]] or the former [[https://csdietz.github.io/arch-beginner-guide/][Beginner's Guide]].
-Rather, it mostly serves as a small summary with a few useful notes
-about the gotchas.
-
-So, make sure you understand what you type into your terminal. If you
-don't, checking out the Arch wiki should probably be your first step.
-
-/Note:/ you will need internet access throughout the installation and
-the MacBook Air's WiFi doesn't work out of the box on Arch. I
-recommend using your phone's USB Tethering (if it does support it), or
-using an Ethernet-USB adapter.
-
-*** Shrinking the macOS partition
-
-The first step I take is resizing the HFS+ macOS partition to make
-room for the new {{{abbr(GNU/Linux)}}} installation. There are plenty
-of tutorials on how to do this using macOS's Disk Utility, so do that
-and then come back!
-
-*** Creating a bootable Arch Installer USB
-
-There are different ways of creating a bootable Arch USB, all
-documented on the [[https://wiki.archlinux.org/index.php/USB_flash_installation_media][USB flash installation media]] page on the Arch wiki,
-but the simplest one is using =dd= if you already have access to
-another UNIX system.
-
-{{{span(red,Warning:)}}} make sure you backup the data on your flash
-drive, as =dd= will irrevocably destroy all data on it.
-
-Use =lsblk= to find the name (block device) of your USB drive, then
-run =dd= (as root) as shown below:
-
-#+begin_src bash
-dd bs=4M if=/path/to/archlinux.iso of=/dev/sdx status=progress && sync
-#+end_src
-
-Replace =/path/to/archlinux.iso= with the path to the Arch image you
-have downloaded, and =/dev/sdx= with your drive.
-
-*** Booting up from the USB
-
-After creating the install USB, reboot your laptop and hold the alt
-key and boot into the USB.
-
-When booting is complete and you're presented with the prompt, it's a
-good time to make sure you're connected to the internet (see the
-/note/ at the top of this post).
-
-Use =ping= to verify that you've established a connection:
-
-#+begin_src bash
-ping archlinux.org
-#+end_src
-
-*** Updating the system clock
-
-Once you're connected to the internet, make sure the system clock is
-accurate:
-
-#+begin_src bash
-timedatectl set-ntp true # start and enable systemd-timesyncd
-#+end_src
-
-You can check the service status using =timedatectl status=.
-
-*** Partitioning
-:PROPERTIES:
-:CUSTOM_ID: partitioning
-:END:
-
-I won't dive into partitioning and instead, I'll refer you to the
-[[https://wiki.archlinux.org/index.php/Partitioning][Partitioning]] page of Arch wiki. Of the available partitioning tools, I
-personally prefer =cfdisk=.
-
-*** Setting up LVM & LUKS
-
-I use a [[https://wiki.archlinux.org/index.php/Dm-crypt/Encrypting_an_entire_system#LVM_on_LUKS][LVM on LUKS]] setup, where I set up LVM on top of the encrypted
-partition.
-
-First, let's set up the underlying encrypted partition:
-
-#+begin_src bash
-cryptsetup -v --cipher aes-xts-plain64 --key-size 512 --hash sha512 \
- --iter-time 5000 --use-urandom -y luksFormat /dev/sdaX
-#+end_src
-
-where =/dev/sdaX= is the partition you created in the last step
-(e.g. =/dev/sda4=). For more information about the =cryptsetup=
-options, see the [[https://wiki.archlinux.org/index.php/Dm-crypt/Device_encryption#Encryption_options_for_LUKS_mode][LUKS encryption options]].
-
-Then we open the container:
-
-#+begin_src bash
-cryptsetup open --type luks /dev/sdaX lvm
-#+end_src
-
-Now it's time to use lvm and prepare the logical volume(s):
-
-#+begin_src bash
-pvcreate /dev/mapper/lvm
-vgcreate vg /dev/mapper/lvm
-lvcreate --extents +100%FREE -n root vg
-#+end_src
-
-This will create a physical volume on the mapping we just opened,
-create a volume group named =vg= on the physical volume, and create a
-logical volume named =root= that spans the entire volume group. More
-complex setups are possible thanks to the great flexibility of lvm.
-
-We now format the logical volume with =ext4=:
-
-#+begin_src bash
-mkfs.ext4 /dev/mapper/vg-root
-#+end_src
-
-*** Installing the base system
-
-Let's mount the logical volume, make a directory for the mount point
-of the boot partition, and mount the boot partition (=/dev/sda1=):
-
-#+begin_src bash
-mount /dev/mapper/vg-root /mnt
-mkdir /mnt/boot
-mount /dev/sda1 /mnt/boot
-#+end_src
-
-Finally, let's install the base system (and optionally =base-devel=):
-
-#+begin_src bash
-pacstrap /mnt base base-devel
-#+end_src
-
-*** Configuring the system
-
-Let's generate the fstab:
-
-#+begin_src bash
-genfstab -U /mnt >> /mnt/etc/fstab
-#+end_src
-
-Use your favorite terminal-based editor, edit the fstab file and add
-the =discard= option for the root partition to enable TRIM on the SSD.
-
-Now we change root into our newly installed system and will configure
-it. Adjust these according to your own setup.
-
-#+begin_src bash
-arch-chroot /mnt /bin/bash
-passwd # set the root password
-echo myhostname > /etc/hostname # set the hostname
-ln -s /usr/share/zoneinfo/Canada/Eastern /etc/localtime # time zone
-hwclock --systohc --utc # write system clock to hardware clock (UTC)
-useradd -m -G wheel -s /bin/bash myuser # create myuser
-passwd myuser # set the password for myuser
-echo "myuser ALL=(ALL) NOPASSWD: ALL" >> /etc/sudoers.d/myuser
-# uncomment en_US.UTF-8 UTF-8 and other needed locales in /etc/locale.gen
-locale-gen
-echo LANG=en_US.UTF-8 > /etc/locale.conf
-export LANG=en_US.UTF-8
-#+end_src
-
-Then adjust the initramfs hooks in =/etc/mkinitcpio.conf= and enable
-the =encrypt= and =lvm2= hooks, and make sure =keyboard= is available
-before =encrypt= so you can actually type in the LUKS password when
-booting. Your =HOOKS= line should look similar to this:
-
-#+begin_src
-HOOKS="base udev autodetect modconf block keyboard encrypt lvm2 filesystems fsck"
-#+end_src
-
-After adjusting the hooks, build the initramfs:
-
-#+begin_src bash
-mkinitcpio -p linux
-#+end_src
-
-Now, install the =intel-ucode= package. We'll configure the bootloader
-to enable intel microcode updates.
-
-#+begin_src bash
-pacman -S intel-ucode
-#+end_src
-
-Create the =/boot/loader/loader.conf= with the following content
-(adjust the timeout to your liking):
-
-#+begin_src
-default arch
-timeout 3
-#+end_src
-
-Then create the entry for Arch:
-
-#+begin_src bash
-mkdir -p /boot/loader/entries
-touch /boot/loader/entries/arch.conf
-#+end_src
-
-Now edit =/boot/loader/entries/arch.conf= to specify the Arch entry:
-
-#+begin_src
-title Arch GNU/Linux
-linux /vmlinuz-linux
-initrd /intel-ucode.img
-initrd /initramfs-linux.img
-options cryptdevice=/dev/sdaX:vg:allow-discards root=/dev/mapper/vg-root rw
-#+end_src
-
-Again, =/dev/sdaX= is the partition you created in the [[#partitioning][partitioning]]
-step as the underlying encrypted partition.
-
-Finally, install the bootloader, exit the chroot, umount and reboot!
-
-#+begin_src bash
-bootctl install
-exit
-umount -R /mnt
-reboot
-#+end_src
-
-*** Post-installation recommendations
-
-Congratulations! You now have a minimal Arch installation.
-
-At this point, I usually install my favorite AUR helper, [[https://aur.archlinux.org/packages/pacaur/][pacaur]], then
-I install the [[https://aur.archlinux.org/packages/broadcom-wl-dkms/][broadcom-wl-dkms]] wireless driver and [[https://aur.archlinux.org/packages/mba6x_bl-dkms/][mba6x_bl-dkms]]
-backlight driver to fix the post suspend/resume issue where three's no
-brightness after waking up from suspend, and the only available
-brightness would be 100%.
-
-#+begin_src bash
-pacaur -S linux-headers dkms # linux-headers is required for dkms
-pacaur -S broadcom-wl-dkms
-pacaur -S mba6x_bl-dkms
-#+end_src
-
-Then, I'd like to install
-
-- input, graphics, and sound drivers,
-- a desktop environment (I prefer Xfce or LXQt),
-- a display manager for login screen (lightdm or sddm), and
-- a network manager (NetworkManager or ConnMan).
-
-Check out the [[https://wiki.archlinux.org/index.php/General_recommendations][General recommendations]] for more details.
-
-*** References
-
-Here are some resources I've come across each with lots of useful bits
-and pieces, about installing Arch on a MacBook:
-
-- [[https://github.com/pandeiro/arch-on-air][pandeiro/arch-on-air]]
-- [[https://loicpefferkorn.net/2015/01/arch-linux-on-macbook-pro-retina-2014-with-dm-crypt-lvm-and-suspend-to-disk/][Arch Linux on MacBook Pro Retina 2014 with DM-Crypt, LVM and suspend to disk]]
-- [[http://frankshin.com/installing-archlinux-on-macbook-air-2013/][Installing Archlinux on Macbook Air 2013]]
-- [[http://panks.me/posts/2013/06/arch-linux-installation-with-os-x-on-macbook-air-dual-boot/][Arch Linux Installation with OS X on Macbook Air (Dual Boot)]]
-- [[https://visual-assault.org/2016/03/05/install-encrypted-arch-linux-on-apple-macbook-pro/][Installing (encrypted) Arch Linux on an Apple MacBook Pro]]
-- [[http://alexeyzabelin.com/arch-on-mac][Installing Arch Linux on a MacBook Air 2013]]
-- [[https://medium.com/phils-thought-bubble-of-recent-stuff/arch-linux-running-on-my-macbook-2ea525ebefe3][Arch Linux running on my MacBook]]
-- [[http://codylittlewood.com/arch-linux-on-macbook-pro-installation/][Dual boot Arch Linux on MacBook Pro Installation]]
-
-
-* Footnotes
-
-[fn:1] Key summaries generated by including the =--list-key=,
-=--with-fingerprint=, and =--with-subkey-fingerprint= switches along
-with the key id when calling =gpg=.
-
-* COMMENT Local Variables :ARCHIVE:
-# Local Variables:
-# org-hugo-footer: "\n\n[//]: # \"Exported with love from a post written in Org mode\"\n[//]: # \"- https://ox-hugo.scripter.co\""
-# org-hugo-auto-export-on-save: t
-# End:
projects / ~bandali / bndl.org / blobdiff