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]]. I'm interested in using formal methods,
23 especially type systems, to help make software more reliable.
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 doing my third semester as a [[/uw][graduate student]] in the
52 Waterloo Formal Methods group at University of Waterloo. I'm also
53 TA'ing [[https://www.student.cs.uwaterloo.ca/~se212/][SE 212: Logic and Computation]], taught by my supervisor, Nancy.
55 In my spare time, I write [[https://www.gnu.org/philosophy/free-sw.en.html][free software]] (projects page coming soon),
56 and tend to various tasks as a GNU webmaster. I've also been picking
57 up the guitar, after giving up on my longtime dream of being a
58 pianist, at least for now.
60 This update was on {{< lastmod >}}.
65 CLOSED: [2018-09-03 Mon 20:44]
67 :EXPORT_FILE_NAME: contact
68 :EXPORT_HUGO_MENU: :menu topnav :weight 40
69 :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :customTitle "Say hello!"
72 #+macro: xmpp @@html:<a href="xmpp:$1">$1</a>@@
74 You can contact me via email or through my accounts on various online
79 Email is my preferred method of communication.
81 - [[mailto:amin@aminb.org][amin@aminb.org]], personal or general inquiries
82 - [[mailto:bandali@gnu.org][bandali@gnu.org]], GNU- or free software-related ([[/gpg][gpg key]])
83 - [[mailto:abandali@uwaterloo.ca][abandali@uwaterloo.ca]], academic or UW-related
87 - irc: bandali on [[https://freenode.net][freenode]] and [[https://wiki.mozilla.org/IRC][moznet]]
88 - xmpp: {{{xmpp(bandali@member.fsf.org)}}}
89 - matrix: [[https://matrix.to/#/@bandali:matrix.org][@bandali:matrix.org]]
90 - fediverse: [[https://pleroma.site/users/aminb][aminb@pleroma.site]]
92 *** Other online places
94 - [[https://git.sr.ht/~bandali][bandali]] on [[https://sr.ht][sr.ht]]
95 - [[https://savannah.gnu.org/users/bandali][bandali]] on Savannah
96 - [[https://lobste.rs/u/bandali][bandali]] on Lobsters
97 - [[https://hackage.haskell.org/user/bandali][bandali]] on Hackage
98 - [[https://gitlab.com/bandali][bandali]] on GitLab
99 - [[https://keybase.io/bandali][bandali]] on Keybase
100 - [[https://news.ycombinator.com/user?id=bandali][bandali]] on HN
101 - [[https://www.reddit.com/u/bandali][bandali]] on Reddit
105 These are accounts I don't use anymore, unless absolutely necessary.
107 - [[https://functional.cafe/@a][a]] on functional.cafe
108 - [[https://mastodon.social/@aminb][aminb]] on mastodon.social
109 - [[https://savannah.gnu.org/users/aminb][aminb]] on Savannah
110 - [[https://hackage.haskell.org/user/aminb][aminb]] on Hackage
111 - [[https://github.com/aminb][aminb]] on GitHub
112 - [[https://www.reddit.com/u/aminb][aminb]] on Reddit
113 - [[https://twitter.com/aminban][aminban]] on Twitter
117 :EXPORT_FILE_NAME: colophon
120 #+macro: light @@html:<label class="light-off-button-inline" for="light-off"></label>@@
121 #+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>@@
122 #+macro: ccbysa-img @@html:<img alt="Creative Commons Licence" style="border-width:0" src="//i.creativecommons.org/l/by-sa/4.0/80x15.png"/>@@
124 This is my personal website, previous versions of which I've ran on
125 different domains since 2012. I've previously used Octopress, Jekyll,
126 a [[https://github.com/aminb/blog-old][custom]] static site generator written in Haskell (kudos to [[https://ruudvanasseldonk.com][Ruud van
127 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
128 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
129 "carefully crafted Org exporter back-end for Hugo" (kudos to [[https://scripter.co][Kaushal
130 Modi]]). I've never been happier with my setup.
132 The sources are available on [[https://git.sr.ht/~bandali/aminb.org]].
133 The site is automatically generated on each =git push= using the
134 [[https://builds.sr.ht][builds.sr.ht]] service (see the [[https://git.sr.ht/~bandali/aminb.org/tree/master/.build.yml][=.build.yml=]] build manifest) and is
135 deployed to my server, where it's served by [[https://www.nginx.com][Nginx]] on [[https://www.debian.org][Debian GNU/Linux]].
139 To toggle night mode, click on {{{light}}}, which is always available
140 on the top navigation menu. It saves its state in a browser cookie,
141 other than that no JavaScript is required to use this website.
143 *** Copyright and Licenses
145 :CUSTOM_ID: copyright
148 The source code for this site is licensed under version 3 (or, at your
149 option, any later version) of the [[https://gnu.org/licenses/gpl.html][GNU General Public License]] (see the
150 [[https://git.sr.ht/~aminb/aminb.org/tree/COPYING][=COPYING=]] file). The contents of the website are licensed under a
151 {{{ccbysa}}} license.
158 The favicons were derived from [[https://psychosoma.tech][nether]]'s beautiful [[https://psychosoma.tech/me/work/i2pangel.png][i2p angel]], a small
159 version of which is displayed on the home page.
163 :EXPORT_FILE_NAME: gpg
166 My [[https://aminb.org/0xA21A020248816103.txt][current key]] is:[fn:1]
169 pub rsa4096 2018-10-17 [C] [expires: 2020-10-16]
170 BE62 7373 8E61 6D6D 1B3A 08E8 A21A 0202 4881 6103
171 uid [ultimate] Amin Bandali <bandali@gnu.org>
172 sub rsa4096 2018-10-17 [S] [expires: 2020-10-16]
173 39B3 3C8D 9448 0D2D DCC2 A498 8B44 A0CD C7B9 56F2
174 sub rsa4096 2018-10-17 [E] [expires: 2020-10-16]
175 43ED 5F7C F5EC CBDF 2552 FE98 1D52 D14E BCF3 BE08
176 sub rsa4096 2018-10-17 [A] [expires: 2020-10-16]
177 70FB 9AAD 5240 2841 2B14 8685 4040 DFEC 6EC1 3F3A
180 My [[https://aminb.org/0xD1FBA36627D65876.txt][previous key]], from which I transitioned away, is:
183 pub rsa4096 2018-08-05 [C] [expires: 2018-11-16]
184 CDDE 75F9 0353 8E71 813C DA27 D1FB A366 27D6 5876
185 uid [ultimate] Amin Bandali <amin@gnu.org>
186 uid [ultimate] Amin Bandali <amin@aminb.org>
187 uid [ultimate] Amin Bandali <mab@gnu.org>
188 uid [ultimate] Amin Bandali <aminb@gnu.org>
189 sub rsa4096 2018-08-05 [S] [expires: 2018-11-16]
190 E14F 56EE 1338 901E A8A8 D2DD 91A9 6FF7 FEF6 BEB4
191 sub rsa4096 2018-08-05 [E] [expires: 2018-11-16]
192 F9B3 BA24 31A0 9B38 31A3 42EF 1F29 83A9 9A69 D453
193 sub rsa4096 2018-08-05 [A] [expires: 2018-11-16]
194 4FB5 D03D A65E 8DA3 39BE 5EDD 6DC3 8F21 4E4B AAA0
197 You can obtain my key transition statement signed with both of the
198 above keys from https://aminb.org/key-transition-2018-10-17.txt.
203 pub rsa4096 2016-01-31 [SC] [expires: 2019-02-13]
204 500C 1D55 D1EC 1FED E8C0 C8DE 4E05 246A B0BF 7FFB
205 uid [ultimate] Amin Bandali <amin@aminb.org>
206 uid [ultimate] Amin Bandali <aminb@gnu.org>
207 uid [ultimate] Amin Bandali <b@nda.li>
208 uid [ultimate] Amin Bandali <me@aminb.org>
209 sub rsa4096 2016-01-31 [S] [expires: 2019-02-13]
210 5AC5 0B1B D540 A902 D4B6 2B5C DAE5 4A52 337F 0283
211 sub rsa4096 2016-01-31 [E] [expires: 2019-02-13]
212 F05B FB25 77C7 5AF6 7783 A66F 3351 056A ACD6 6B1F
213 sub rsa4096 2016-01-31 [A] [expires: 2019-02-13]
214 C165 6BE2 FDCA D028 0D5A 4314 3A4A C417 58E9 C177
217 The key transition statement I'd generated when transitioning away
218 from this key is available on
219 https://aminb.org/key-transition-2018-08-17.txt.
223 :EXPORT_HUGO_SECTION: /
224 :EXPORT_FILE_NAME: search
225 :EXPORT_HUGO_LAYOUT: search
226 :EXPORT_HUGO_OUTPUTS: html json
227 :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :sitemap '((priority . 0.1))
229 Results from static site search implemented using /Fusejs/, /jquery/
230 and /mark.js/. -- [[https://gist.github.com/eddiewebb/735feb48f50f0ddd65ae5606a1cb41ae][Source]]
234 :EXPORT_HUGO_SECTION: post
235 :EXPORT_HUGO_AUTO_SET_LASTMOD: t
238 ** Arch GNU/Linux on MacBook Air 2013 :arch:macbook:
240 :EXPORT_FILE_NAME: arch-macbook-air
241 :EXPORT_DATE: 2016-11-01
242 :EXPORT_OPTIONS: ^:{}
243 :EXPORT_HUGO_ALIASES: /2016/11/arch-macbook-air
244 :EXPORT_HUGO_CUSTOM_FRONT_MATTER: :toc true
247 This post summarizes how I install and dual-boot Arch GNU/Linux with
248 Full-Disk Encryption alongside macOS. It is not meant to be a
249 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]].
250 Rather, it mostly serves as a small summary with a few useful notes
253 So, make sure you understand what you type into your terminal. If you
254 don't, checking out the Arch wiki should probably be your first step.
256 /Note:/ you will need internet access throughout the installation and
257 the MacBook Air's WiFi doesn't work out of the box on Arch. I
258 recommend using your phone's USB Tethering (if it does support it), or
259 using an Ethernet-USB adapter.
261 *** Shrinking the macOS partition
263 The first step I take is resizing the HFS+ macOS partition to make
264 room for the new {{{abbr(GNU/Linux)}}} installation. There are plenty
265 of tutorials on how to do this using macOS's Disk Utility, so do that
268 *** Creating a bootable Arch Installer USB
270 There are different ways of creating a bootable Arch USB, all
271 documented on the [[https://wiki.archlinux.org/index.php/USB_flash_installation_media][USB flash installation media]] page on the Arch wiki,
272 but the simplest one is using =dd= if you already have access to
275 {{{span(red,Warning:)}}} make sure you backup the data on your flash
276 drive, as =dd= will irrevocably destroy all data on it.
278 Use =lsblk= to find the name (block device) of your USB drive, then
279 run =dd= (as root) as shown below:
282 dd bs=4M if=/path/to/archlinux.iso of=/dev/sdx status=progress && sync
285 Replace =/path/to/archlinux.iso= with the path to the Arch image you
286 have downloaded, and =/dev/sdx= with your drive.
288 *** Booting up from the USB
290 After creating the install USB, reboot your laptop and hold the alt
291 key and boot into the USB.
293 When booting is complete and you're presented with the prompt, it's a
294 good time to make sure you're connected to the internet (see the
295 /note/ at the top of this post).
297 Use =ping= to verify that you've established a connection:
303 *** Updating the system clock
305 Once you're connected to the internet, make sure the system clock is
309 timedatectl set-ntp true # start and enable systemd-timesyncd
312 You can check the service status using =timedatectl status=.
316 :CUSTOM_ID: partitioning
319 I won't dive into partitioning and instead, I'll refer you to the
320 [[https://wiki.archlinux.org/index.php/Partitioning][Partitioning]] page of Arch wiki. Of the available partitioning tools, I
321 personally prefer =cfdisk=.
323 *** Setting up LVM & LUKS
325 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
328 First, let's set up the underlying encrypted partition:
331 cryptsetup -v --cipher aes-xts-plain64 --key-size 512 --hash sha512 \
332 --iter-time 5000 --use-urandom -y luksFormat /dev/sdaX
335 where =/dev/sdaX= is the partition you created in the last step
336 (e.g. =/dev/sda4=). For more information about the =cryptsetup=
337 options, see the [[https://wiki.archlinux.org/index.php/Dm-crypt/Device_encryption#Encryption_options_for_LUKS_mode][LUKS encryption options]].
339 Then we open the container:
342 cryptsetup open --type luks /dev/sdaX lvm
345 Now it's time to use lvm and prepare the logical volume(s):
348 pvcreate /dev/mapper/lvm
349 vgcreate vg /dev/mapper/lvm
350 lvcreate --extents +100%FREE -n root vg
353 This will create a physical volume on the mapping we just opened,
354 create a volume group named =vg= on the physical volume, and create a
355 logical volume named =root= that spans the entire volume group. More
356 complex setups are possible thanks to the great flexibility of lvm.
358 We now format the logical volume with =ext4=:
361 mkfs.ext4 /dev/mapper/vg-root
364 *** Installing the base system
366 Let's mount the logical volume, make a directory for the mount point
367 of the boot partition, and mount the boot partition (=/dev/sda1=):
370 mount /dev/mapper/vg-root /mnt
372 mount /dev/sda1 /mnt/boot
375 Finally, let's install the base system (and optionally =base-devel=):
378 pacstrap /mnt base base-devel
381 *** Configuring the system
383 Let's generate the fstab:
386 genfstab -U /mnt >> /mnt/etc/fstab
389 Use your favorite terminal-based editor, edit the fstab file and add
390 the =discard= option for the root partition to enable TRIM on the SSD.
392 Now we change root into our newly installed system and will configure
393 it. Adjust these according to your own setup.
396 arch-chroot /mnt /bin/bash
397 passwd # set the root password
398 echo myhostname > /etc/hostname # set the hostname
399 ln -s /usr/share/zoneinfo/Canada/Eastern /etc/localtime # time zone
400 hwclock --systohc --utc # write system clock to hardware clock (UTC)
401 useradd -m -G wheel -s /bin/bash myuser # create myuser
402 passwd myuser # set the password for myuser
403 echo "myuser ALL=(ALL) NOPASSWD: ALL" >> /etc/sudoers.d/myuser
404 # uncomment en_US.UTF-8 UTF-8 and other needed locales in /etc/locale.gen
406 echo LANG=en_US.UTF-8 > /etc/locale.conf
407 export LANG=en_US.UTF-8
410 Then adjust the initramfs hooks in =/etc/mkinitcpio.conf= and enable
411 the =encrypt= and =lvm2= hooks, and make sure =keyboard= is available
412 before =encrypt= so you can actually type in the LUKS password when
413 booting. Your =HOOKS= line should look similar to this:
416 HOOKS="base udev autodetect modconf block keyboard encrypt lvm2 filesystems fsck"
419 After adjusting the hooks, build the initramfs:
425 Now, install the =intel-ucode= package. We'll configure the bootloader
426 to enable intel microcode updates.
429 pacman -S intel-ucode
432 Create the =/boot/loader/loader.conf= with the following content
433 (adjust the timeout to your liking):
440 Then create the entry for Arch:
443 mkdir -p /boot/loader/entries
444 touch /boot/loader/entries/arch.conf
447 Now edit =/boot/loader/entries/arch.conf= to specify the Arch entry:
452 initrd /intel-ucode.img
453 initrd /initramfs-linux.img
454 options cryptdevice=/dev/sdaX:vg:allow-discards root=/dev/mapper/vg-root rw
457 Again, =/dev/sdaX= is the partition you created in the [[#partitioning][partitioning]]
458 step as the underlying encrypted partition.
460 Finally, install the bootloader, exit the chroot, umount and reboot!
469 *** Post-installation recommendations
471 Congratulations! You now have a minimal Arch installation.
473 At this point, I usually install my favorite AUR helper, [[https://aur.archlinux.org/packages/pacaur/][pacaur]], then
474 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]]
475 backlight driver to fix the post suspend/resume issue where three's no
476 brightness after waking up from suspend, and the only available
477 brightness would be 100%.
480 pacaur -S linux-headers dkms # linux-headers is required for dkms
481 pacaur -S broadcom-wl-dkms
482 pacaur -S mba6x_bl-dkms
485 Then, I'd like to install
487 - input, graphics, and sound drivers,
488 - a desktop environment (I prefer Xfce or LXQt),
489 - a display manager for login screen (lightdm or sddm), and
490 - a network manager (NetworkManager or ConnMan).
492 Check out the [[https://wiki.archlinux.org/index.php/General_recommendations][General recommendations]] for more details.
496 Here are some resources I've come across each with lots of useful bits
497 and pieces, about installing Arch on a MacBook:
499 - [[https://github.com/pandeiro/arch-on-air][pandeiro/arch-on-air]]
500 - [[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]]
501 - [[http://frankshin.com/installing-archlinux-on-macbook-air-2013/][Installing Archlinux on Macbook Air 2013]]
502 - [[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)]]
503 - [[https://visual-assault.org/2016/03/05/install-encrypted-arch-linux-on-apple-macbook-pro/][Installing (encrypted) Arch Linux on an Apple MacBook Pro]]
504 - [[http://alexeyzabelin.com/arch-on-mac][Installing Arch Linux on a MacBook Air 2013]]
505 - [[https://medium.com/phils-thought-bubble-of-recent-stuff/arch-linux-running-on-my-macbook-2ea525ebefe3][Arch Linux running on my MacBook]]
506 - [[http://codylittlewood.com/arch-linux-on-macbook-pro-installation/][Dual boot Arch Linux on MacBook Pro Installation]]
511 [fn:1] Key summaries generated by including the =--list-key=,
512 =--with-fingerprint=, and =--with-subkey-fingerprint= switches along
513 with the key id when calling =gpg=.
515 * COMMENT Local Variables :ARCHIVE:
517 # org-hugo-footer: "\n\n[//]: # \"Exported with love from a post written in Org mode\"\n[//]: # \"- https://ox-hugo.scripter.co\""
518 # org-hugo-auto-export-on-save: t