contact: add link to my LibrePlanet user profile

[~bandali/bndl.org] / content-org / aminb.org

#+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 Amin Bandali (often =bandali= or =aminb= on [[/contact][the interwebs]]).  I’m
currently a [[/uw][graduate student]] in the [[https://watform.uwaterloo.ca][WatForm]] group at University of
Waterloo, supervised by [[https://cs.uwaterloo.ca/~nday/][Nancy Day]].  My current research focuses on
formal logic, model checking, and verification.  On the side, I also
dabble in [[https://leanprover.github.io][Lean]] and [[https://www.rust-lang.org][Rust]], and I enjoy [[https://stallman.org/articles/on-hacking.html][hacking]] on [[https://www.gnu.org/software/emacs/manual/elisp.html][Elisp]].

** 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-06 Sun 22:37]
:PROPERTIES:
:EXPORT_FILE_NAME: projects
:EXPORT_HUGO_MENU: :menu topnav :weight 30
:END:

TODO: set up projects page with my projects.

In the mean time, have a look at [[https://git.aminb.org][git.aminb.org]] instead.

** 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@bndl.org][amin@bndl.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://git.aminb.org/aminb.org]].  On each
=git push=, the repository is mirrored from my personal server to my
sr.ht account, the site is then automatically generated using the
[[https://builds.sr.ht][builds.sr.ht]] service (see the [[https://git.aminb.org/aminb.org/tree/.build.yml][=.build.yml=]] build manifest), and is
deployed back 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.aminb.org/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 copy of
which is displayed on [[https://git.aminb.org][git.aminb.org]].

** 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:
# eval: (org-hugo-auto-export-mode)
# org-hugo-footer: "\n\n[//]: # \"Exported with love from a post written in Org mode\"\n[//]: # \"- https://ox-hugo.scripter.co\""
# End: