Posts

[…] alas! either the locks were too large, or the key was too small, but at any rate it would not open any of them. – Lewis Carroll, Alice’s Adventures in Wonderland The Long-Standing Issue rustup#988 is probably one of the oldest open issues in the whole history of the rustup project, filed by no other than @matklad when he was working on Intellij Rust. As it turned out, rustup the toolchain manager did not have a proper locking mechanism to prevent concurrent invocation of its commands. The original issue explicitly mentioned that two concurrent rustup component add invocations (i.e. writing modifications) would cancel each other out with an error. ...

You are filled with determination… Doing proofs from the book Programming Language Foundations in Agda in the Lean 4 prover has really been a refreshing experience for me. However, things did get annoying sometimes for me, especially when I just couldn’t get pass the termination check. Although I haven’t seen every piece of the puzzle yet, I do hope that by sharing what I have seen so far, this blog post could save you some time from bashing “lean termination” into your search box , which could potentially lead you to some random web pages about Lean Manufacturing. ...

Now playing: Bad Apple!! Problem Being a polyglot can be painful sometimes. Particularly, it is extremely common for me to have multiple windows open at the same time, each using a different language: at this very moment, I have my messenger on where I participate conversations in Chinese, and I am writing this post in English at the same time in my VSCode window. As a result, with OS defaults, I have to switch between input sources (a.k.a. input methods) so often that I have even grown the bad habit of continuously pressing the fn key for… nothing at all. Assuredly, fn is more convenient than Windows PCs’ win + space, but wouldn’t it be much better if I don’t have to press any key? ...

Hi there! I have been using GitHub repos as my scratchpads since my very first days as a self-taught developer. However, it did occur to me recently that I could use some more organized form of output. Hopefully, this blog will help me take notes of my random ideas and efforts while providing the right contexts for them, so that they might not remain undiscovered lying in my repos. À très bientôt! 👋 ...