add GNU Inside badge
[~bandali/bndl.org] / content-org / aminb.org
CommitLineData
caf3b78c
AB
1#+title: sources of aminb.org's pages and posts
2
3#+hugo_base_dir: ..
4#+seq_todo: TODO DRAFT DONE
5#+property: header-args :eval never-export
6#+options: author:nil
7
8#+macro: abbr @@html:<abbr>$1</abbr>@@
9#+macro: span @@html:<span class="$1">$2</span>@@
10
bdec7790 11* Pages
ae39b0da
AB
12:PROPERTIES:
13:EXPORT_HUGO_SECTION: /
bdec7790
AB
14:END:
15
16** Home
17:PROPERTIES:
ae39b0da
AB
18:EXPORT_FILE_NAME: _index
19:END:
20
21I'm a [[/uw][graduate student]] in the [[https://watform.uwaterloo.ca][WatForm]] group at University of Waterloo,
22supervised by [[https://cs.uwaterloo.ca/~nday/][Dr. Nancy Day]]. I'm interested in using formal methods,
23especially type systems, to help make software more reliable.
24
caf3b78c
AB
25** CV
26:PROPERTIES:
27:EXPORT_FILE_NAME: cv
bdec7790 28:EXPORT_HUGO_MENU: :menu topnav :weight 10
caf3b78c
AB
29:END:
30
31My academic {{{abbr(CV)}}} is available as [[/cv.pdf][cv.pdf]],
32and an outdated professional resume is available as [[/resume.pdf][resume.pdf]] as
33well.
34
35I'm interested in functional programming and functional languages,
36type systems, and formal methods in general. I love writing Haskell
37and I'm looking into Rust and Lean as well. Feel free to [[/contact][drop me a
38line]] if you like to geek out about any of the above.
39
345fdf43
AB
40** DONE Now
41CLOSED: [2018-09-04 Tue 10:53]
42:PROPERTIES:
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"
47:END:
48
49This is my [[https://nownownow.com/about][now page]].
50
51I'm currently doing my third semester as a [[/uw][graduate student]] in the
52Waterloo Formal Methods group at University of Waterloo. I'm also
53TA'ing [[https://www.student.cs.uwaterloo.ca/~se212/][SE 212: Logic and Computation]], taught by my supervisor, Nancy.
54
55In my spare time, I write [[https://www.gnu.org/philosophy/free-sw.en.html][free software]] (projects page coming soon),
56and tend to various tasks as a GNU webmaster. I've also been picking
57up the guitar, after giving up on my longtime dream of being a
58pianist, at least for now.
59
60This update was on {{< lastmod >}}.
caf3b78c
AB
61
62** TODO Projects
63
d6fab81a
AB
64** DONE Contact
65CLOSED: [2018-09-03 Mon 20:44]
66:PROPERTIES:
67:EXPORT_FILE_NAME: contact
bdec7790 68:EXPORT_HUGO_MENU: :menu topnav :weight 40
d6fab81a
AB
69:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :customTitle "Say hello!"
70:END:
71
72#+macro: xmpp @@html:<a href="xmpp:$1">$1</a>@@
73
74You can contact me via email or through my accounts on various online
75platforms.
76
6f99381c 77*** Primary
d6fab81a 78
6f99381c
AB
79Email is my preferred method of communication.
80
81- [[mailto:amin@aminb.org][amin@aminb.org]], personal or general inquiries
f052da50 82- [[mailto:bandali@gnu.org][bandali@gnu.org]], GNU- or free software-related ([[/gpg][gpg key]])
6f99381c 83- [[mailto:abandali@uwaterloo.ca][abandali@uwaterloo.ca]], academic or UW-related
6f99381c
AB
84
85*** Secondary
86
87- irc: bandali on [[https://freenode.net][freenode]] and [[https://wiki.mozilla.org/IRC][moznet]]
f052da50 88- xmpp: {{{xmpp(bandali@member.fsf.org)}}}
ed1b80bb 89- matrix: [[https://matrix.to/#/@bandali:matrix.org][@bandali:matrix.org]]
f052da50 90- fediverse: [[https://pleroma.site/users/aminb][aminb@pleroma.site]]
d6fab81a
AB
91
92*** Other online places
93
c8dc487a
AB
94- [[https://git.sr.ht/~bandali][bandali]] on [[https://sr.ht][sr.ht]]
95- [[https://savannah.gnu.org/users/bandali][bandali]] on Savannah
30827978 96- [[https://lobste.rs/u/bandali][bandali]] on Lobsters
32d82dc5 97- [[https://hackage.haskell.org/user/bandali][bandali]] on Hackage
30827978
AB
98- [[https://gitlab.com/bandali][bandali]] on GitLab
99- [[https://keybase.io/bandali][bandali]] on Keybase
ff88e9ad 100- [[https://news.ycombinator.com/user?id=bandali][bandali]] on HN
6f99381c
AB
101- [[https://www.reddit.com/u/bandali][bandali]] on Reddit
102
103*** Dormant accounts
104
105These are accounts I don't use anymore, unless absolutely necessary.
106
107- [[https://functional.cafe/@a][a]] on functional.cafe
108- [[https://mastodon.social/@aminb][aminb]] on mastodon.social
c8dc487a 109- [[https://savannah.gnu.org/users/aminb][aminb]] on Savannah
32d82dc5 110- [[https://hackage.haskell.org/user/aminb][aminb]] on Hackage
6f99381c
AB
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
caf3b78c 114
eac9e3d2
AB
115** Colophon
116:PROPERTIES:
117:EXPORT_FILE_NAME: colophon
eac9e3d2
AB
118:END:
119
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"/>@@
123
124This is my personal website, previous versions of which I've ran on
3f126e4c
AB
125different domains since 2012. I've previously used Octopress, Jekyll,
126a [[https://github.com/aminb/blog-old][custom]] static site generator written in Haskell (kudos to [[https://ruudvanasseldonk.com][Ruud van
af0b7ec5
AB
127Asseldonk]]), [[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
128also [[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
3f126e4c
AB
129"carefully crafted Org exporter back-end for Hugo" (kudos to [[https://scripter.co][Kaushal
130Modi]]). I've never been happier with my setup.
131
132The sources are available on [[https://git.sr.ht/~bandali/aminb.org]].
133The 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
eac9e3d2
AB
135deployed to my server, where it's served by [[https://www.nginx.com][Nginx]] on [[https://www.debian.org][Debian GNU/Linux]].
136
137*** Night mode
138
139To toggle night mode, click on {{{light}}}, which is always available
140on the top navigation menu. It saves its state in a browser cookie,
141other than that no JavaScript is required to use this website.
142
143*** Copyright and Licenses
144:PROPERTIES:
145:CUSTOM_ID: copyright
146:END:
147
148The source code for this site is licensed under version 3 (or, at your
149option, 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.
152
84421557
AB
153*** i2p angel
154:PROPERTIES:
155:CUSTOM_ID: i2pangel
156:END:
157
158The favicons were derived from [[https://psychosoma.tech][nether]]'s beautiful [[https://psychosoma.tech/me/work/i2pangel.png][i2p angel]], a small
159version of which is displayed on the home page.
160
f052da50
AB
161** GPG
162:PROPERTIES:
163:EXPORT_FILE_NAME: gpg
164:END:
165
166My [[https://aminb.org/0xA21A020248816103.txt][current key]] is:[fn:1]
167
168#+begin_src txt
169pub rsa4096 2018-10-17 [C] [expires: 2020-10-16]
170 BE62 7373 8E61 6D6D 1B3A 08E8 A21A 0202 4881 6103
171uid [ultimate] Amin Bandali <bandali@gnu.org>
172sub rsa4096 2018-10-17 [S] [expires: 2020-10-16]
173 39B3 3C8D 9448 0D2D DCC2 A498 8B44 A0CD C7B9 56F2
174sub rsa4096 2018-10-17 [E] [expires: 2020-10-16]
175 43ED 5F7C F5EC CBDF 2552 FE98 1D52 D14E BCF3 BE08
176sub rsa4096 2018-10-17 [A] [expires: 2020-10-16]
177 70FB 9AAD 5240 2841 2B14 8685 4040 DFEC 6EC1 3F3A
178#+end_src
179
180My [[https://aminb.org/0xD1FBA36627D65876.txt][previous key]], from which I transitioned away, is:
181
182#+begin_src txt
183pub rsa4096 2018-08-05 [C] [expires: 2018-11-16]
184 CDDE 75F9 0353 8E71 813C DA27 D1FB A366 27D6 5876
185uid [ultimate] Amin Bandali <amin@gnu.org>
186uid [ultimate] Amin Bandali <amin@aminb.org>
187uid [ultimate] Amin Bandali <mab@gnu.org>
188uid [ultimate] Amin Bandali <aminb@gnu.org>
189sub rsa4096 2018-08-05 [S] [expires: 2018-11-16]
190 E14F 56EE 1338 901E A8A8 D2DD 91A9 6FF7 FEF6 BEB4
191sub rsa4096 2018-08-05 [E] [expires: 2018-11-16]
192 F9B3 BA24 31A0 9B38 31A3 42EF 1F29 83A9 9A69 D453
193sub rsa4096 2018-08-05 [A] [expires: 2018-11-16]
194 4FB5 D03D A65E 8DA3 39BE 5EDD 6DC3 8F21 4E4B AAA0
195#+end_src
196
197You can obtain my key transition statement signed with both of the
198above keys from https://aminb.org/key-transition-2018-10-17.txt.
199
200*** Older keys
201
202#+begin_src txt
203pub rsa4096 2016-01-31 [SC] [expires: 2019-02-13]
204 500C 1D55 D1EC 1FED E8C0 C8DE 4E05 246A B0BF 7FFB
205uid [ultimate] Amin Bandali <amin@aminb.org>
206uid [ultimate] Amin Bandali <aminb@gnu.org>
207uid [ultimate] Amin Bandali <b@nda.li>
208uid [ultimate] Amin Bandali <me@aminb.org>
209sub rsa4096 2016-01-31 [S] [expires: 2019-02-13]
210 5AC5 0B1B D540 A902 D4B6 2B5C DAE5 4A52 337F 0283
211sub rsa4096 2016-01-31 [E] [expires: 2019-02-13]
212 F05B FB25 77C7 5AF6 7783 A66F 3351 056A ACD6 6B1F
213sub rsa4096 2016-01-31 [A] [expires: 2019-02-13]
214 C165 6BE2 FDCA D028 0D5A 4314 3A4A C417 58E9 C177
215#+end_src
216
217The key transition statement I'd generated when transitioning away
218from this key is available on
219https://aminb.org/key-transition-2018-08-17.txt.
220
bdec7790
AB
221** Search
222:PROPERTIES:
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))
228:END:
229Results from static site search implemented using /Fusejs/, /jquery/
230and /mark.js/. -- [[https://gist.github.com/eddiewebb/735feb48f50f0ddd65ae5606a1cb41ae][Source]]
231
caf3b78c
AB
232* Posts
233:PROPERTIES:
234:EXPORT_HUGO_SECTION: post
ae39b0da 235:EXPORT_HUGO_AUTO_SET_LASTMOD: t
caf3b78c
AB
236:END:
237
238** Arch GNU/Linux on MacBook Air 2013 :arch:macbook:
239:PROPERTIES:
240:EXPORT_FILE_NAME: arch-macbook-air
241:EXPORT_DATE: 2016-11-01
caf3b78c 242:EXPORT_OPTIONS: ^:{}
ae39b0da
AB
243:EXPORT_HUGO_ALIASES: /2016/11/arch-macbook-air
244:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :toc true
caf3b78c
AB
245:END:
246
247This post summarizes how I install and dual-boot Arch GNU/Linux with
248Full-Disk Encryption alongside macOS. It is not meant to be a
249replacement 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]].
250Rather, it mostly serves as a small summary with a few useful notes
251about the gotchas.
252
253So, make sure you understand what you type into your terminal. If you
254don't, checking out the Arch wiki should probably be your first step.
255
256/Note:/ you will need internet access throughout the installation and
257the MacBook Air's WiFi doesn't work out of the box on Arch. I
258recommend using your phone's USB Tethering (if it does support it), or
259using an Ethernet-USB adapter.
260
261*** Shrinking the macOS partition
262
263The first step I take is resizing the HFS+ macOS partition to make
264room for the new {{{abbr(GNU/Linux)}}} installation. There are plenty
265of tutorials on how to do this using macOS's Disk Utility, so do that
266and then come back!
267
268*** Creating a bootable Arch Installer USB
269
270There are different ways of creating a bootable Arch USB, all
271documented on the [[https://wiki.archlinux.org/index.php/USB_flash_installation_media][USB flash installation media]] page on the Arch wiki,
272but the simplest one is using =dd= if you already have access to
273another UNIX system.
274
275{{{span(red,Warning:)}}} make sure you backup the data on your flash
276drive, as =dd= will irrevocably destroy all data on it.
277
278Use =lsblk= to find the name (block device) of your USB drive, then
279run =dd= (as root) as shown below:
280
281#+begin_src bash
282dd bs=4M if=/path/to/archlinux.iso of=/dev/sdx status=progress && sync
283#+end_src
284
285Replace =/path/to/archlinux.iso= with the path to the Arch image you
286have downloaded, and =/dev/sdx= with your drive.
287
288*** Booting up from the USB
289
290After creating the install USB, reboot your laptop and hold the alt
291key and boot into the USB.
292
293When booting is complete and you're presented with the prompt, it's a
294good time to make sure you're connected to the internet (see the
295/note/ at the top of this post).
296
297Use =ping= to verify that you've established a connection:
298
299#+begin_src bash
300ping archlinux.org
301#+end_src
302
303*** Updating the system clock
304
305Once you're connected to the internet, make sure the system clock is
306accurate:
307
308#+begin_src bash
309timedatectl set-ntp true # start and enable systemd-timesyncd
310#+end_src
311
312You can check the service status using =timedatectl status=.
313
314*** Partitioning
315:PROPERTIES:
316:CUSTOM_ID: partitioning
317:END:
318
319I 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
321personally prefer =cfdisk=.
322
323*** Setting up LVM & LUKS
324
325I 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
326partition.
327
328First, let's set up the underlying encrypted partition:
329
330#+begin_src bash
331cryptsetup -v --cipher aes-xts-plain64 --key-size 512 --hash sha512 \
332 --iter-time 5000 --use-urandom -y luksFormat /dev/sdaX
333#+end_src
334
335where =/dev/sdaX= is the partition you created in the last step
336(e.g. =/dev/sda4=). For more information about the =cryptsetup=
337options, see the [[https://wiki.archlinux.org/index.php/Dm-crypt/Device_encryption#Encryption_options_for_LUKS_mode][LUKS encryption options]].
338
339Then we open the container:
340
341#+begin_src bash
342cryptsetup open --type luks /dev/sdaX lvm
343#+end_src
344
345Now it's time to use lvm and prepare the logical volume(s):
346
347#+begin_src bash
348pvcreate /dev/mapper/lvm
349vgcreate vg /dev/mapper/lvm
350lvcreate --extents +100%FREE -n root vg
351#+end_src
352
353This will create a physical volume on the mapping we just opened,
354create a volume group named =vg= on the physical volume, and create a
355logical volume named =root= that spans the entire volume group. More
356complex setups are possible thanks to the great flexibility of lvm.
357
358We now format the logical volume with =ext4=:
359
360#+begin_src bash
361mkfs.ext4 /dev/mapper/vg-root
362#+end_src
363
364*** Installing the base system
365
366Let's mount the logical volume, make a directory for the mount point
367of the boot partition, and mount the boot partition (=/dev/sda1=):
368
369#+begin_src bash
370mount /dev/mapper/vg-root /mnt
371mkdir /mnt/boot
372mount /dev/sda1 /mnt/boot
373#+end_src
374
375Finally, let's install the base system (and optionally =base-devel=):
376
377#+begin_src bash
378pacstrap /mnt base base-devel
379#+end_src
380
381*** Configuring the system
382
383Let's generate the fstab:
384
385#+begin_src bash
386genfstab -U /mnt >> /mnt/etc/fstab
387#+end_src
388
389Use your favorite terminal-based editor, edit the fstab file and add
390the =discard= option for the root partition to enable TRIM on the SSD.
391
392Now we change root into our newly installed system and will configure
393it. Adjust these according to your own setup.
394
395#+begin_src bash
396arch-chroot /mnt /bin/bash
397passwd # set the root password
398echo myhostname > /etc/hostname # set the hostname
399ln -s /usr/share/zoneinfo/Canada/Eastern /etc/localtime # time zone
400hwclock --systohc --utc # write system clock to hardware clock (UTC)
401useradd -m -G wheel -s /bin/bash myuser # create myuser
402passwd myuser # set the password for myuser
403echo "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
405locale-gen
406echo LANG=en_US.UTF-8 > /etc/locale.conf
407export LANG=en_US.UTF-8
408#+end_src
409
410Then adjust the initramfs hooks in =/etc/mkinitcpio.conf= and enable
411the =encrypt= and =lvm2= hooks, and make sure =keyboard= is available
412before =encrypt= so you can actually type in the LUKS password when
413booting. Your =HOOKS= line should look similar to this:
414
415#+begin_src
416HOOKS="base udev autodetect modconf block keyboard encrypt lvm2 filesystems fsck"
417#+end_src
418
419After adjusting the hooks, build the initramfs:
420
421#+begin_src bash
422mkinitcpio -p linux
423#+end_src
424
425Now, install the =intel-ucode= package. We'll configure the bootloader
426to enable intel microcode updates.
427
428#+begin_src bash
429pacman -S intel-ucode
430#+end_src
431
432Create the =/boot/loader/loader.conf= with the following content
433(adjust the timeout to your liking):
434
435#+begin_src
436default arch
437timeout 3
438#+end_src
439
440Then create the entry for Arch:
441
442#+begin_src bash
443mkdir -p /boot/loader/entries
444touch /boot/loader/entries/arch.conf
445#+end_src
446
447Now edit =/boot/loader/entries/arch.conf= to specify the Arch entry:
448
449#+begin_src
450title Arch GNU/Linux
451linux /vmlinuz-linux
452initrd /intel-ucode.img
453initrd /initramfs-linux.img
454options cryptdevice=/dev/sdaX:vg:allow-discards root=/dev/mapper/vg-root rw
455#+end_src
456
457Again, =/dev/sdaX= is the partition you created in the [[#partitioning][partitioning]]
458step as the underlying encrypted partition.
459
460Finally, install the bootloader, exit the chroot, umount and reboot!
461
462#+begin_src bash
463bootctl install
464exit
465umount -R /mnt
466reboot
467#+end_src
468
469*** Post-installation recommendations
470
471Congratulations! You now have a minimal Arch installation.
472
473At this point, I usually install my favorite AUR helper, [[https://aur.archlinux.org/packages/pacaur/][pacaur]], then
474I 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]]
475backlight driver to fix the post suspend/resume issue where three's no
476brightness after waking up from suspend, and the only available
477brightness would be 100%.
478
479#+begin_src bash
480pacaur -S linux-headers dkms # linux-headers is required for dkms
481pacaur -S broadcom-wl-dkms
482pacaur -S mba6x_bl-dkms
483#+end_src
484
485Then, I'd like to install
486
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).
491
492Check out the [[https://wiki.archlinux.org/index.php/General_recommendations][General recommendations]] for more details.
493
494*** References
495
496Here are some resources I've come across each with lots of useful bits
497and pieces, about installing Arch on a MacBook:
498
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]]
507
caf3b78c 508
f052da50
AB
509* Footnotes
510
511[fn:1] Key summaries generated by including the =--list-key=,
512=--with-fingerprint=, and =--with-subkey-fingerprint= switches along
513with the key id when calling =gpg=.
514
caf3b78c
AB
515* COMMENT Local Variables :ARCHIVE:
516# Local Variables:
bdec7790
AB
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
caf3b78c 519# End: