aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYuchen Pei <hi@ypei.me>2022-02-06 21:25:01 +1100
committerYuchen Pei <hi@ypei.me>2022-02-06 21:25:01 +1100
commit2c422ce0a29154964cbb5011182711b1570541f9 (patch)
treebf363dcf1271ab7b2a36a34e2ca459f62b2849a0
parent292bab155170594932cc397683ba228fbc9791b9 (diff)
updated a bunch
-rw-r--r--html-templates/preamble.html6
-rw-r--r--microposts/bitcoin-theory.org7
-rw-r--r--microposts/chilean-constitution.org10
-rw-r--r--microposts/coq-is-cool.org15
-rw-r--r--microposts/curve25519.org5
-rw-r--r--microposts/dependent-types.org80
-rw-r--r--microposts/djokovic.org19
-rw-r--r--microposts/emacs-switch.org32
-rw-r--r--microposts/emms.org29
-rw-r--r--microposts/get-australia-weather.org56
-rw-r--r--microposts/google-antitrust-bully.org12
-rw-r--r--microposts/lxo-digital-tyranny.org18
-rw-r--r--microposts/lxo-open-letter.org10
-rw-r--r--microposts/mu4e-gnus.org31
-rw-r--r--microposts/network-freedom.org80
-rw-r--r--microposts/nov-el.org21
-rw-r--r--microposts/stallmansupport.org4
-rw-r--r--microposts/theyvoteforyou.org6
-rw-r--r--microposts/think-apac.org24
-rw-r--r--microposts/why-software-foundations.org36
-rw-r--r--pages/index.org15
-rw-r--r--pages/my-computing.org63
-rw-r--r--publish.el13
23 files changed, 572 insertions, 20 deletions
diff --git a/html-templates/preamble.html b/html-templates/preamble.html
index 314bcb0..cb0e7ac 100644
--- a/html-templates/preamble.html
+++ b/html-templates/preamble.html
@@ -6,9 +6,3 @@
<a href="/blog.html">Blog</a><a href="/microblog.html">Microblog</a><a href="https://g.ypei.me">Projects (git)</a>
</nav>
</header>
-<div id="fsf-banner">
- <center>Please join me to support the FSF for a free society:</center>
- <iframe src="//static.fsf.org/nosvn/banners/202111fundraiser/" scrolling="no"
- style="width: 100%; height: 150px; display: block; margin: 0; border: 0 none; overflow: hidden;">
- </iframe>
-</div>
diff --git a/microposts/bitcoin-theory.org b/microposts/bitcoin-theory.org
new file mode 100644
index 0000000..a9758d8
--- /dev/null
+++ b/microposts/bitcoin-theory.org
@@ -0,0 +1,7 @@
+#+title: Theory of Bitcoin
+
+#+date: <2021-12-23>
+
+The theoretical model of bitcoin is surprisingly simple. A transaction is a list of inputs and outputs, where the inputs trace to outputs of previous transactions. Transactions form blocks, and blocks form the blockchain with each block verifying the previous ones, going all the way back to the [[https://live.blockcypher.com/btc/block/000000000019d6689c085ae165831e934ff763ae46a2a6c172b3f1b60a8ce26f/][genesis block]]. Proof of work requires finding a nonce that hashes to a sufficiently small number. One new block every 10 minutes, transaction fees and award of 6.25BTC (halving every 210k blocks) goes to whoever created the block (aka miner). A total of 21mil BTC, running out by ~2140.
+
+By the way, the whitepaper is not very useful for understanding the theory of bitcoin, but Wikipedia and the [[https://en.bitcoin.it/wiki/Main_Page/][bitcoin wiki]] are far better resources IMO.
diff --git a/microposts/chilean-constitution.org b/microposts/chilean-constitution.org
new file mode 100644
index 0000000..d22b3c3
--- /dev/null
+++ b/microposts/chilean-constitution.org
@@ -0,0 +1,10 @@
+#+title: New Hampshire and Chile free software politics
+#+date: <2022-01-27>
+
+News was that a New Hampshire bill to promote free software in
+government services (especially mandating online government services
+to be usable if nonfree javascript is blocked using tools like
+LibreJS) is [[https://www.fsf.org/blogs/community/new-hampshire-residents-make-your-voice-heard-on-january-11th][on the table]], and [[https://drewdevault.com/2022/01/19/Help-Chile-promote-digital-freedoms.html][Chile]] is rewriting its constitution,
+with proposals to include free software values (Access to knowledge)
+and related digital rights values (Technological and digital
+sovereignty and Internet privacy).
diff --git a/microposts/coq-is-cool.org b/microposts/coq-is-cool.org
new file mode 100644
index 0000000..97d8d56
--- /dev/null
+++ b/microposts/coq-is-cool.org
@@ -0,0 +1,15 @@
+#+title: Coq is cool
+
+#+date: <2022-01-06>
+
+Having written emacs lisp for a while and grown my emacs init file to thousands of lines, I decided to revisit the /[[http://landoflisp.com/][Land of Lisp]]/, a fanstastically and humorously written book about lisp.
+
+The book said that lisp is basically lambda calculus, which got me thinking. How is it lambda calculus?
+
+So I went back into the rabbit hole that drew me in a few years ago, not knowing that's where I was going. I started by refreshing my knowledge reading /[[https://www.cis.upenn.edu/~bcpierce/tapl/][Types and Programming Languages]]/ (TAPL). After reading it I still didn't quite get how lisp is basically lambda calculus.
+
+TAPL mentioned Curry-Howard correspondence, a theory that connects logic systems with type systems. I wanted to know what each of the 8 vertices of the [[https://en.wikipedia.org/wiki/Lambda_cube][lambda cube]] corresponds to and how, which was not covered in TAPL. After a failed web surfing session in an attempt to find quick answers to my question, I was reminded of the /[[https://softwarefoundations.cis.upenn.edu/][Software Foundations]]/ series, and indeed, it talked about Curry-Howard correspondence with real code.
+
+So I went on to read the first volume titled /[[https://softwarefoundations.cis.upenn.edu/lf-current/index.html][Logic Foundations]]/. Previously I had an (irrational?) aversion towards logic, fearing much of it was all dry tautology and not as fun as more "useful" mathematics like probably theory. Boy was I wrong. /Logic Foundations/ introduces coq, which I didn't touch due to the same aversion. But as it turned out, coq answered most of my questions about formal mathematics, and fully developed my (unoriginal) [[https://toywiki.xyz/][ideas of formalising mathematics]]. Maths is code. Theorems are identified by their proofs. You can apply a theorem in the proof of another theorem, matching terms. You can parameterise theorems etc. etc. Coq is something I wish I knew when I was a PhD student. The logic system is constrained in CoC, calculus of constructions, which is the top vertex in the lambda cube. I am still reading the book and can't wait to find out the extent of mathematics covered by it and what can be done about non-constructive systems (like the classical maths where you can cheat with excluded middle) using coq or other formal systems.
+
+If one day programs and proofs are indistinguishable, the two traditions will blend. Maths has no copyright, but advanced maths can be hard to understand, though written in well-commented code it will be more accessible. Computer programs are the opposite, heavily copyrighted under good free licenses like (A)GPLv3+ and evil proprietary licenses, but more accessible (though code obfuscation is also thing but it cannot have gaps). My hope is this will bring the best of both worlds, that is, an elimination of copyright in computer programs (look, it is all maths, and copyrighting theorems and proofs are absurd!), and a more accessible corpus of advanced mathematics.
diff --git a/microposts/curve25519.org b/microposts/curve25519.org
new file mode 100644
index 0000000..f208504
--- /dev/null
+++ b/microposts/curve25519.org
@@ -0,0 +1,5 @@
+#+title: Curve25519
+
+#+date: <2021-12-23>
+
+[[https://research.nccgroup.com/wp-content/uploads/2020/02/A_Tour_of_Curve25519_in_Erlang-1.pdf][A tour of Curve25519]] is a great introduction on elliptic curve encryption. It explains how EC is like modular arithmetic, with the analogue what multiplication to EC is what exponentiation to modular arithmetic.
diff --git a/microposts/dependent-types.org b/microposts/dependent-types.org
new file mode 100644
index 0000000..5c4d70a
--- /dev/null
+++ b/microposts/dependent-types.org
@@ -0,0 +1,80 @@
+#+title: Curry-Howard correspondence and Dependent types
+#+date: <2022-01-20>
+
+What is Curry-Howard correspondence?
+
+Roughly speaking, it says there is a one-one correspondence between
+world of propositions (proofs) and world of types (programs).
+
+A simple illustration:
+
+For any two propositions P and Q, the proposition that P implying Q,
+i.e. P -> Q, corresponds to: for any two types T and S, the functional
+type T -> S.
+
+Finding a proof of P -> Q corresponds to finding an element in T -> S.
+
+In a more simplified setting, proving a proposition P corresponds to
+finding an element of T.
+
+In coq, one can write:
+
+#+begin_src coq
+Theorem p_implies_q : P -> Q.
+#+end_src
+
+Which looks exactly the same as, except the keywords =Theorem= and
+=Definition=,
+
+#+begin_src coq
+Definition some_function : T -> S.
+#+end_src
+
+To show the pun is genuine, if you want, you can prove a definition
+and define a theorem:
+
+#+begin_src coq
+Definition add_one : nat -> nat.
+Proof.
+ intro n. (* introduce the argument of the function to the context and call it n. *)
+ apply succ. (* apply succ to the "goal" *)
+ apply n.
+Defined.
+
+Definition imp_refl : forall P : Prop, P -> P := fun P p : P => p.
+#+end_src
+
+It may still feel rather forced, as the proof of the definition is way
+less readable than a direct definition, and the definition of the
+theorem is just plain silly (Logical Foundations has a more reasonable
+example - the evenness of a number).
+
+How about an actual example, where one cannot do without the
+correspondence? Well, look no further than dependent types!
+
+Say you want to work with vectors, which are lists of a certain
+length, which is encoded as a pair (the list, the length) with a
+condition:
+
+#+begin_src coq
+Definition vector (X : Type) :=
+ { '(xs, n) : list X * nat | length xs = n }.
+#+end_src
+
+This is called a dependent sum type, or sigma type, where the vertical
+bar =|= serves the same role as in set theory, meaning "such that".
+
+The full definition is a bit more involved which we will skip.
+
+Now, how do you define a concat function that takes two vectors of
+length m and n and returns a concatenated vector of length m + n? You
+will have to do two things in such a definition:
+
+- *Define* the resulting pair.
+- *Prove* the length of the resulting list is m + n.
+
+Now there's no escaping the pun!
+
+To learn more about this, check out [[https://softwarefoundations.cis.upenn.edu/lf-current/index.html][Logical Foundations]] and [[https://softwarefoundations.cis.upenn.edu/vfa-current/index.html][Verified
+Functional Algorithms]]. More specifically, [[https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html][ProofObjects: The
+Curry-Howard Correspondence]] and [[https://softwarefoundations.cis.upenn.edu/vfa-current/ADT.html#lab168][ADT: Abstract Data Types]].
diff --git a/microposts/djokovic.org b/microposts/djokovic.org
new file mode 100644
index 0000000..c6cfbcd
--- /dev/null
+++ b/microposts/djokovic.org
@@ -0,0 +1,19 @@
+#+title: The Djokovic case
+
+#+date: <2022-01-18>
+
+#+begin_quote
+Rules are rules the Prime Minister declared, especially when it comes
+to our borders. Rules weren't rules last year, when celebrities
+travelled to and from Australia while ordinary people were denied a
+permit to leave, or even more scandalously, not afforded the most
+basic right of a citizen to return to their country. Now though, when
+Australia chooses to insist on a medical procedure as a condition of
+entry to Australia the rules are suddenly rigid.
+#+end_quote
+
+- [[https://www.smh.com.au/national/djokovic-case-will-perpetuate-the-worst-aspects-of-the-pandemic-20220113-p59o4x.html?ref=rss&utm_medium=rss&utm_source=rss_national][Djokovic case will perpetuate the worst aspects of the pandemic]]
+
+Meanwhile, [[https://www.sbs.com.au/news/asylum-seekers-beg-australians-don-t-forget-us-when-djokovic-leaves/a1705542-309c-4f99-add2-86321ad450eb][asylum seekers beg Australians: ‘Don’t forget us when
+Djokovic leaves’]], and [[https://www.theguardian.com/australia-news/2022/jan/17/pm-accused-of-outright-lie-after-claiming-detainees-in-melbourne-hotel-are-not-refugees?CMP=Share_AndroidApp_Other][PM accused of ‘outright lie’ after claiming
+detainees in Melbourne hotel are not refugees]].
diff --git a/microposts/emacs-switch.org b/microposts/emacs-switch.org
new file mode 100644
index 0000000..8460ce3
--- /dev/null
+++ b/microposts/emacs-switch.org
@@ -0,0 +1,32 @@
+#+title: Emacs is cool
+
+#+date: <2021-12-30>
+
+Emacs blows Vim out of water.
+
+I started using vim in late 2000s, perhaps 2010, as I was drawn by the marketing slogan with vim "what you think is what you get".
+
+I tried to get vi keybinding on everything, in browser (vimperator), pdf viewer (zathura), window manager (i3) etc. I used vimwiki heavily for knowledge and task management, and even wrote the initial version of the pandoc vimwiki reader.
+
+About 18 months ago (around end of June 2020) I decided to give Emacs a try. The reason for this decision was more ideological than technical - I was fed up with a free software hostile environment, and Emacs always striked me as a centre piece of the GNU project.
+
+I started the official Emacs distribution with an empty config file, and read the emacs tutorial. Coming from vim, it was quite uncomfortable to go without the convenient keys from hjkl for basic navigation to C-d for scrolling down half page and . for repeating the last action.
+
+Org mode came as a double culture shock for someone used to vimwiki. Why would anyone think having a level-8 heading is a good idea? The link format was also a bit more verbose. Online resources focused more on GTD workflow than describing the markup syntax. And the table auto-align was nothing fancy - we have that in vimwiki.
+
+But soon enough, I found out Emacs is indeed way better than vim. It can be used for almost about every computing task, including web browsing, emails, media player, executing shell commands, reading epub, managing files, version control, and of course, text editing. Days without emacs now seemed like dark ages.
+
+Some aha moments in my Emacs journey:
+
+- When I discovered icomplete and fido, completion and function / variable discovery became so much easier.
+- When I combined icomplete with (setq org-refile-use-outline-path t), (setq org-refile-use-cache t), and (setq org-outline-path-complete-in-steps nil), which allows me to jump to any entry in a huge org file within seconds.
+- When I learned about emacsclient, so that I can have a long running emacs server so that I can share states across multiple emacs frames (or "windows" in a DE / WM context), and I don't lose anything when accidentally typing C-x C-c and quitting emacs.
+- When I found out EMMS to be the only media player with persistent playlists that I can switch and control with ease, and with the help of mpv, it can play urls in multiple schemes from http to sftp, and with the help you youtube-dl, it can play mediagoblin webpages, which allowed me to go through talks at https://audio-video.gnu.org/video/ and https://media.libreplanet.org/videos without losing track.
+- When I read the GTD book, despite not having a secretary to bring me the tickler folder or a koi pond to for me pave around with a wine glass in hand, I could finally put the design of org mode in context and vastly improve my workflow by implementing my version of GTD.
+- When I switched from webmail to mu4e, I learned how to get mails as a client and that emails are basically plaintext files (e.g. maildir) which can be read and written to locally and synced to remote server, and that smtp and imap are completely separate areas of concern; when I switched from mu4e to gnus, I learned how to serve mails using dovecot as an imap server and talk to a mail server using telnet, as well as the nice thing about offloading indexing to an external party (updating mails in gnus is instant, compared to mu4e-update-index).
+
+The most useful tool, the killer feature for me, is of course org mode. I spent most of my emacs screen time in org mode. I can't think of any aha moments related to it, but the process of adoption was gradual and there are so many nice features. I approached org mode with starting using one new feature every few weeks: speed command, org agenda, links, properties, org capture, effort estimate, clocking, tagging, refiling, attachment, online image display, citing... The problem with marketing org mode, and emacs in general, is that it integrates so much in my life and its workflow is so involved, that it is rather difficult to come up with a quick demo to impress people.
+
+One final point is that my usage is pretty vanilla, in that I strongly prefer the core distribution and GNU ELPA. I also installed a few packages from NonGNU ELPA, but I don't use MELPA at all, both for ideological reasons and simplicity. In the rare occasions when I really need a package not in core / NonGNU ELPA, I normally install it manually with make / add-to-list load-path and require / autoload.
+
+Enough rambling...
diff --git a/microposts/emms.org b/microposts/emms.org
new file mode 100644
index 0000000..34cd551
--- /dev/null
+++ b/microposts/emms.org
@@ -0,0 +1,29 @@
+#+title: EMMS and MPV
+#+date: <2022-01-27>
+
+[[https://www.gnu.org/software/emms/][EMMS]] is a multimedia playlist management tool on emacs. It allows
+users to control the playback of audio, video and even images by
+interacting with external players like mpv and vlc using IPC.
+
+I've been using EMMS exclusively with mpv, and the separation of media
+playlist management and playback, as well as moving playlist
+management to a purely plaintext environment make perfect sense.
+
+What is a playlist, but a list of urls? As a simple experiment, you
+can write a working m3u file by hand, with each line the raw path to a
+media file. It will load in EMMS, neat.
+
+What's also neat is mpv, a media player able to handle any kind of url
+you throw at it. Local files? Of course. Remote file urls over
+https? Yup. SFTP? You don't even need to sshfs mount, just do =mpv
+sftp://host:port/path/to/media.file=. How about Libreplanet videos?
+It will work, through youtube-dl extractors, just do =mpv
+https://media.libreplanet.org/u/libreplanet/m/fsf-award-ceremony/=.
+By the way, there's no mediagoblin extractor, but youtube-dl could
+find the media file using its rather versitile generic extractor.
+
+You can also create a playlist based on a youtube channel or playlist,
+with the help of some elisp plumbing calling =youtube-dl -j
+<playlist-or-channel-url> | jq '.webpage_url'= and add the urls to a
+playlist. If you want, you can even bind a key to download a remote
+media piece you like!
diff --git a/microposts/get-australia-weather.org b/microposts/get-australia-weather.org
new file mode 100644
index 0000000..246a6c4
--- /dev/null
+++ b/microposts/get-australia-weather.org
@@ -0,0 +1,56 @@
+#+title: A simple shell script to get Australian weather forecast from BoM
+
+#+date: <2022-01-13>
+
+In this micropost I'll show how to write your own android weather app
+("app" in a liberal sense) to retrieve weather for an Australian town,
+using Melbourne as an example.
+
+The short form (précis) 7-day forecasts, containing min / max
+temperature, humidity level and chances of precipitation are available
+as xml files [[http://www.bom.gov.au/catalogue/data-feeds.shtml][provided by the BoM]] - simply go there and get the link
+for the state you are interested in. For Victoria it is
+<ftp://ftp.bom.gov.au/anon/gen/fwo/IDV10753.xml>.
+
+So the first step is to download the xml to a temp directory, which
+can be done with wget:
+
+#+begin_src sh
+cd $PREFIX/tmp
+rm IDV10753.xml || true
+wget ftp://ftp.bom.gov.au/anon/gen/fwo/IDV10753.xml
+#+end_src
+
+Next one needs to query the xml file for the relevant data. Locate
+the city name, date, temperatures and chance of pricipitation using
+the nice [[https://en.wikipedia.org/wiki/XMLStarlet][xmlstarlet]] tool and format them nicely.
+
+#+begin_src sh
+result=`xml sel -t -m '//area[@description="Melbourne"]/forecast-period'\
+ -v "substring-before(@start-time-local, 'T')" \
+ -o " - min: " -v "element[@type='air_temperature_minimum']" \
+ -o " - max: " -v "element[@type='air_temperature_maximum']" \
+ -o " - " -v "text[@type='precis']" \
+ -o " - chance of precipitation: " -v "text[@type='probability_of_precipitation']" \
+ -n IDV10753.xml`
+#+end_src
+
+And finally, send the forecast to yourself using [[https://f-droid.org/en/packages/com.termux.api][Termux:API]].
+
+#+begin_src sh
+echo -e "7-day weather forecast in Melbourne:\n${result}" | \
+ termux-sms-send -n 044444444 # replace 044444444 with your phone number
+#+end_src
+
+To use it in termux, it doesn't hurt to specify the location of the
+shell in a shebang:
+
+#+begin_src sh
+#!/data/data/com.termux/files/usr/bin/bash
+#+end_src
+
+Finally, to make the script a bit more convenient to invoke, use
+[[https://f-droid.org/en/packages/com.termux.widget/][Termux:Widget]], and copy the script to =~/.shortcut=, and you can make
+it appear as a button in a desktop widget.
+
+Enjoy the Melbourne weather!
diff --git a/microposts/google-antitrust-bully.org b/microposts/google-antitrust-bully.org
new file mode 100644
index 0000000..893fd4c
--- /dev/null
+++ b/microposts/google-antitrust-bully.org
@@ -0,0 +1,12 @@
+#+title: Warren, Jayapal Demand Google Stop Trying to 'Bully' DOJ Antitrust Official
+
+#+date: <2022-01-18>
+
+[[https://www.commondreams.org/news/2022/01/05/warren-jayapal-demand-google-stop-trying-bully-doj-antitrust-official][Warren, Jayapal Demand Google Stop Trying to 'Bully' DOJ Antitrust Official]]
+
+Google is too big and powerful and should be broken up. Everyone
+should read the antitrust filings against Google, easpecially the [[https://storage.courtlistener.com/recap/gov.uscourts.nysd.564903/gov.uscourts.nysd.564903.152.0_1.pdf][one
+led by the Texas AG]]. Another good read which the filing was
+apparently built on, with more comprehensive introduction of the
+relevant technologies is [[https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3500919][Why Google Dominates Advertising Markets]] by
+Srinivasan.
diff --git a/microposts/lxo-digital-tyranny.org b/microposts/lxo-digital-tyranny.org
new file mode 100644
index 0000000..578c01a
--- /dev/null
+++ b/microposts/lxo-digital-tyranny.org
@@ -0,0 +1,18 @@
+#+title: Free software vs. open source
+
+#+date: <2022-01-18>
+
+Alexandre Oliva's post [[https://www.fsfla.org/ikiwiki/blogs/lxo/pub/against-software-tyranny.en.html][Against Software Tyranny]] is a good read on the
+difference between free software and open source. Free software is
+the liberation of computing, whereas open source is to hope for the
+corporations to be enlightened. Much like copyleft vs. pushover and
+dare I say progressives vs. liberals.
+
+Corporations view "open source" software as commons, just like natural
+resources, free for their taking. This is the key cause of
+unsustainable free software development recently under discussion.
+This is also why I don't really like to refer to the free world as
+commons.
+
+A commons is too weak to protect our computing freedom, and only makes
+sense if nonfree software is eliminated.
diff --git a/microposts/lxo-open-letter.org b/microposts/lxo-open-letter.org
new file mode 100644
index 0000000..1c8b0e1
--- /dev/null
+++ b/microposts/lxo-open-letter.org
@@ -0,0 +1,10 @@
+#+title: lxo open letter
+#+date: <2022-01-25>
+
+Alexandre Oliva (lxo) [[https://www.fsfla.org/ikiwiki/blogs/lxo/2021-12-24-open-letter.en.html][posted an email reply]] to a celebrated feminist
+leader regarding <https://stallmansupport.org> and the drama. Yet
+another powerful piece.
+
+In other news, with the [[https://www.fsf.org/news/fsf-expands-process-for-associate-members-to-nominate-new-members-of-the-board][FSF expanding process to allow associate
+members to nominate new board members]], I hope lxo can be back on the
+FSF Board.
diff --git a/microposts/mu4e-gnus.org b/microposts/mu4e-gnus.org
new file mode 100644
index 0000000..f4c3ca3
--- /dev/null
+++ b/microposts/mu4e-gnus.org
@@ -0,0 +1,31 @@
+#+title: From mu4e to gnus
+#+date: <2022-01-27>
+
+mu4e is a very popular emacs email client, known for the ease of setup.
+
+However it has its problems. The search is not very good (for example
+I had a hard time searching for patterns with special symbols like
+subjects containg the string "[gnu.org #". The indexing is part of the
+program, which combined with its lack of concurrency, makes it rather
+tricky to schedule update its index (on a side note elfeed has a
+similar problem). One may need to perform some hack by killing any mu
+process running in emacs in a cron script before indexing. I had been
+doing manual indexing, and waiting for 30 seconds to index all the
+mails whenever I want to check the mailbox for update was rather
+distracting.
+
+I made the move to gnus, which did not disappoint. Its search is more
+useful and natural - one does not have to worry about symbols. If
+gnus is configured with an imap server program like dovecot, indexing
+becomes that program's job, which could run as a cron job without
+bothering gnus. Since the imap server handles concurrency, one can
+even open up gnus in multiple emacs instance. As an added benefit,
+opening mailboxes is also much faster than mu4e.
+
+As mentioned before, the popular RSS reader elfeed operates on a
+similar model as mu4e, thus lacking concurrency. In fact, it is even
+more limited, as if one runs elfeed on two emacs, the update in one
+does not reflect on the other! I hope there could be an emacs RSS
+reader with the simplicity of elfeed, but taking gnus approach,
+leaving fetching, indexing and storage to a (local) server program,
+while the reader itself simply acting as a local client.
diff --git a/microposts/network-freedom.org b/microposts/network-freedom.org
new file mode 100644
index 0000000..4336ace
--- /dev/null
+++ b/microposts/network-freedom.org
@@ -0,0 +1,80 @@
+#+title: User freedom on the web
+
+#+date: <2022-01-25>
+
+The user freedom issues on the web are slightly complicated.
+
+- Client-side: is code executed on the client machine (e.g. javascript)
+ free? If so then the user's freedom is protected.
+ - Then there's also the case when the client blocks the execution of
+ nonfree javascript (e.g. by using [[https://www.gnu.org/software/librejs/][LibreJS]]), in which case the
+ user's freedom is still protected.
+ - There are also false positives when using LibreJS, when the
+ javascript code is free, but not labelled or annoated in a
+ LibreJS-compliant way. In this case, since the client code is
+ free it is safe to whitelist the scripts.
+- Server-side: is the server not under the user's (individual or
+ collective) control, doing computing on the user's behalf? If so
+ then that's bad (SaaSS), otherwise user freedom respecting.
+ - Examples of computing inherently one's own include translation,
+ photo editing etc.
+ - Examples of computing not inherently one's own are generally
+ activities requiring communication with others' computers, include
+ accessing information published by others (e.g. reading a blog
+ post) and publishing information (e.g. tweeting).
+
+Case studies:
+- Visiting [[https://fsf.org][the FSF homepage]] in a graphical browser like Firefox :: This
+ is fine, because all Javascript is trivial or LibreJS compliant.
+ Reading information published by the FSF is computing not inherently
+ one's own, so it's not SaaSS hence freedom respecting.
+- Tooting on Mastodon using its web client :: This is generally fine, as
+ Mastodon webclient is free software, and some instances (like
+ hostux.social) are LibreJS-compliant. Publishing microblogposts is
+ a communication act, thus the Mastodon service that does so is not
+ SasSS.
+- Watching videos on Peertube using its webclient :: Even though
+ Peertube is unusable with LibreJS on, it is free software from
+ backend to frontend. Whitelisting is generally safe. Watching
+ videos is again access information published by others, thus not
+ SaaSS.
+- Recaptcha :: Requires nonfree JS, bad.
+- Watching YouTube videos on an invidious proxy ::
+ similarly reading tweets on nitter, reading stuff on bibliogram or
+ doing these activities using a free software client. This is
+ certainly OK on the frontend as well as backend since it's
+ communication.
+- Routing on osmand :: Osmand is a free software client and all
+ computation happens locally so it's good.
+- Routing on osm.org :: It depends whether the routing calculation is
+ done locally using free javascript programs, or remotely (SaaSS).
+- Reading github issues :: Doable with LibreJS blocking all
+ non-trivial nonfree javascript, and it is communications.
+- Publishing tweets using free software clients :: Using free clients
+ is fine on the client side, and publication counts as communication
+ i.e. not SaaSS. [[https://www.fsf.org/twitter][This is what the FSF does]].
+- Get weather forecast :: Even though the forecast is done by
+ computation on meteorological data, the user did not supply data,
+ thus such computation does not count as SaaSS. It is similar to
+ when someone does computation in their head (to outline, draft and
+ revise) before publishing a blog post.
+
+We can spot some trends from these case studies:
+- Generally, a free software (not necessarily web) client is good.
+ Many tools offer help with this, including the alternative
+ frontends, haketilo and woot.tech.
+- F-droid Non-Free Network Service antifeature is not consistent with
+ the above method. In fact, it is not clear what is the definition
+ of this antifeature. For example, free alternative frontends like
+ [[https://f-droid.org/en/packages/org.schabi.newpipe/][NewPipe]] and [[https://f-droid.org/en/packages/com.jonjomckay.fritter/][Fritter]] are labelled with such antifeature, though by
+ the analysis above these are fine.
+- AGPL is mostly irrelevant in this discussion because it is mostly
+ concerned with the freedom of the service provider, even though it
+ is the best software license.
+- It's OK freedom-wise to use GAFAM service as long as the client is
+ free and the service does not count as SaaSS, though there are
+ separate concerns like user privacy.
+
+Further readings:
+- [[https://www.gnu.org/philosophy/who-does-that-server-really-serve.en.html][Who Does That Server Really Serve?]]
+- [[https://www.gnu.org/philosophy/network-services-arent-free-or-nonfree.html][Network Services Aren't Free or Nonfree; They Raise Other Issues]]
diff --git a/microposts/nov-el.org b/microposts/nov-el.org
new file mode 100644
index 0000000..037dffc
--- /dev/null
+++ b/microposts/nov-el.org
@@ -0,0 +1,21 @@
+#+title: Reading EPUB in Emacs
+#+date: <2022-02-03>
+
+[[https://depp.brause.cc/nov.el/][nov.el]] is pretty handy as an EPUB reader in Emacs. Before that I was
+using the calibre reader, which is slow and resource hungry.
+
+Emacs integration also means you get the following for free:
+
+1. Use [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Follow-Mode.html][follow-mode]] to allow double- or triple-page display. Note that
+ you may need to remove the header line for the text continuation to
+ be correct.
+2. Annotation can be done with org-capture, which can easily get the
+ selected text and link to the EPUB with the correct position.
+
+One feature that I am sorely missing from calibre reader is fulltext
+search, which is [[https://depp.brause.cc/nov.el/TODO.org][an item in the todo list of the project]].
+
+Another feature would be an equivalent to Info-index, which could
+allow jumping to any section in the book, with completion.
+
+
diff --git a/microposts/stallmansupport.org b/microposts/stallmansupport.org
index eb7b2a3..47f08a3 100644
--- a/microposts/stallmansupport.org
+++ b/microposts/stallmansupport.org
@@ -14,6 +14,8 @@ Other organisations also joined in, including Software Freedom Conservancy, Free
These groups and people refused to engage in discussions and some outright censored disagreements on this matter.
-It was a religious inquisition, a lynch mob, and a textbook case of ritual defamation. It damaged the free software movement and harmed the Free Software Foundation. The management team resigned, leaving the organisation in a bad shape, which was likely capitalised by opportunists in the GCC Steering Committee to Stallman, and remove the copyright assignment requirement from the project without community consultation, which further set a precedence and other GNU projects were planning on a similar move. The dilution of copyright will make GPL enforcement harder for these projects.
+It was a religious inquisition, a lynch mob, and a textbook case of ritual defamation. It damaged the free software movement and harmed the Free Software Foundation. The management team resigned, leaving the organisation in a bad shape, which was likely capitalised by opportunists in the GCC Steering Committee to remove Stallman, and remove the copyright assignment requirement from the project without community consultation, which further set a precedence and other GNU projects were planning on a similar move. The dilution of copyright will make GPL enforcement harder for these projects.
I condemn the defamatory attacks and [[https://rms-support-letter.github.io/][support Richard M. Stallman]] and I hope you join me. Please see also https://stallmansupport.org.
+
+P.S. Alexandre Oliva wrote [[http://www.fsfla.org/ikiwiki/blogs/lxo/2021-03-28-pursuing-justice-and-freedom.en.html][a very insightful piece on the drama]].
diff --git a/microposts/theyvoteforyou.org b/microposts/theyvoteforyou.org
new file mode 100644
index 0000000..9d712eb
--- /dev/null
+++ b/microposts/theyvoteforyou.org
@@ -0,0 +1,6 @@
+#+title: theyvoteforyou.org.au
+
+#+date: <2022-01-18>
+
+[[https://theyvoteforyou.org.au/][theyvoteforyou.org.au]] looks like [[https://yewtu.be/watch?v=ygeZdbgOuV8][a very useful resource for democracy]]
+and shouldn't be shut down.
diff --git a/microposts/think-apac.org b/microposts/think-apac.org
new file mode 100644
index 0000000..c034115
--- /dev/null
+++ b/microposts/think-apac.org
@@ -0,0 +1,24 @@
+#+title: Virtual event organisers, please think of people in the APAC region
+
+#+date: <2022-01-11>
+
+It is impossible to hold an online event that works for people from
+America, Europe and Asia-Pacific (APAC) regions at the same time.
+Normally one region will be dropped in favour of the other two. Most
+online tech events are organised by people located in Europe or
+America. 98% of them are set at a time that accommodates people in
+both regions, thus not work for people in APAC. Perhaps this is
+because not as many from the APAC region attend in an APAC-friendly
+time, compared to the number of participants from Europe in an
+Europe-friendly time (say) when the event is organised by someone in
+the States, which could be an effect as well, of events not
+accommodating APAC time.
+
+As such, if organisers in Europe or America sometimes set events time
+to be APAC-friendly say 40% of the time, instead of accommodating
+those across the pond, a more diverse and vibrant community may
+result. More concretely, that roughly translates to 12am-12pm UTC for
+Europe-based organisers, 7pm-7am UTC-5 for US East Coast, and 3pm-3am
+for US West Coast.
+
+Thank you!
diff --git a/microposts/why-software-foundations.org b/microposts/why-software-foundations.org
new file mode 100644
index 0000000..6f8257a
--- /dev/null
+++ b/microposts/why-software-foundations.org
@@ -0,0 +1,36 @@
+#+title: Why you should read Software Foundations
+
+#+date: <2022-01-13>
+
+I finished reading the [[https://softwarefoundations.cis.upenn.edu/lf-current/index.html][Logical Foundations]], the first volume of
+[[https://softwarefoundations.cis.upenn.edu/][Software Foundations]]. What an amazing book.
+
+I learned about formal proofs before, by playing the [[https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/][natural number game]]
+designed by Kevin Buzzard, which is in Lean.
+
+Logical Foundations covers all that and goes much deeper.
+
+There are many great things about this book. You can download it,
+ignore the html files, and just burn through the coq .v files, which
+are actually the source of the webpages. The texts are basically
+comments in the .v files, but the readability is not worse than the
+html files, and actually much better in emacs. It is almost like
+literate programming.
+
+As an aside, initially I had some problems with getting org-babel to
+work, but the files were deleted years ago. After reading LF I
+realised org-babel is not really important, since I can just happily
+work through the giant .v files in [[https://proofgeneral.github.io/][Proof General]] (which you can
+easily install manually without MELPA).
+
+Another neat thing about LF is that it really demonstrates the
+parallel between propositions and types, by using the same arrow
+notations for implication and function, by making no notational
+distinctions with proofs of a theorem and elements of type. A Proof
+is a Definition, and a property of numbers is a dependent type. If
+you want to understand Curry-Howard Correspondence, you can't go wrong
+with Logical Foundations.
+
+By the end of book, you will have worked through the implementation of
+a mini imperative language called Imp, and proved some simple
+properties of programs written in Imp - great value for your time!
diff --git a/pages/index.org b/pages/index.org
index a5f3d17..88bfe4d 100644
--- a/pages/index.org
+++ b/pages/index.org
@@ -25,13 +25,14 @@ for two years, writing C++, Python and Typescript, as well as
occassionaly grilling people on algorithms and data structure (aka
tech interviews).
-I am an associate member and licensing volunteer of the [[https://fsf.org][Free Software
-Foundation]], and a maintainer of [[https://www.gnu.org/software/librejs/][GNU LibreJS]] and [[https://h-node.org][h-node.org]]. In my
-past academic life I also applied the philosophy of free software to
-knowledge and research. For example I shared my research in
-Robinson-Schensted algorithms as a [[https://toywiki.xyz][wiki]] under a free Creative Commons
-license. I believe anyone can be an academic, seeking truth and
-sharing their findings with the public.
+As a free software advocate, I am an associate member and licensing
+volunteer of the [[https://fsf.org][Free Software Foundation]], and a maintainer of [[https://www.gnu.org/software/librejs/][GNU
+LibreJS]] and [[https://h-node.org][h-node.org]]. You can read about [[file:./my-computing.org][how I do my computing]] as a
+person on the [[https://fsf.org/campaigns/campaigns-summaries#ladder][freedom ladder]]. In my past academic life I also applied
+the philosophy of free software to knowledge and research. For example
+I shared my research in Robinson-Schensted algorithms as a [[https://toywiki.xyz][wiki]] under
+a free Creative Commons license. I believe anyone can be an academic,
+seeking truth and sharing their findings with the public.
I can be reached at: xU)U1M2fEQL6bfYGpwSG (PGP key: [[/assets/ypei-pubkey.txt][47F9 D050 1E11
8879 9040 4941 2126 7E93 EF86 DFD0]]). Feel free to email me, whether
diff --git a/pages/my-computing.org b/pages/my-computing.org
new file mode 100644
index 0000000..d67ed5d
--- /dev/null
+++ b/pages/my-computing.org
@@ -0,0 +1,63 @@
+# Copyright (C) 2013-2021 Yuchen Pei.
+
+# Permission is granted to copy, distribute and/or modify this
+# document under the terms of the GNU Free Documentation License,
+# Version 1.3 or any later version published by the Free Software
+# Foundation; with no Invariant Sections, no Front-Cover Texts, and
+# no Back-Cover Texts. You should have received a copy of the GNU
+# Free Documentation License. If not, see <https://www.gnu.org/licenses/>.
+
+# This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License. To view a copy of this license, visit http://creativecommons.org/licenses/by-sa/4.0/ or send a letter to Creative Commons, PO Box 1866, Mountain View, CA 94042, USA.
+
+#+title: How I do my computing
+
+* How I do my computing
+
+The way I do my computing is evolving and in flux, but here it is.
+
+I try to avoid nonfree programs, including nonfree javascript. I
+interact with many proprietary platforms in a read-only fashion
+without logged in, like watching videos on invidious, reading issues
+in a github repo, or checking out local events on meetup, with [[https://www.gnu.org/software/librejs/][LibreJS]]
+on 99% of the time.
+
+Unfortunately I have not achieved 100% free software use in that
+respect, as sometimes I have to for example log in to github for
+communication purposes like opening an issue or do online banking. I
+look forward to tech meetup groups resuming in person events, so that
+I can join AFK without having to log in and RSVP.
+
+That said, I currently don't have an active facebook, linkedin or
+google account. I also don't have Google services on my lineage os.
+Being a relatively late adopter of free software, the journey of
+slowly shaking off these malware was rather fun. For example, once I
+discovered my firefox was actually infested with nonfree extensions
+and purged them all.
+
+In terms of communication, I use xmpp, frequent IRC, and lurk on
+mailing lists. These days I read and write emails on gnus, and I sign
+and encrypt emails when needed. I also use Signal and (regrettably)
+some proprietary communications application which I'm in the process
+of getting rid of.
+
+I like both command line and emacs interface for getting things done,
+and given that most of my screen time is spent in emacs, I find myself
+writing elisp scripts to retrieve information from the web, or process
+data calling command line utilities, so that I can get things into
+Emacs (mainly org mode). I also use org-protocol somewhat heavily for
+that purpose with custom dispatchers.
+
+For low level or latency sensitive tasks, like rsync scripts for
+backups, cron jobs for retrieving emails and ssh into very remote
+servers I use command line, as it is more reliable than the emacs
+interface in this case.
+
+Though I like minimalistic tools like i3 and zathura, I'm not in the
+suckless camp, and do believe GUI has values. I use firefox and enjoy
+beautifully designed webpages (with nonfree javascript disabled of
+course), but take measures to improve my privacy. My websurfing is
+split about 30-70 between EWW and Firefox. I use EWW when I need to
+closely process the information in the surfing session in Emacs, when
+the webpage does not work with nonfree javascript, or when the
+colorscheme of the webpage is dark (yeah, my eyes can't take dark
+theme).
diff --git a/publish.el b/publish.el
index 3144ce5..9581a6e 100644
--- a/publish.el
+++ b/publish.el
@@ -60,6 +60,7 @@ The content starts with the first empty line."
(when (and (file-readable-p file) (not (directory-name-p file)))
(with-temp-buffer
(insert-file-contents file)
+ (delete-trailing-whitespace) ;; important, otherwise org may truncate the sitemap, probably due to some problem in converting all things to a list
(goto-char (point-min))
(let ((beg (+ 1 (re-search-forward "^$"))))
(buffer-substring beg (point-max)))))))
@@ -71,16 +72,16 @@ ENTRY: file-name
STYLE:
PROJECT: `microposts in this case."
(cond ((not (directory-name-p entry))
- (format "*[[%s][%s]]* - %s\n<<%s>>\n\n%s"
+ (format "*[[%s][%s]]* - %s\n<<%s>>\n\n%s"
(file-name-sans-extension entry)
- (format-time-string this-date-format
- (org-publish-find-date entry project))
- (org-publish-find-title entry project)
+ (format-time-string this-date-format
+ (org-publish-find-date entry project))
+ (org-publish-find-title entry project)
(file-name-sans-extension entry)
(org-publish-find-content entry project)
))
- ((eq style 'tree) (file-name-nondirectory (directory-file-name entry)))
- (t entry)))
+ ((eq style 'tree) (file-name-nondirectory (directory-file-name entry)))
+ (t entry)))
(defun me/org-publish-microblog (plist filename pub-dir)
"Publish RSS with PLIST, only when FILENAME is '../pages/microblog.org'.