Lean 4

I saw several Mastodon posts by Terence Tao recently on his learning journey with Lean 4 and used it for the formalization of his paper. He began his learning with Lean 4 from scratch on Oct. 9 [1] with the help of ChatGPT and completed the formalization on Nov. 5 [2]. It's always fascinating to see how differently the same tools can be used by such talented people. Some of his comments on ChatGPT in the past:

AI tools like #ChatGPT will soon be capable of answering a large fraction of traditional university homework type questions with reasonable accuracy. In the long term, it seems futile to fight against this; perhaps what we as lecturers need to do is to move to an "open books, open AI" mode of examination where we give the students full access to AI tools but ask them more challenging questions, both to teach the material and also to teach the students how best to use the AI tools of the future.

Dec 19, 2022, 16:21, https://mathstodon.xyz/@tao/109543141003492779

Today was the first day that I could definitively say that #GPT4 has saved me a significant amount of tedious work. As part of my responsibilities as chair of the ICM Structure Committee, I needed to gather various statistics on the speakers at the previous ICM (for instance, how many speakers there were for each section, taking into account that some speakers were jointly assigned to multiple sections). The raw data (involving about 200 speakers) was not available to me in spreadsheet form, but instead in a number of tables in web pages and PDFs. In the past I would have resigned myself to the tedious task of first manually entering the data into a spreadsheet and then looking up various spreadsheet functions to work out how to calculate exactly what I needed; but both tasks were easily accomplished in a few minutes by GPT4, and the process was even somewhat enjoyable (with the only tedious aspect being the cut-and-paste between the raw data, GPT4, and the spreadsheet).

Am now looking forward to native integration of AI into the various software tools that I use, so that even the cut-and-paste step can be omitted. (Just being able to resolve >90% of LaTeX compilation issues automatically would be wonderful...)

Apr 09, 2023, 20:37, https://mathstodon.xyz/@tao/110172426733603359

On the other hand, Lean 4 [3] is a very interesting project. Sure, Lean 4 can be learned by people from different perspectives [4]. I'm wondering how I can benefit from Lean 4 in the field of computer networking. I saw some ongoing projects such as SciLean [5] which is currently a proof-of-concept project on optimization and machine learning. Maybe it can be helpful in computer networking in term of algorithm formalization or to proof certain algorithm properties. Nonetheless, it should be "fun" to learn something completely new to me, maybe in 2024.

Cloud Computing in Africa

Somehow I needed a VPS running in Africa, specifically in Lagos, Nigeria. Currently, major cloud computing companies don't have a major market share in Africa and most of them are located in South Africa.

Google Cloud Platform:
Announced in Oct. 2022 [6], there will be a new region in Johannesburg, South Africa.

Amazon Web Service:
Launched Africa (Cape Town) Region in 2020 [7].

Microsoft Azure:
Launched South Africa datacenter in Cape Town and Johannesburg in 2019 [8].

It was actually quite tricky to find a reliable VPS provider in Lagos and I just used Google search to find any available one randomly.

Cloudflare Outages

Cloudflare experienced a serious outage, again [9]. Luckily, it only affects the control plane and analytics. They are always transparent in post mortem report.

[1] https://mathstodon.xyz/@tao/111206761117553482

[2] https://mathstodon.xyz/@tao/111360218854032278

[3] Lean 4 programming language and theorem prover
https://github.com/leanprover/lean4

[4] Learning Lean 4
https://leanprover-community.github.io/learn.html

[5] Scientific computing in Lean 4
https://github.com/lecopivo/SciLean

[6] New cloud regions coming to a country near you
https://cloud.google.com/blog/products/infrastructure/introducing-new-google-cloud-regions

[7] Regions and Availability Zones
https://aws.amazon.com/about-aws/global-infrastructure/regions_az/

[8] Microsoft opens first data centers in Africa with general availability of Microsoft Azure

Microsoft opens first datacenters in Africa with general availability of Microsoft Azure

[9] Post Mortem on Cloudflare Control Plane and Analytics Outage
https://blog.cloudflare.com/post-mortem-on-cloudflare-control-plane-and-analytics-outage/

Remote accessing a mini PC in the Western Indian Ocean

This week, I was given a task to configure an Intel NUC-like mini PC, which will be sent to a remote island country in the Western Indian Ocean. This mini PC has two Ethernet ports (both will be connected to different ISPs) and one wireless interface (which will not be used however).

lspci
...
01:00.0 Ethernet controller: Realtek Semiconductor Co., Ltd. RTL8111/8168/8411 PCI Express Gigabit Ethernet Controller (rev 15)
02:00.0 Ethernet controller: Realtek Semiconductor Co., Ltd. RTL8111/8168/8411 PCI Express Gigabit Ethernet Controller (rev 15)
03:00.0 Network controller: Realtek Semiconductor Co., Ltd. RTL8821CE 802.11ac PCIe Wireless Network Adapter

After it's been connected, it will act as a network probe for one of our ongoing network measurements. However, the liaison there who will help us host the mini PC is not a professional IT guy. We have to take every precaution possible to prevent losing the remote connection.

Here is what I have done so far:

1. Linux distribution of choice: Debian 12.2. It's the latest Debian stable as of writing and we are more familiar with Debian-based distributions. Why not Ubuntu? Previously we had some networking issues (possibly DHCP-related) on Ubuntu with another mini PC of the same specs. Although we didn't figure out whether that's Ubuntu to blame, we chose Debian anyway for the myth of the "stability" of Debian over Ubuntu.

2. For remote login, we installed Tailscale. Cloudflare Tunnel and Ngrok [2] are also configured as backups. Cloudflare Tunnel also supports `--edge-bind-address` [1] to bind the tunnel to specific network interfaces. So I started two `cloudflared` instances using different systemd unit files and bound them to two Ethernet cards respectively (Does that make any sense?).

3. Set up automatic recovery from power loss in BIOS.

4. Set up auto reboot from kernel panic after 5 seconds using `/proc/sys/kernel/panic` [3].

5. Set up syslog forwarding using syslog-ng and Telegraf [4] to a centralized InfluxDB instance back here in Canada. In case of kernel panic/system hang or any connection loss, we can still query the last available system log from Grafana dashboards.

6. Set up Grafana's No-data alerting. I didn't use any external alert manager but stick to Grafana's built-in alerting capabilities. It's the first time I used Grafana's built-in alerting functions. At least it works and meets our demands for now.

However, things will be much easier if the mini PC has Intel vPro or any other IPMI capabilities. Unfortunately, it doesn't. We also considered whether we should purchase a PiKVM. We haven't, yet. We still have a few days before the mini PC is sent out. Meanwhile, we are trying to conduct some stress testing (just using `stress`?) on the mini PC to see whether there are any issues.

Software patching the Voyagers

NASA wants the Voyagers to age gracefully, so it’s time for a software patch

It's fascinating to see NASA is still trying to push software patches to decades-old Voyagers!

Voyagers current locations: https://voyager.jpl.nasa.gov/mission/status/

One way light time is 22 hours...I happened to come across an IETF draft (draft-many-deepspace-ip-assessment-00 [5]) recently on "Revisiting the Use of the IP Protocol Stack in Deep Space: Assessment and Possible Solutions" and also a new IETF mailing list on deepspace [6]. TCP/IP was invented and implemented in the late 70s, CCSDS was founded in the 80s, and NASA definitely used some very specific protocols to communicate with the Voyagers. But what about the future? NASA currently releases version 4 of "LunaNet Interoperability Specification" [7]. How will the existing networking stack work on an interplanetary scale?

Flash Player Emulator

> Ruffle is an Adobe Flash Player emulator written in the Rust programming language. Ruffle targets both the desktop and the web using WebAssembly.

https://github.com/ruffle-rs/ruffle

[1]: Cloudflare Tunnel run parameters
https://developers.cloudflare.com/cloudflare-one/connections/connect-networks/configure-tunnels/tunnel-run-parameters/#edge-bind-address

[2]: Ngrok
https://ngrok.com/

[3]: proc(5) - Linux man page
https://linux.die.net/man/5/proc

[4]: Telegraf / InfluxDB / Grafana as syslog receiver
https://nwmichl.net/2020/03/15/telegraf-influxdb-grafana-as-syslog-receiver/

[5]: Revisiting the Use of the IP Protocol Stack in Deep Space: Assessment and Possible Solutions
https://datatracker.ietf.org/doc/draft-many-deepspace-ip-assessment/

[6]: IETF deepspace mail archive
https://mailarchive.ietf.org/arch/browse/deepspace/

[7]: LunaNet Interoperability Specification

LunaNet Interoperability Specification

HEPiX

This week, the HEPiX forum's Autumn 2023 [1] meeting was held at UVic. About HEPiX, quote from their website:

The HEPiX forum brings together worldwide Information Technology staff, including system administrators, system engineers, and managers from the High Energy Physics and Nuclear Physics laboratories and institutes, to foster a learning and sharing experience between sites facing scientific computing and data challenges. Participating sites include ASGC, BNL, CERN, DESY, FNAL, IHEP, IN2P3, INFN, JLAB, KEK, KIT, Nikhef, PIC, RAL, SLAC, TRIUMF and many others. The HEPiX organization was formed in 1991, and its semi-annual meetings are an excellent source of information and sharing for IT experts in scientific computing.

ref: https://www.hepix.org/

I learned about this event from the conversation with the UVic networking architect mentioned in last week's randombits #41. What surprised me is that this event covers a wide range of topics, from CERN/affiliated site reports, networking & security, storage & filesystems, cloud, virtualization and operating systems, etc. All the slides are available at [2]. It's amazing to see the gargantuan amount of data that CERN and its affiliated institutions have to deal with. For example,

The Worldwide Large Hadron Collider Computing Grid (WLCG) as a specific (and very large) example of HEP research infrastructure supports multiple CERN experiments, with a reported 200PB of data generated annually and distributed to over 170 computing centers in 42 countries. As a massively distributed infrastructure with approximately 1.4 million CPU cores and 1.5 exabytes of storage, WLCG makes use of Research and Education (R&E) networks which have been highly engineered to handle this as well as other data-intensive sciences. Within the connected R&E networks, WLCG further makes use of the Large Hadron Collider Optical Private Network (LHCOPN) consisting of dedicated physical and virtual links, as well as a global-scale L3VPN overlay called the Large Hadron Collider Open Network Environment (LHCONE) which provides additional dedicated resources and segmentation from other R&E traffic.

ref: https://datatracker.ietf.org/doc/draft-cc-v6ops-wlcg-flow-label-marking/

That's why high-energy physics has always been the driving force of the evolution of the Internet and all kinds of other related technologies.

perfSONAR

One of the tools I learned from the slides of HEPiX is perfSONAR [3] and I played with it a bit. If I understand correctly, on one hand, it's just a collection of wrappers of many networking diagnostic and performance evaluation tools, including ping, traceroute, iperf3, owping, etc and you can schedule tasks using `pScheduler` [6]. The test types can be found at [4]. However, what makes it appealing and useful is that end users can submit tasks to different testpoints (or perfSONAR instances) to initiate measurements. There is a Grafana dashboard showing the list of perfSONAR testpoints [5] and you can also install a dashboard for a specific grid/network [7]. To some extent, I think it's similar to RIPE Atlas, but it's more widely deployed in academic institutions. You can get started and install perfSONAR on your own. For example, start a perfSONAR testpoint by running a single Docker container [8].

Framework Laptop 16

The first hands-on video of Framework Laptop 16 is out by Dave2D [9]. As a current user of the 12th Gen Intel Framework Laptop 13 (previously mentioned in 一些2022年的感想), after using it for about a year, I'm very glad to see Framework as a company continues to evolve and grow steadily. I'm not a fan of big laptops, none of my previously used laptops exceeds 14". I do like the form factor of Framework Laptop 16 (now with six expansion slots!), especially the swappable extension bay system. As Dave2D mentioned, building the cooling fans into the rear module expands the possibility of future upgrades when you need more advanced cooling solutions. Though it's pricey, I do hope they can succeed and the 3rd party accessory ecosystem continues to grow further.

Wrinkle the duck

A YouTube channel that can bring inner peace. "Wrinkle The Duck" [10].

I, Voyager

An open-source software planetarium [11] that reminds me of the game Universe Sandbox [12].

Raspberry Pi Thermal Upgrade

I purchased a Raspberry Pi 4 Model B with the official fan case back in July, and have been running several programs (PiHole, Grafana, Cloudflare Tunnel, etc) on it. The official fan case does not help a lot, the temperature barely drops below 60 degrees. Recently, I bought a USB to SATA adapter and replaced the boot drive from microSD to a SATA SSD. Strangely, the thermal situation becomes worse, the fan kicks in a lot more frequently (and it's very loud). So I bought a new cooling fan, with a relatively "huge" radiator, and applied thermal paste. Now the CPU temperature rarely increases above 30 degrees. Huge improvements.

[1]: HEPiX Autumn 2023
https://indico.cern.ch/event/1289243/overview

[2]: HEPiX Autumn 2023 Slides
https://indico.cern.ch/event/1289243/timetable/#20231016.detailed

[3]: perfSONAR
https://www.perfsonar.net/

[4]: perfSONAR Test and Tool Reference
https://docs.perfsonar.net/pscheduler_ref_tests_tools.html

[5]: Current list of global perfSONAR services
https://stats.perfsonar.net/d/spFwAQi4z/perfsonar-public?orgId=2/

[6]: What is pScheduler?
https://docs.perfsonar.net/pscheduler_intro.html

[7]: ESnet perfSONAR Dashboard
http://ps-dashboard.es.net/maddash-webui/

[8]: Using perfSONAR with Docker
https://docs.perfsonar.net/install_docker.html

[9]: This Laptop Can Last FOREVER

[10]: Wrinkle the Duck
https://www.youtube.com/@wrinkletheduck

[11]: I, Voyager

About

[12]: Universe Sandbox
https://universesandbox.com/

IPv6

Last week, I finally setup IPv6 support in my home network. My landlord uses Telus. Telus actually has end-to-end IPv6 support for quite a while. But I've always been reluctant to set up IPv6 in my home network.

For one reason, my landlord only gives me access to a WiFi access point, and I have been using an OpenWRT router to setup a wireless bridge [1], and connect my own router and switch behind it. The `relayd` package only had IPv6 support quite recently.

And IPv4...despite all the criticism on NAT, it just works. Especially since I started using Tailscale [2], remote login to my home network from the Internet, regardless of all the complexity of NAT, it works.

Recently, I've been doing a research project that requires some investigation on the IPv6 allocation of Starlink networks, I thought it was time to get some hands-on experience with IPv6.

To get a crash course and refresh on IPv6, I found the Netgate documentation [3] covers a lot of basic concepts of IPv6, and I can always learn something useful from wzyboy's blog [4]. Setting up IPv6 on OpenWRT with the `relayd` package is relatively straightforward, by following the documentation [1]. I did find something confusing on (3) in the Section of "Adding IPv6 support", probably because of the outdated documentation, but I did find some workaround from a forum post [5]. Nonetheless, it works.

One caveat though, I don't have access to the Telus router, which may have built-in firewall rules that disable the incoming IPv6 traffic. However, at least for now, I can use Tailscale or Cloudflare Tunnel to either remote login with IPv4 or publish my self-hosted services.

My institution (UVic, also maybe most major Canadian universities) has very sparing support for IPv6. BCNet and Canarie both have full support of IPv6 for a long time. And UVic, indeed has IPv6 support at the edge [6], with `2607:f8f0:c00::/40`, `2607:f8f0:c10::/48` and `2607:f8f0:c11::/48`. Last week, I happened to have a discussion with a networking architect at University IT Systems. He claimed that previously they indeed wanted to push the deployment of IPv6 in the campus, but Microsoft Update/Office 365 somehow doesn't work properly with dual-stack networks. (I believe I read some similar news before). And the OpenStack cluster they deployed had issues with IPv6 as well (I don't know what version they deployed at that time, but later last Friday, he told me the OpenStack cluster the university uses now has end-to-end proper IPv6 support already). So they retracted the IPv6 deployment on campus WiFi, and only enable it on case-by-case basis. For example, the university web portal does have IPv6 support.

```
~ dig @1.1.1.1 AAAA uvic.ca
;; ANSWER SECTION:
uvic.ca. 219 IN AAAA 2607:f8f0:c10::100
```

And some research groups have requested to use IPv6, such as the high energy physics research group that has research collaboration with CERN [8] [9].

"randombits" series...

This series was inspired by a friend of mine, he/she recently started this blog series [7] covering random topics he/she encountered during a week. I always read a bunch of random and weird stuffs every day on social media. Previously, I might just read it and forget it, or just archive the link in a random bookmark.
I hope my series can keep updating, at least for a while.

And this is the first blog post since I installed the ActivityPub plugin for WordPress [11]. It says the comments from the Fediverse will be displayed as comments of this blog post. Not quite sure how that looks like and how that interacts with the Fediverse. Follow the Fediverse account of this blog ([email protected]) and leave a comment! It turns out the ActivityPub plugin for WordPress is quite messy and creates a lot of messes, I might consider uninstall it someday in the future.

[1] Wi-Fi extender / repeater / bridge configuration
https://openwrt.org/docs/guide-user/network/wifi/relay_configuration

[2] Tailscale
https://tailscale.com/

[3] Netgate Documentation on IPv6
https://docs.netgate.com/pfsense/en/latest/network/ipv6/index.html

[4] IPv6 学习笔记 (In Chinese)
https://wzyboy.im/post/1536.html

[5] How to set up IPv6 with relay bridge
https://forum.openwrt.org/t/how-to-set-up-ipv6-with-relay-bridge/13723/5

[6] AS16462 University of Victoria
https://bgp.he.net/AS16462#_prefixes6

[7] ﾏﾖｲﾉﾈｸﾞﾗ
https://blg.1e41.com/posts/999main.md.html

[8] ATLAS at UVic
https://particle.phys.uvic.ca/atlas/press.shtml

[9] The ATLAS-Canada network
https://iopscience.iop.org/article/10.1088/1742-6596/119/5/052032/pdf

[10] HEPNet Canada
http://www.hepnetcanada.ca/

[11] ActivityPub for WordPress

ActivityPub