1 #+title: sources of aminb.org's pages and posts
4 #+seq_todo: TODO DRAFT DONE
5 #+property: header-args :eval never-export
8 #+macro: abbr @@html:<abbr>$1</abbr>@@
9 #+macro: span @@html:<span class="$1">$2</span>@@
13 :EXPORT_HUGO_SECTION: /
18 :EXPORT_FILE_NAME: _index
21 I'm a [[/uw][graduate student]] in the [[https://watform.uwaterloo.ca][WatForm]] group at University of Waterloo,
22 supervised by [[https://cs.uwaterloo.ca/~nday/][Dr. Nancy Day]]. Currently, my research focuses on formal
23 logic, model checking, and verification.
28 :EXPORT_HUGO_MENU: :menu topnav :weight 10
31 My academic {{{abbr(CV)}}} is available as [[/cv.pdf][cv.pdf]],
32 and an outdated professional resume is available as [[/resume.pdf][resume.pdf]] as
35 I'm interested in functional programming and functional languages,
36 type systems, and formal methods in general. I love writing Haskell
37 and I'm looking into Rust and Lean as well. Feel free to [[/contact][drop me a
38 line]] if you like to geek out about any of the above.
41 CLOSED: [2018-09-04 Tue 10:53]
43 :EXPORT_FILE_NAME: now
44 :EXPORT_HUGO_AUTO_SET_LASTMOD: t
45 :EXPORT_HUGO_MENU: :menu topnav :weight 20
46 :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :customTitle "What I'm doing now"
49 This is my [[https://nownownow.com/about][now page]].
51 I'm currently a [[/uw][graduate student]] in the Waterloo Formal Methods group
52 at University of Waterloo. I just finished my degreeās coursework
53 requirements in Fall 2018, and will be focusing on my thesis starting
54 this term, Winter 2019.
56 In my spare time, I write [[https://www.gnu.org/philosophy/free-sw.en.html][free software]] (see my [[/projects][projects]] page), and
57 tend to various tasks as a GNU webmaster. I've also been picking up
58 the guitar, after giving up on my longtime dream of being a pianist
61 This update was on {{< lastmod >}}.
64 CLOSED: [2019-01-02 Wed 00:32]
66 :EXPORT_FILE_NAME: projects
67 :EXPORT_HUGO_MENU: :menu topnav :weight 30
70 This page is simply a placeholder to generate a menu item, and my
71 server routes this request to cgit.
73 That said, if you /are/ seeing this page, then something has gone
74 wrong; please do get in touch with me!
77 CLOSED: [2018-09-03 Mon 20:44]
79 :EXPORT_FILE_NAME: contact
80 :EXPORT_HUGO_MENU: :menu topnav :weight 40
81 :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :customTitle "Say hello!"
84 #+macro: xmpp @@html:<a href="xmpp:$1">$1</a>@@
86 You can contact me via email or through my accounts on various online
91 Email is my preferred method of communication.
93 - [[mailto:amin@aminb.org][amin@aminb.org]], personal or general inquiries
94 - [[mailto:bandali@gnu.org][bandali@gnu.org]], GNU- or free software-related ([[/gpg][gpg key]])
95 - [[mailto:abandali@uwaterloo.ca][abandali@uwaterloo.ca]], academic or UW-related
99 - irc: bandali on [[https://freenode.net][freenode]] and [[https://wiki.mozilla.org/IRC][moznet]]
100 - xmpp: {{{xmpp(bandali@member.fsf.org)}}}
101 - matrix: [[https://matrix.to/#/@bandali:matrix.org][@bandali:matrix.org]]
102 - fediverse: [[https://pleroma.site/users/aminb][aminb@pleroma.site]]
104 *** Other online places
106 - [[https://git.sr.ht/~bandali][bandali]] on [[https://sr.ht][sr.ht]]
107 - [[https://savannah.gnu.org/users/bandali][bandali]] on Savannah
108 - [[https://lobste.rs/u/bandali][bandali]] on Lobsters
109 - [[https://hackage.haskell.org/user/bandali][bandali]] on Hackage
110 - [[https://gitlab.com/bandali][bandali]] on GitLab
111 - [[https://keybase.io/bandali][bandali]] on Keybase
112 - [[https://news.ycombinator.com/user?id=bandali][bandali]] on HN
113 - [[https://www.reddit.com/u/bandali][bandali]] on Reddit
117 These are accounts I don't use anymore, unless absolutely necessary.
119 - [[https://functional.cafe/@a][a]] on functional.cafe
120 - [[https://mastodon.social/@aminb][aminb]] on mastodon.social
121 - [[https://savannah.gnu.org/users/aminb][aminb]] on Savannah
122 - [[https://hackage.haskell.org/user/aminb][aminb]] on Hackage
123 - [[https://github.com/aminb][aminb]] on GitHub
124 - [[https://www.reddit.com/u/aminb][aminb]] on Reddit
125 - [[https://twitter.com/aminban][aminban]] on Twitter
129 :EXPORT_FILE_NAME: colophon
132 #+macro: light @@html:<label class="light-off-button-inline" for="light-off"></label>@@
133 #+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>@@
134 #+macro: ccbysa-img @@html:<img alt="Creative Commons Licence" style="border-width:0" src="//i.creativecommons.org/l/by-sa/4.0/80x15.png"/>@@
136 This is my personal website, previous versions of which I've ran on
137 different domains since 2012. I've previously used Octopress, Jekyll,
138 a [[https://github.com/aminb/blog-old][custom]] static site generator written in Haskell (kudos to [[https://ruudvanasseldonk.com][Ruud van
139 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
140 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
141 "carefully crafted Org exporter back-end for Hugo" (kudos to [[https://scripter.co][Kaushal
142 Modi]]). I've never been happier with my setup.
144 The sources are available at [[https://aminb.org/projects/aminb.org]].
145 The site is automatically generated on each =git push= using the
146 [[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
147 deployed to my server, where it's served using [[https://www.nginx.com][Nginx]] on [[https://www.debian.org][Debian
152 To toggle night mode, click on {{{light}}}, which is always available
153 on the top navigation menu. It saves its state in a browser cookie,
154 other than that no JavaScript is required to use this website.
156 *** Copyright and Licenses
158 :CUSTOM_ID: copyright
161 The source code for this site is licensed under version 3 (or, at your
162 option, any later version) of the [[https://gnu.org/licenses/gpl.html][GNU General Public License]] (see the
163 [[https://git.sr.ht/~aminb/aminb.org/tree/COPYING][=COPYING=]] file). The contents of the website are licensed under a
164 {{{ccbysa}}} license.
171 The favicons were derived from [[https://psychosoma.tech][nether]]'s beautiful [[https://psychosoma.tech/me/work/i2pangel.png][i2p angel]], a small
172 version of which is displayed on the home page.
176 :EXPORT_FILE_NAME: gpg
179 My [[https://aminb.org/0xA21A020248816103.txt][current key]] is:[fn:1]
182 pub rsa4096 2018-10-17 [C] [expires: 2020-10-16]
183 BE62 7373 8E61 6D6D 1B3A 08E8 A21A 0202 4881 6103
184 uid [ultimate] Amin Bandali <bandali@gnu.org>
185 sub rsa4096 2018-10-17 [S] [expires: 2020-10-16]
186 39B3 3C8D 9448 0D2D DCC2 A498 8B44 A0CD C7B9 56F2
187 sub rsa4096 2018-10-17 [E] [expires: 2020-10-16]
188 43ED 5F7C F5EC CBDF 2552 FE98 1D52 D14E BCF3 BE08
189 sub rsa4096 2018-10-17 [A] [expires: 2020-10-16]
190 70FB 9AAD 5240 2841 2B14 8685 4040 DFEC 6EC1 3F3A
193 My [[https://aminb.org/0xD1FBA36627D65876.txt][previous key]], from which I transitioned away, is:
196 pub rsa4096 2018-08-05 [C] [expires: 2018-11-16]
197 CDDE 75F9 0353 8E71 813C DA27 D1FB A366 27D6 5876
198 uid [ultimate] Amin Bandali <amin@gnu.org>
199 uid [ultimate] Amin Bandali <amin@aminb.org>
200 uid [ultimate] Amin Bandali <mab@gnu.org>
201 uid [ultimate] Amin Bandali <aminb@gnu.org>
202 sub rsa4096 2018-08-05 [S] [expires: 2018-11-16]
203 E14F 56EE 1338 901E A8A8 D2DD 91A9 6FF7 FEF6 BEB4
204 sub rsa4096 2018-08-05 [E] [expires: 2018-11-16]
205 F9B3 BA24 31A0 9B38 31A3 42EF 1F29 83A9 9A69 D453
206 sub rsa4096 2018-08-05 [A] [expires: 2018-11-16]
207 4FB5 D03D A65E 8DA3 39BE 5EDD 6DC3 8F21 4E4B AAA0
210 You can obtain my key transition statement signed with both of the
211 above keys from https://aminb.org/key-transition-2018-10-17.txt.
216 pub rsa4096 2016-01-31 [SC] [expires: 2019-02-13]
217 500C 1D55 D1EC 1FED E8C0 C8DE 4E05 246A B0BF 7FFB
218 uid [ultimate] Amin Bandali <amin@aminb.org>
219 uid [ultimate] Amin Bandali <aminb@gnu.org>
220 uid [ultimate] Amin Bandali <b@nda.li>
221 uid [ultimate] Amin Bandali <me@aminb.org>
222 sub rsa4096 2016-01-31 [S] [expires: 2019-02-13]
223 5AC5 0B1B D540 A902 D4B6 2B5C DAE5 4A52 337F 0283
224 sub rsa4096 2016-01-31 [E] [expires: 2019-02-13]
225 F05B FB25 77C7 5AF6 7783 A66F 3351 056A ACD6 6B1F
226 sub rsa4096 2016-01-31 [A] [expires: 2019-02-13]
227 C165 6BE2 FDCA D028 0D5A 4314 3A4A C417 58E9 C177
230 The key transition statement I'd generated when transitioning away
231 from this key is available on
232 https://aminb.org/key-transition-2018-08-17.txt.
236 :EXPORT_HUGO_SECTION: /
237 :EXPORT_FILE_NAME: search
238 :EXPORT_HUGO_LAYOUT: search
239 :EXPORT_HUGO_OUTPUTS: html json
240 :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :sitemap '((priority . 0.1))
242 Results from static site search implemented using /Fusejs/, /jquery/
243 and /mark.js/. -- [[https://gist.github.com/eddiewebb/735feb48f50f0ddd65ae5606a1cb41ae][Source]]
247 :EXPORT_HUGO_SECTION: post
248 :EXPORT_HUGO_AUTO_SET_LASTMOD: t
251 ** Arch GNU/Linux on MacBook Air 2013 :arch:macbook:
253 :EXPORT_FILE_NAME: arch-macbook-air
254 :EXPORT_DATE: 2016-11-01
255 :EXPORT_OPTIONS: ^:{}
256 :EXPORT_HUGO_ALIASES: /2016/11/arch-macbook-air
257 :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :toc true
260 This post summarizes how I install and dual-boot Arch GNU/Linux with
261 Full-Disk Encryption alongside macOS. It is not meant to be a
262 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]].
263 Rather, it mostly serves as a small summary with a few useful notes
266 So, make sure you understand what you type into your terminal. If you
267 don't, checking out the Arch wiki should probably be your first step.
269 /Note:/ you will need internet access throughout the installation and
270 the MacBook Air's WiFi doesn't work out of the box on Arch. I
271 recommend using your phone's USB Tethering (if it does support it), or
272 using an Ethernet-USB adapter.
274 *** Shrinking the macOS partition
276 The first step I take is resizing the HFS+ macOS partition to make
277 room for the new {{{abbr(GNU/Linux)}}} installation. There are plenty
278 of tutorials on how to do this using macOS's Disk Utility, so do that
281 *** Creating a bootable Arch Installer USB
283 There are different ways of creating a bootable Arch USB, all
284 documented on the [[https://wiki.archlinux.org/index.php/USB_flash_installation_media][USB flash installation media]] page on the Arch wiki,
285 but the simplest one is using =dd= if you already have access to
288 {{{span(red,Warning:)}}} make sure you backup the data on your flash
289 drive, as =dd= will irrevocably destroy all data on it.
291 Use =lsblk= to find the name (block device) of your USB drive, then
292 run =dd= (as root) as shown below:
295 dd bs=4M if=/path/to/archlinux.iso of=/dev/sdx status=progress && sync
298 Replace =/path/to/archlinux.iso= with the path to the Arch image you
299 have downloaded, and =/dev/sdx= with your drive.
301 *** Booting up from the USB
303 After creating the install USB, reboot your laptop and hold the alt
304 key and boot into the USB.
306 When booting is complete and you're presented with the prompt, it's a
307 good time to make sure you're connected to the internet (see the
308 /note/ at the top of this post).
310 Use =ping= to verify that you've established a connection:
316 *** Updating the system clock
318 Once you're connected to the internet, make sure the system clock is
322 timedatectl set-ntp true # start and enable systemd-timesyncd
325 You can check the service status using =timedatectl status=.
329 :CUSTOM_ID: partitioning
332 I won't dive into partitioning and instead, I'll refer you to the
333 [[https://wiki.archlinux.org/index.php/Partitioning][Partitioning]] page of Arch wiki. Of the available partitioning tools, I
334 personally prefer =cfdisk=.
336 *** Setting up LVM & LUKS
338 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
341 First, let's set up the underlying encrypted partition:
344 cryptsetup -v --cipher aes-xts-plain64 --key-size 512 --hash sha512 \
345 --iter-time 5000 --use-urandom -y luksFormat /dev/sdaX
348 where =/dev/sdaX= is the partition you created in the last step
349 (e.g. =/dev/sda4=). For more information about the =cryptsetup=
350 options, see the [[https://wiki.archlinux.org/index.php/Dm-crypt/Device_encryption#Encryption_options_for_LUKS_mode][LUKS encryption options]].
352 Then we open the container:
355 cryptsetup open --type luks /dev/sdaX lvm
358 Now it's time to use lvm and prepare the logical volume(s):
361 pvcreate /dev/mapper/lvm
362 vgcreate vg /dev/mapper/lvm
363 lvcreate --extents +100%FREE -n root vg
366 This will create a physical volume on the mapping we just opened,
367 create a volume group named =vg= on the physical volume, and create a
368 logical volume named =root= that spans the entire volume group. More
369 complex setups are possible thanks to the great flexibility of lvm.
371 We now format the logical volume with =ext4=:
374 mkfs.ext4 /dev/mapper/vg-root
377 *** Installing the base system
379 Let's mount the logical volume, make a directory for the mount point
380 of the boot partition, and mount the boot partition (=/dev/sda1=):
383 mount /dev/mapper/vg-root /mnt
385 mount /dev/sda1 /mnt/boot
388 Finally, let's install the base system (and optionally =base-devel=):
391 pacstrap /mnt base base-devel
394 *** Configuring the system
396 Let's generate the fstab:
399 genfstab -U /mnt >> /mnt/etc/fstab
402 Use your favorite terminal-based editor, edit the fstab file and add
403 the =discard= option for the root partition to enable TRIM on the SSD.
405 Now we change root into our newly installed system and will configure
406 it. Adjust these according to your own setup.
409 arch-chroot /mnt /bin/bash
410 passwd # set the root password
411 echo myhostname > /etc/hostname # set the hostname
412 ln -s /usr/share/zoneinfo/Canada/Eastern /etc/localtime # time zone
413 hwclock --systohc --utc # write system clock to hardware clock (UTC)
414 useradd -m -G wheel -s /bin/bash myuser # create myuser
415 passwd myuser # set the password for myuser
416 echo "myuser ALL=(ALL) NOPASSWD: ALL" >> /etc/sudoers.d/myuser
417 # uncomment en_US.UTF-8 UTF-8 and other needed locales in /etc/locale.gen
419 echo LANG=en_US.UTF-8 > /etc/locale.conf
420 export LANG=en_US.UTF-8
423 Then adjust the initramfs hooks in =/etc/mkinitcpio.conf= and enable
424 the =encrypt= and =lvm2= hooks, and make sure =keyboard= is available
425 before =encrypt= so you can actually type in the LUKS password when
426 booting. Your =HOOKS= line should look similar to this:
429 HOOKS="base udev autodetect modconf block keyboard encrypt lvm2 filesystems fsck"
432 After adjusting the hooks, build the initramfs:
438 Now, install the =intel-ucode= package. We'll configure the bootloader
439 to enable intel microcode updates.
442 pacman -S intel-ucode
445 Create the =/boot/loader/loader.conf= with the following content
446 (adjust the timeout to your liking):
453 Then create the entry for Arch:
456 mkdir -p /boot/loader/entries
457 touch /boot/loader/entries/arch.conf
460 Now edit =/boot/loader/entries/arch.conf= to specify the Arch entry:
465 initrd /intel-ucode.img
466 initrd /initramfs-linux.img
467 options cryptdevice=/dev/sdaX:vg:allow-discards root=/dev/mapper/vg-root rw
470 Again, =/dev/sdaX= is the partition you created in the [[#partitioning][partitioning]]
471 step as the underlying encrypted partition.
473 Finally, install the bootloader, exit the chroot, umount and reboot!
482 *** Post-installation recommendations
484 Congratulations! You now have a minimal Arch installation.
486 At this point, I usually install my favorite AUR helper, [[https://aur.archlinux.org/packages/pacaur/][pacaur]], then
487 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]]
488 backlight driver to fix the post suspend/resume issue where three's no
489 brightness after waking up from suspend, and the only available
490 brightness would be 100%.
493 pacaur -S linux-headers dkms # linux-headers is required for dkms
494 pacaur -S broadcom-wl-dkms
495 pacaur -S mba6x_bl-dkms
498 Then, I'd like to install
500 - input, graphics, and sound drivers,
501 - a desktop environment (I prefer Xfce or LXQt),
502 - a display manager for login screen (lightdm or sddm), and
503 - a network manager (NetworkManager or ConnMan).
505 Check out the [[https://wiki.archlinux.org/index.php/General_recommendations][General recommendations]] for more details.
509 Here are some resources I've come across each with lots of useful bits
510 and pieces, about installing Arch on a MacBook:
512 - [[https://github.com/pandeiro/arch-on-air][pandeiro/arch-on-air]]
513 - [[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]]
514 - [[http://frankshin.com/installing-archlinux-on-macbook-air-2013/][Installing Archlinux on Macbook Air 2013]]
515 - [[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)]]
516 - [[https://visual-assault.org/2016/03/05/install-encrypted-arch-linux-on-apple-macbook-pro/][Installing (encrypted) Arch Linux on an Apple MacBook Pro]]
517 - [[http://alexeyzabelin.com/arch-on-mac][Installing Arch Linux on a MacBook Air 2013]]
518 - [[https://medium.com/phils-thought-bubble-of-recent-stuff/arch-linux-running-on-my-macbook-2ea525ebefe3][Arch Linux running on my MacBook]]
519 - [[http://codylittlewood.com/arch-linux-on-macbook-pro-installation/][Dual boot Arch Linux on MacBook Pro Installation]]
524 [fn:1] Key summaries generated by including the =--list-key=,
525 =--with-fingerprint=, and =--with-subkey-fingerprint= switches along
526 with the key id when calling =gpg=.
528 * COMMENT Local Variables :ARCHIVE:
530 # org-hugo-footer: "\n\n[//]: # \"Exported with love from a post written in Org mode\"\n[//]: # \"- https://ox-hugo.scripter.co\""
531 # org-hugo-auto-export-on-save: t