I managed to read 31 "books" in 2020. I'm happy with that. I thought the Pandemic would prevent me reaching my goal (30), since I did most of my reading on the commute to the Newcastle office, pre-pandemic. Somehow I've managed to compensate. I started setting a goal for books read per year in 2012 when I started to use goodreads. Doing so started to influence the type of reading I do (which is the reason I stopped my Interzone subscription in 2014, although I resumed it again sometime afterwards). Once I realised that I've been a bit more careful to ensure setting a goal was a worthwhile thing to do and not just another source of stress in my life. Two books I read were published in 2020. The first was Robert Galbraith's (a.k.a. J K Rowling's) Troubled Blood, the fifth (and largest) in the series of crime novels featuring Cormoran Strike (and the equally important Robin Ellacott). Nowadays Rowling is a controversial figure, but I'm not writing about that today, or the book itself, in much detail: briefly, it exceeded expectations, and my wife and I really enjoyed it. The other was Susanna Clarke's Piranesi: an utterly fantastic modern-fantasy story, quite short, completely different to her successful debut novel Jonathan Strange & Mr Norrell. I really loved this book, partly because it appeals to my love of fantasy geography, but also because it is very well put together, with a strong sense of the value of people's lives. A couple of the other books I read were quite Pandemic-appropriate. I tore through Josh Malerman's Bird Box, a fast-paced post-apocalyptic style horror/suspense story. The appeal was mostly in the construction and delivery: the story itself was strong enough to support the book at the length that it is, but I don't really feel it could have lasted much longer, and so I've no idea how the new sequel (Malorie) will work. The other was Station Eleven by Emily St. John Mandel. This was a story about a group of travelling musicians in a post-apocalyptic (post-pandemic) North America. A cast of characters all revolve around their relationship (or six degrees of separation) to an actor who died just prior to the Pandemic. The world-building in this book was really strong, and I felt sufficiently invested in the characters that I would love to read more about them in another book. However, I think that (although I'm largely just guessing here), in common with Bird Box, the setting was there to support the novel and the ideas that the author wanted to get across, and so I (sadly) doubt she will return to it. Finally I read a lot of short fiction. I'll write more about that in a separate blog post.

Review: A Deadly Education, by Naomi Novik

Series:	The Scholomance #1
Publisher:	Del Rey
Copyright:	2020
ISBN:	0-593-12849-4
Format:	Kindle
Pages:	319

Some children are born with magic, which grows as they mature. Magic attracts maleficaria: extremely deadly magical beasts that want to feast on that magic. Having innate magical ability is therefore a recipe for endless attacks from monsters and a death at a young age. This was true even for the enclaves, which are the rich, gated communities of the magical world. Hence, the Scholomance. This is a boarding school for magic users placed in the Void and protected against maleficaria as completely as possible while still letting the students graduate and leave after their senior year. Students are sent there via a teleportation spell with a weight allowance, taught magic by automated systems and magical artifacts, and left on their own to make alliances and survive. Or not survive; protected as well as possible still means that there are maleficaria everywhere, sneaking past the wards of the graduation hall and looking for snacks. The school sends cleansing fire through the halls at certain times; the rest of the time, the students either learn enough magic to defeat maleficaria themselves, form alliances with those who can, or die to feed the magic of the school. Enter Galadriel, or El as she prefers. She's not an enclave kid; she's the grumpy, misfit daughter of a hippie mother whose open-hearted devotion to healing and giving away her abilities make her the opposite of the jealously guarded power structures of the enclaves. El has no resources other than what she can muster on her own. She also has her mother's ethics, which means that although she has an innate talent for malia, drawing magic from the death of other living things, she forces herself to build her mana through rigorously ethical means. Like push-ups. Or, worse, crochet. At the start of the book, El is in her third year of four, and significantly more of her classmates are alive than normally would be. That's because of her classmate, Orion Lake, who has made a full-time hobby of saving everyone from maleficaria. His unique magical ability frees him from the constraints of mana or malia that everyone else is subject to, and he uses that to be a hero, surrounded by adoring fans. And El is thoroughly sick of it. This book is so good in so many different ways that I don't know where to start. Obviously, A Deadly Education is a twist on the boarding school novel, both the traditional and the magical kind. This is not a genre in which I'm that well-read, but even with my lack of familiarity, I noticed so many things Novik does to improve the genre tropes, starting with not making the heroic character with the special powers the protagonist. And getting rid of all the adults, which leaves way more space for rich social dynamics between the kids (complex and interesting ones that are entangled with the social dynamics outside of the school, not some simplistic Lord of the Flies take). Going alone anywhere in the school is dangerous, as is sitting at the bad tables in the cafeteria, so social cliques become a matter of literal life and death. And the students aren't just trying to survive; the ones who aren't part of enclaves are jockeying for invitations or trying to build the power to help their family and allies form their own. El is the first-person narrator of the story and she's wonderful. She's grumpy, cynical, and sarcastic, which is often good for first-person narrators, but she also has a core of ethics from her mother, and from her own decisions, that gives her so much depth. She is the type of person who knows exactly how much an ethical choice will cost her and how objectively stupid it is, and then will make it anyway out of sheer stubbornness and refuse to take credit for it. I will happily read books about characters like El until the end of time. Her mother never appears in this book, and yet she's such a strong presence because El's relationship with her matters, to both El and to the book. El could not be more unlike her mother in both personality and in magical focus, and she's exasperated by the sheer impracticality of some of her mother's ideals. And yet there's a core of love and understanding beneath that, a level at which El completely understands her mother's goals, and El relies on it even when she doesn't realize she's doing so. I don't think I've ever read a portrayal of a mother-daughter relationship this good where one of the parties isn't even present. And I haven't even gotten to the world-building, and the level to which Novik chases down and explores all the implications of this ridiculous murder machine of a school. I will offer this caveat: If you poke at the justification for creating this school in the way it was built, it's going to teeter a lot. That society thought this school was the best solution to its child mortality problem is just something you have to roll with. But once you accept that, the implications are handled so very well. The school is an inhuman character in its own right, with exasperating rules that the students learn and warn each other about. It tries to distract you with rare spellbooks or artifact materials because it's trying to kill you. The language tapes whisper horrific stories of your death. The back wall of your room is a window to the Void, from which you can demand spellbooks. You'll even get them in languages that you understand, for a generous definition of understand that may have involved glancing at one page of text, so be careful not to do that! The school replaces all of the adult teachers in the typical boarding school novel and is so much more interesting than any of them because it adds the science fiction thrill of setting as character. The world-building does mean a lot of infodumping, so be prepared for that. El likes to explain things, tell stories, and over-analyze her life, and reading this book is a bit like reading the journal of a teenage girl. For me, El's voice is so strong, authentic, stubborn, and sarcastically funny that I scarcely noticed the digressions into background material. And the relationships! Some of the turns will be predictable, since of course El's stubborn ethics will be (eventually) rewarded by the story, but the dynamic that develops between El and Orion is something special. It takes a lot to make me have sympathy with the chosen one boy hero, but Novik pulls it off without ever losing sight of the dynamics of class and privilege that are also in play. And the friendships El develops almost accidentally by being stubbornly herself are just wonderful, and the way she navigates them made me respect her even more. The one negative thing I will say about this book is that I don't think Novik quite nailed the climax. Some of this is probably because this is the first book of a series and Novik wanted to hold some social developments in reserve, but I thought El got a bit sidelined and ended up along for the ride in an action-movie sequence. Still, it's a minor quibble, and it's clear from the very end of the book that El is going to get more attention and end up in a different social position in the next book. This was a wholly engrossing and enjoyable story with a satisfying climax and only the barb of a cliffhanger in the very last line. It's the best SFF novel published in 2020 that I've read so far (yes, even better than Network Effect). Highly recommended, and I hope it gets award recognition this year. Followed by The Last Graduate (not yet published at the time of this review). Rating: 9 out of 10

Review: Laziness Does Not Exist, by Devon Price

Publisher:	Atria Books
Copyright:	January 2021
ISBN:	1-9821-4013-5
Format:	Kindle
Pages:	216

The premise of Laziness Does Not Exist is in the title: Laziness as a moral failing does not exist. It is a misunderstanding of other problems with physical or psychological causes, a belief system that is used to extract unsustainable amounts of labor, an excuse to withdraw our empathy, and a justification for not solving social problems. Price refers to this as the Laziness Lie, which they define with three main tenets:

1. Your worth is your productivity.
2. You cannot trust your own feelings and limits.
3. There is always more you could be doing.

This book (an expansion of a Medium article) makes the case against all three tenets using the author's own burnout-caused health problems as the starting argument. They then apply that analysis to work, achievements, information overload, relationships, and social pressure. In each case, Price's argument is to prioritize comfort and relaxation, listen to your body and your limits, and learn who you are rather than who the Laziness Lie is trying to push you to be. The reader reaction to a book like this will depend on where the reader is in thinking about the problem. That makes reviewing a challenge, since it's hard to simulate a reader with a different perspective. For myself, I found the content unobjectionable, but largely repetitive of other things I've read. The section on relationships in particular will be very familiar to Captain Awkward readers, just not as pointed. Similarly, the chapter on information overload is ground already covered by Digital Minimalism, among other books. That doesn't make this a bad book, but it's more of a survey, so if you're already well-read on this topic you may not get much out of it. The core assertion is aggressive in part to get the reader to argue with it and thus pay attention, but I still came away convinced that laziness is not a useful word. The symptoms that cause us to call ourselves lazy procrastination, burnout, depression, or executive function problems, for example are better understood without the weight of moral reproach that laziness carries. I do think there is another meaning of laziness that Price doesn't cover, since they are aiming this book exclusively at people who are feeling guilty about possibly being lazy, and we need some term for people who use their social power to get other people to do all their work for them. But given how much the concept of laziness is used to attack and belittle the hard-working or exhausted, I'm happy to replace "laziness" with "exploitation" when talking about that behavior. This is a profoundly kind and gentle book. Price's goal is to help people be less hard on themselves and to take opportunities to relax without guilt. But that also means that it stays in the frame of psychological analysis and self-help, and only rarely strays into political or economic commentary. That means it's more useful for taking apart internalized social programming, but less useful for thinking about the broader political motives of those who try to convince us to work endlessly and treat all problems as personal responsibilities rather than political failures. For that, I think Anne Helen Peterson's Can't Even is the more effective book. Price also doesn't delve much into history, and I now want to read a book on the origin of a work ethic as a defining moral trait. One truly lovely thing about this book is that it's quietly comfortable with human variety of gender and sexuality in a way that's never belabored but that's obvious from the examples that Price uses. Laziness Does Not Exist felt more inclusive in that way, and to some extent on economic class, than Can't Even. I was in the mood for a book that takes apart the political, social, and economic motivations behind convincing people that they have to constantly strive to not be lazy, so the survey nature of this book and its focus on self-help made it not the book for me. It also felt a bit repetitive despite its slim length, and the chapter structure didn't click for me. But it's not a bad book, and I suspect it will be the book that someone else needs to read. Rating: 6 out of 10

How our for-profit company became a nonprofit, to better tackle the digital divide. Originally posted on the Endless OS Foundation blog.

An 8-year journey to a nonprofit On the 1st of April 2020, our for-profit Endless Mobile officially became a nonprofit as the Endless OS Foundation. Our launch as a nonprofit just as the global pandemic took hold was, predictably, hardly noticed, but for us the timing was incredible: as the world collectively asked What can we do to help others in need? , we framed our mission statement and launched our .org with the same very important question in mind. Endless always had a social impact mission at its heart, and the challenges related to students, families, and communities falling further into the digital divide during COVID-19 brought new urgency and purpose to our team s decision to officially step in the social welfare space.

On April 1st 2020, our for-profit Endless Mobile officially became a nonprofit as the Endless OS Foundation, focused on the #DigitalDivide.

Our updated status was a long time coming: we began our transformation to a nonprofit organization in late 2019 with the realization that the true charter and passions of our team would be greatly accelerated without the constraints of for-profit goals, investors and sales strategies standing in the way of our mission of digital access and equity for all. But for 8 years we made a go of it commercially, headquartered in Silicon Valley and framing ourselves as a tech startup with access to the venture capital and partnerships on our doorstep. We believed that a successful commercial channel would be the most efficient way to scale the impact of bringing computer devices and access to communities in need. We still believe this we ve just learned through our experience that we don t have the funding to enter the computer and OS marketplace head-on. With the social impact goal first, and the hope of any revenue a secondary goal, we have had many successes in those 8 years bridging the digital divide throughout the world, from Brazil, to Kenya, and the USA. We ve learned a huge amount which will go on to inform our strategy as a nonprofit.

Endless always had a social impact mission at its heart. COVID-19 brought new urgency and purpose to our team s decision to officially step in the social welfare space.

Our unique perspective One thing we learned as a for-profit is that the OS and technology we ve built has some unique properties which are hugely impactful as a working solution to digital equity barriers. And our experience deploying in the field around the world for 8 years has left us uniquely informed via many iterations and incremental improvements.

With this knowledge in-hand, we ve been refining our strategy throughout 2020 and now starting to focus on what it really means to become an effective nonprofit and make that impact. In many ways it is liberating to abandon the goals and constraints of being a for-profit entity, and in other ways it s been a challenging journey for me and the team to adjust our way of thinking and let these for-profit notions and models go. Previously we exclusively built and sold a product that defined our success; and any impact we achieved was a secondary consequence of that success and seen through that lens. Now our success is defined purely in terms of social impact, and through our actions, those positive impacts can be made with or without our product . That means that we may develop and introduce technology to solve a problem, but it is equally as valid to find another organization s existing offering and design a way to increase that positive impact and scale.

We develop technology to solve access equity issues, but it s equally as valid to find another organization s offering and partner in a way that increases their positive impact.

The analogy to Free and Open Source Software is very strong while Endless has always used and contributed to a wide variety of FOSS projects, we ve also had a tension where we ve been trying to hold some pieces back and capture value such as our own application or content ecosystem, our own hardware platform necessarily making us competitors to other organisations even though they were hoping to achieve the same things as us. As a nonprofit we can let these ideas go and just pick the best partners and technologies to help the people we re trying to reach.

Digital equity 4 barriers we need to overcome In future, our decisions around which projects to build or engage with will revolve around 4 barriers to digital equity, and how our Endless OS, Endless projects, or our partners offerings can help to solve them. We define these 4 equity barriers as: barriers to devices, barriers to connectivity, barriers to literacy in terms of your ability to use the technology, and barriers to engagement in terms of whether using the system is rewarding and worthwhile.

We define the 4 digital equity barriers we exist to impact as:
1. barriers to devices
2. barriers to connectivity
3. barriers to literacy
4. barriers to engagement

It doesn t matter who makes the solutions that break these barriers; what matters is how we assist in enabling people to use technology to gain access to the education and opportunities these barriers block. Our goal therefore is to simply ensure that solutions exist building them ourselves and with partners such as the FOSS community and other nonprofits proving them with real-world deployments, and sharing our results as widely as possible to allow for better adoption globally. If we define our goal purely in terms of whether people are using Endless OS, we are effectively restricting the reach and scale of our solutions to the audience we can reach directly with Endless OS downloads, installs and propagation. Conversely, partnerships that scale impact are a win-win-win for us, our partners, and the communities we all serve. Engineering impact Our Endless engineering roots and capabilities feed our unique ability to build and deploy all of our solutions, and the practical experience of deploying them gives us evidence and credibility as we advocate for their use. Either activity would be weaker without the other.

Our engineering roots and capabilities feed our unique ability to build and deploy digital divide solutions.

Our partners in various engineering communities will have already seen our change in approach. Particularly, with GNOME we are working hard to invest in upstream and reconcile the long-standing differences between our experience and GNOME. If successful, many more people can benefit from our work than just users of Endless OS. We re working with Learning Equality on Kolibri to build a better app experience for Linux desktop users and bring content publishers into our ecosystem for the first time, and we ve also taken our very own Hack, the immersive and fun destination for kids learning to code, released it for non-Endless systems on Flathub, and made it fully open-source.

What s next for our OS? What then is in store for the future of Endless OS, the place where we have invested so much time and planning through years of iterations? For the immediate future, we need the capacity to deploy everything we ve built all at once, to our partners. We built an OS that we feel is very unique and valuable, containing a number of world-firsts: first production OS shipped with OSTree, first Flatpak-only desktop, built-in support for updating OS and apps from USBs, while still providing a great deal of reliability and convenience for deployments in offline and educational-safe environments with great apps and content loaded on every system. However, we need to find a way to deliver this Linux-based experience in a more efficient way, and we d love to talk if you have ideas about how we can do this, perhaps as partners. Can the idea of Endless OS evolve to become a spec that is provided by different platforms in the future, maybe remixes of Debian, Fedora, openSUSE or Ubuntu? Build, Validate, Advocate Beyond the OS, the Endless OS Foundation has identified multiple programs to help underserved communities, and in each case we are adopting our build, validate, advocate strategy. This approach underpins all of our projects: can we build the technology (or assist in the making), will a community in-need validate it by adoption, and can we inspire others by telling the story and advocating for its wider use?

We are adopting a build, validate, advocate strategy.
1. build the technology (or assist in the making)
2. validate by community adoption
3. advocate for its wider use

As examples, we have just launched the Endless Key (link) as an offline solution for students during the COVID-19 at-home distance learning challenges. This project is also establishing a first-ever partnership of well-known online educational brands to reach an underserved offline audience with valuable learning resources. We are developing a pay-as-you-go platform and new partnerships that will allow families to own laptops via micro-payments that are built directly into the operating system, even if they cannot qualify for standard retail financing. And during the pandemic, we ve partnered with Teach For America to focus on very practical digital equity needs in the USA s urban and rural communities. One part of the world-wide digital divide solution We are one solution provider for the complex matrix of issues known collectively as the #DigitalDivide, and these issues will not disappear after the pandemic. Digital equity was an issue long before COVID-19, and we are not so naive to think it can be solved by any single institution, or by the time the pandemic recedes. It will take time and a coalition of partnerships to win. We are in for the long-haul and we are always looking for partners, especially now as we are finding our feet in the nonprofit world. We d love to hear from you, so please feel free to reach out to me I m ramcq on IRC, RocketChat, Twitter, LinkedIn or rob@endlessos.org.

Like each month, have a look at the work funded by Freexian s Debian LTS offering. Debian project funding In December, we put aside 2100 EUR to fund Debian projects. The first project proposal (a tracker.debian.org improvement for the security team) was received and quickly approved by the paid contributors, then we opened a request for bids and the bid winner was announced today (it was easy, we had only one candidate). Hopefully this first project will be completed until our next report. We re looking forward to receive more projects from various Debian teams! Learn more about the rationale behind this initiative in this article. Debian LTS contributors In December, 12 contributors have been paid to work on Debian LTS, their reports are available:

• Abhijith PA did 7.0h (out of 14h assigned), thus carrying over 7h to January.
• Ben Hutchings did 16.5h (out of 16h assigned and 9h from November), thus carrying over 8.5h to January.
• Brian May did 10h (out of 10h assigned).
• Chris Lamb did 18h (out of 18h assigned), thus carrying over h to January.
• Emilio Pozuelo Monfort did 16.5h (out of 26h assigned), thus carrying over 9.5h to January.
• Holger Levsen did 3.5h coordinating/managing the LTS team.
• Markus Koschany did 26h (out of 26h assigned and 10.75h from November), thus carrying over 10.75 h to January.
• Ola Lundqvist did 9.5h (out of 12h assigned and 11h from November), thus carrying over 11.5h to January.
• Roberto C. S nchez did 18.5h (out of 26h assigned and 2.25h from November) and gave back the remaining 9.75h.
• Sylvain Beucler did 26h (out of 26h assigned).
• Thorsten Alteholz did 26h (out of 26h assigned).
• Utkarsh Gupta did 26h (out of 26h assigned).

Evolution of the situation December was a quiet month as we didn t have a team meeting nor any other unusual activity and we released 43 DLAs. The security tracker currently lists 30 packages with a known CVE and the dla-needed.txt file has 25 packages needing an update. This month we are pleased to welcome Deveryware as new sponsor! Thanks to our sponsors Sponsors that joined recently are in bold.

• Platinum sponsors:
• TOSHIBA (for 64 months)
• GitHub (for 54 months)
• Civil Infrastructure Platform (CIP) (for 32 months)
• Gold sponsors:
• Blablacar (for 79 months)
• Roche Diagnostics International AG (for 75 months)
• Linode (for 69 months)
• Babiel GmbH (for 58 months)
• Plat Home (for 57 months)
• University of Oxford (for 14 months)
• Deveryware
• Silver sponsors:
• The Positive Internet Company (for 80 months)
• Domeneshop AS (for 79 months)
• Nantes M tropole (for 73 months)
• Univention GmbH (for 65 months)
• Universit Jean Monnet de St Etienne (for 65 months)
• Ribbon Communications, Inc. (for 59 months)
• Exonet B.V. (for 48 months)
• Leibniz Rechenzentrum (for 42 months)
• CINECA (for 32 months)
• Minist re de l Europe et des Affaires trang res (for 26 months)
• Cloudways Ltd (for 15 months)
• Dinahosting SL (for 13 months)
• Platform.sh (for 8 months)
• Bauer Xcel Media Deutschland KG (for 7 months)
• Moxa Intelligence Co., Ltd.
• Bronze sponsors:
• Seznam.cz, a.s. (for 80 months)
• Evolix (for 79 months)
• Linuxhotel GmbH (for 77 months)
• Intevation GmbH (for 76 months)
• Daevel SARL (for 75 months)
• Bitfolk LTD (for 74 months)
• Megaspace Internet Services GmbH (for 74 months)
• Greenbone Networks GmbH (for 73 months)
• NUMLOG (for 73 months)
• WinGo AG (for 72 months)
• Ecole Centrale de Nantes LHEEA (for 69 months)
• Entr ouvert (for 64 months)
• Adfinis AG (for 61 months)
• Laboratoire LEGI UMR 5519 / CNRS (for 56 months)
• Tesorion (for 56 months)
• GNI MEDIA (for 55 months)
• Bearstech (for 47 months)
• LiHAS (for 47 months)
• People Doc (for 43 months)
• Catalyst IT Ltd (for 41 months)
• Supagro (for 37 months)
• Demarcq SAS (for 35 months)
• Universit Grenoble Alpes (for 22 months)
• TouchWeb SAS (for 14 months)
• SPiN AG (for 10 months)
• CoreFiling (for 6 months)
• Institut des sciences cognitives Marc Jeannerod

Review: The Secret Barrister, by The Secret Barrister

Publisher:	Picador
Copyright:	2018
Printing:	2019
ISBN:	1-5098-4115-6
Format:	Kindle
Pages:	344

The Secret Barrister is a survey and critique of the criminal legal system of England and Wales. The author is an anonymous barrister who writes a legal blog of the same name (which I have not read). A brief and simplified primer for those who, like me, are familiar with the US legal system but not the English one: A barrister is a lawyer who argues cases in court, as distinct from a solicitor who does all the other legal work (and may make limited court appearances). If you need criminal legal help in England and Wales, you hire a solicitor, and they are your primary source of legal advise. If your case goes to court, your solicitor will generally (not always) refer the work of arguing your case before a judge and jury to a barrister and "instruct" them in the details of your argument. The job of the barrister is then to handle the courtroom trial, offer trial-specific legal advice, and translate your defense (or the crown's prosecution) into persuasive courtroom arguments. Unlike the United States, with its extremely sharp distinction between prosecutors and criminal defense attorneys, criminal barristers in England and Wales argue both prosecutions and defenses depending on who hires them. (That said, the impression I got from this book is that the creation of the Crown Prosecution Service is moving England closer to the US model and more prosecutions are now handled by barristers employed directly by the CPS, whom I assume do not take defense cases.) Barristers follow the cab-rank rule, which means that, like a taxicab, they are professionally obligated to represent people on a first-come, first-serve basis and are not allowed to pick and choose clients. (Throughout, I'm referencing the legal system of England and Wales because the author restricts his comments to it. Presumably this is because the Scottish and Northern Irish? legal systems are different yet again in ways I do not know.) If details like this sound surprising, you can see the appeal of this book to me. It's easy, in the US, to have a vast ignorance about the legal systems of other countries or even the possibility of different systems, which makes it hard to see how our system could be improved. I had a superficial assumption that since US law started as English common law, the US and English legal systems would be substantially similar. And they are to an extent; they're both adversarial rather than inquisitorial, for example (more on that in a moment). But the current system of criminal prosecution evolved long after US independence and thus evolved differently despite similar legal foundations. Those differences are helpful for this American to ponder the road not taken and the impact of our respective choices. That said, explaining the criminal legal system to Americans isn't the author's purpose. The first fifty pages are that beginner's overview, since apparently even folks who live in England are confused by the ubiquity of US legal dramas (not that those are very accurate representations of the US legal system either). The rest of the book, and its primary purpose, is an examination of the system's failings, starting with the magistrates' courts (which often use lay judges and try what in the US would be called misdemeanors, although as discussed in this book their scope is expanding). Other topics include problems with bail, how prosecution is structured, how victims and witnesses are handled, legal aid, sentencing, and the absurd inadequacy of compensation for erroneous convictions. The most useful part of this book for me, apart from the legal system introduction, was the two chapters the author spends arguing first for and then against replacing an adversarial system with an inquisitorial system (the French criminal justice system, for example). When one is as depressed about the state of one's justice system as both I and the author are, something radically different sounds appealing. The author first makes a solid case for the inquisitorial system and then tries to demolish it, still favoring the adversarial system, and I liked that argument construction. The argument in favor of an adversarial system is solid and convincing, but it's also depressing. It's the argument of someone who has seen the corruption, sloppiness, and political motivations in an adversarial system and fears what would happen if they were able to run rampant under a fig leaf of disinterested objectivity. I can't disagree, particularly when starting from an adversarial system, but this argument feels profoundly cynical. It reminds me of the libertarian argument for capitalism: humans are irredeemably awful, greed and self-interest are the only reliable or universal human motives, and therefore the only economic system that can work is one based on and built to harness greed, because expecting any positive characteristics from humans collectively is hopelessly naive. The author of this book is not quite that negative in their argument for an adversarial system, but it's essentially the same reasoning: the only way a system can be vaguely honest is if it's constantly questioned and attacked. It can never be trusted to be objective on its own terms. I wish the author had spent more time on the obvious counter-argument: when the system is designed for adversarial combat, it normalizes and even valorizes every dirty tactic that might result in a victory. The system reinforces our worst impulses, not to mention grinding up and destroying people who cannot afford their own dirty tricks. The author proposes several explanations for the problems they see in the criminal legal system, including "tough on crime" nonsense from politicians that sounds familiar to this American reader. Most problems, though, they trace back to lack of funding: of the police, of the courts, of the prosecutors, and of legal aid. I don't know enough about English politics to have an independent opinion on this argument, but the stories of outsourcing to the lowest bidder, overworked civil servants, ridiculously low compensation rates, flawed metrics like conviction rates, and headline-driven political posturing that doesn't extend to investing in necessary infrastructure like better case-tracking systems sounds depressingly familiar. This is one of those books where I appreciated the content but not the writing. It's not horrible, but the sentences are ponderous and strained and the author is a bit too fond of two-dollar words. They also have a dramatic and self-deprecating way of describing their own work that I suspect they thought was funny but that I found grating. By the end of this book, I was irritated enough that I can't recommend it. But the content was interesting, even the critique of a political system that isn't mine, and it prompted some new thoughts on the difficulties of creating a fair justice system. If you can deal with the author's writing style, you may also enjoy it. Rating: 6 out of 10

The promise of free software is a near-future utopia, built on democratized technology. This future is just and it is beautiful, full of opportunity and fulfillment for everyone everywhere. We can create the things we dream about when we let our minds wander into the places they want to. We can be with the people we want and need to be, when we want and need to. This is currently possible with the technology we have today, but it s availability is limited by the reality of the world we live in the injustice, the inequity, the inequality. Technology runs the world, but it does not serve the interests of most of us. In order to create a better world, our technology must be transparent, accountable, trustworthy. It must be just. It must be free. The job of the free software movement is to demonstrate that this world is possible by living its values now: justice, equity, equality. We build them into our technology, and we build technology that make it possible for these values to exist in the world. At the Free Software Foundation, we liked to say that we used all free software because it was important to show that we could. You can do anything with free software, so we did everything with it. We demonstrated the importance of unions for tech workers and non-profit workers by having one. We organized collectively and protected our rights for the sake of ourselves and one another. We had non-negotiable salaries, based on responsibility level and position. That didn t mean we worked in an office free from the systemic problems that plague workplaces everywhere, but we were able to think about them differently. Things were this way because of Richard Stallman but I view his influence on these things as negative rather than positive. He was a cause that forced these outcomes, rather than being supportive of the desires and needs of others. Rather than indulge in gossip or stories, I would like to jump to the idea that he was supposed to have been deplatformed in October 2019. In resigning from his position as president of the FSF, he certainly lost some of his ability to reach audiences. However, Richard still gives talks. The FSF continues to use his image and rhetoric in their own messaging and materials. They gave him time to speak at their annual conference in 2020. He maintains leadership in the GNU project and otherwise within the FSF sphere. The people who empowered him for so many years are still in charge. Richard, and the continued respect and space he is given, is not the only problem. It represents a bigger problem. Sexism and racism (among others) run rampant in the community. This happens because of bad actors and, more significantly, by the complacency of organizations, projects, and individuals afraid of losing contributors, respect, or funding. In a sector that has so much money and so many resources, women are still being paid less than men; we deny people opportunities to learn and grow in the name of immediate results; people who aren t men, who aren t white, are abused and harassed; people are mentally and emotionally taken advantage of, and we are coerced into burn out and giving up our lives for these companies and projects and we are paid for tolerating all of this by being told we re doing a good job or making a difference. But we re not making a difference. We re perpetuating the worst of the status quo that we should be fighting against. We must not continue. We cannot. We need to live our ideals as they are, and take the natural next steps in their evolution. We cannot have a world of just technology when we live in a world of exclusion; we cannot have free software if we continue to allow, tolerate, and laud the worst of us. I ve been in and around free software for seventeen years. Nearly every part of it I ve participated in has members and leadership that benefit from allowing and encouraging the continuation of maleficence and systemic oppression. We must purge ourselves of these things of sexism, racism, injustice, and the people who continue and enable it. There is no space to argue over whether a comment was transphobic if it hurt a trans person then it is transphobic and it is unacceptable. Racism is a global problem and we must be anti-racist or we are complicit. Sexism is present and all men benefit from it, even if they don t want to. These are free software issues. These are things that plague software, and these are things software reinforces within our societies. If a technology is exclusionary, it does not work. If a community is exclusionary, it must be fixed or thrown away. There is no middle ground here. There is no compromise. Without doing this, without taking the hard, painful steps to actually live the promise of user freedom and everything it requires and entails, our work is pointless and free software will fail. I don t think it s too late for there to be a radical change the radical change that allows us to create the utopia we want to see in the world. We must do that by acknowledging that just technology leads to a just society, and that a just society allows us to make just technology. We must do that by living within the principles that guide this future now. I don t know what will happen if things don t change soon. I recently saw someone comment that change doesn t happens unless one person is willing to sacrifice everything to make that change, to lead and inspire others to play small parts. This is unreasonable to ask of or expect from someone. I ve been burning myself out to meet other people s expectations for seventeen years, and I can t keep doing it. Of course I am not alone, and I am not the only one working on and occupied by these problems. More people must step up, not just for my sake, but for the sake of all of us, the work free software needs to do, and the future I dream about.

In the comments on my post about Load Average Monitoring [1] an anonymous person recommended that I investigate PSI. As an aside, why do I get so many great comments anonymously? Don t people want to get credit for having good ideas and learning about new technology before others? PSI is the Pressure Stall Information subsystem for Linux that is included in kernels 4.20 and above, if you want to use it in Debian then you need a kernel from Testing or Unstable (Bullseye has kernel 4.19). The place to start reading about PSI is the main Facebook page about it, it was originally developed at Facebook [2]. I am a little confused by the actual numbers I get out of PSI, while for the load average I can often see where they come from (EG have 2 processes each taking 100% of a core and the load average will be about 2) it s difficult to work out where the PSI numbers come from. For my own use I decided to treat them as unscaled numbers that just indicate problems, higher number is worse and not worry too much about what the number really means. With the cgroup2 interface which is supported by the version of systemd in Testing (and which has been included in Debian backports for Buster) you get PSI files for each cgroup. I ve just uploaded version 1.3.5-2 of etbemon (package mon) to Debian/Unstable which displays the cgroups with PSI numbers greater than 0.5% when the load average test fails.

System CPU Pressure: avg10=0.87 avg60=0.99 avg300=1.00 total=20556310510
/system.slice avg10=0.86 avg60=0.92 avg300=0.97 total=18238772699
/system.slice/system-tor.slice avg10=0.85 avg60=0.69 avg300=0.60 total=11996599996
/system.slice/system-tor.slice/tor@default.service avg10=0.83 avg60=0.69 avg300=0.59 total=5358485146
System IO Pressure: avg10=18.30 avg60=35.85 avg300=42.85 total=310383148314
 full avg10=13.95 avg60=27.72 avg300=33.60 total=216001337513
/system.slice avg10=2.78 avg60=3.86 avg300=5.74 total=51574347007
/system.slice full avg10=1.87 avg60=2.87 avg300=4.36 total=35513103577
/system.slice/mariadb.service avg10=1.33 avg60=3.07 avg300=3.68 total=2559016514
/system.slice/mariadb.service full avg10=1.29 avg60=3.01 avg300=3.61 total=2508485595
/system.slice/matrix-synapse.service avg10=2.74 avg60=3.92 avg300=4.95 total=20466738903
/system.slice/matrix-synapse.service full avg10=2.74 avg60=3.92 avg300=4.95 total=20435187166

Above is an extract from the output of the loadaverage check. It shows that tor is a major user of CPU time (the VM runs a ToR relay node and has close to 100% of one core devoted to that task). It also shows that Mariadb and Matrix are the main users of disk IO. When I installed Matrix the Debian package told me that using SQLite would give lower performance than MySQL, but that didn t seem like a big deal as the server only has a few users. Maybe I should move Matrix to the Mariadb instance. to improve overall system performance. So far I have not written any code to display the memory PSI files. I don t have a lack of RAM on systems I run at the moment and don t have a good test case for this. I welcome patches from people who have the ability to test this and get some benefit from it. We are probably about 6 months away from a new release of Debian and this is probably the last thing I need to do to make etbemon ready for that.

• [1] https://etbe.coker.com.au/2020/02/02/load-average-monitoring/
• [2] https://facebookmicrosites.github.io/psi/docs/overview.html

Background I usually don t mind ads, as not as they not very intrusive. I get that the current media model is basically ad-funded, and that unless I want to pay $1/month or so to 50 web sites, I have to accept ads, so I don t run an ad-blocker. Sure, sometimes are annoying (hey YT, mid-roll ads are borderline), but I ve also seen many good ads, as in interesting or funny even. Well, I don t think I ever bought anything as direct result from ads, so I don t know how useful ads are for the companies, but hey, what do I care. Except there a few ad networks that run what I would say are basically revolting ads. Things I don t want to ever accidentally see while eating, or things that are really make you go WTF? Maybe you know them, maybe you don t, but I guess there are people who don t know how to clean their ears, or people for whom a fast 7 day weight loss routine actually works. Thankfully, most of the time I don t browse sites which use this networks, but randomly they do leak to even sites I do browse. If I m not very stressed already, I can ignore them, otherwise they really, really annoy me. Case in point, I was on Slashdot, and because I was logged on and recently had mod points, the right side column had a check-box disable ads . That sidebar had some relatively meaningful ads, like a VPN subscription (not that I would use it, but it is a tech thing), or even a book about Kali Linux, etc. etc. So I click the disable ads , and the right column goes away. I scroll down happily, only to be met, at the bottom, by the best way to clean your ear , the most 50 useless planes ever built (which had a drawing of something that was for sure never ever built outside of in movies), you won t believe how this child actor looks today , etc.

Solving the problem The above really, really pissed me off, so I went to search how to block ad network . To my surprise, the fix was not that simple, for standard users at least.

Method 1: hosts file The hosts file is reasonable as it is relatively cross-platform (Linux and Windows and Mac, I think), but how the heck do you edit hosts on your phone? And furthermore, it has some significant downsides. First, /etc/hosts lists individual hosts, so for an entire ad network, the example I had had two screens of host names. This is really unmaintainable, since rotating host names, or having a gazillion of them is trivial. Second, it cannot return negative answers. I.e. you have to give each of those hosts a valid IPv4/IPv6, and have something either reply with 404 or another 4xx response, or not listen on port 80/443. Too annoying. And finally, it s a client-side solution, so one would have to replicate it across all clients in a home, and keep it in sync.

Method 2: ad-blockers I dislike ad-blockers on principle, since they need wide permissions on all pages, but it is a recommended solution. However, to my surprise, one finds threads saying ad-blocker foo has whitelisted ad network bar, at which point you re WTF? Why do I use an ad-blocker if they get paid by the lowest of the ad networks to show the ads? And again, it s a client-side solution, and one would have to deploy it across N clients, and keep them in sync, etc.

Method 3: HTTP proxy blocking To my surprise, I didn t find this mentioned in a quick internet search. Well, HTTP proxies have long gone the way of the dodo due to HTTPs everywhere , and while one can still use them even with HTTPS, it s not that convenient:

• you need to tunnel all traffic through them, which might result in bottlenecks (especially for media playing/maybe video-conference/etc.).
• or even worse, there might be protocol issues/incompatibilities due to 100% tunneling.
• running a proxy opens up some potential security issues on the internal network, so you need to harden the proxy as well, and maintain it.
• you need to configure all clients to know about the proxy (via DHCP or manually), which might or might not work well, since it s client-dependent.
• you can only block at CONNECT level (host name), and you have to build up regexes for the host name.

On the good side, the actual blocking configuration is centralised, and the only distributed configuration is pointing the clients through the proxy. While I used to run a proxy back in HTTP times, the gains were significant back them (media elements caching, downloads caching, all with a slow pipe, etc.), but today is not worth it, so I ve stopped and won t bring a proxy back just for this.

Method 4: DNS resolver filtering After thinking through all the options, I thought - hey, a caching/recursive DNS resolver is what most people with a local network run, right? How difficult is to block at resolver level? and oh my, it is so trivial, for some resolvers at least. And yes, I didn t know about this a week ago

Response Policy Zones Now, of course, there is a standard for this, called Response Policy Zone, and which is supported across multiple resolvers. There are many tutorials on how to use RPZs to configure things, some of them quite detailed - e.g. this one, or a simple/more straightforward one here. The upstream BIND documentation also explains things quite well here, so you can go that route as well. It looks a bit hairy for me thought, but it works, and since it is a standard, it can be more easily deployed. There are many discussions on the internet about how to configure RPZs, how to not even resolve the names (if you re going to return something explicitly/statically), etc. so there are docs, but again it seems a bit overdone.

Resolver hooks There s another way too, if your resolver allows scripting. For example, the PowerDNS resolver allow Lua scripting, and has a relatively simple API at least, to me it looks way, way simpler than the RPZ equivalent. After 20 minutes of reading the docs, I ended up with this, IMO trivial, solution (in a file named e.g. rules.lua):

ads = newDS()
ads:add( 'evilads.com', 'evilads.well-known-cdn.com', 'moreads.net' )

function preresolve(dq)
  if ads:check(dq.qname) then
    dq.rcode = pdns.NXDOMAIN
    return true;
  end
  return false;
end

and that s it. Well, enable it/load the file in the configuration, but nothing else. Syntax is pretty straightforward, matching by suffix here, and if you need more complex stuff, you can of course do it; it s just Lua and a simple API. I don t see any immediate equivalent in Bind, so there s that, but if you can use PowerDNS, then the above solution seems simple for simple cases, and could be extended if needed (not sure in which cases). The only other thing one needs to do is to serve the local/custom resolver to all clients, whether desktop or mobile, and that s it. DNS server is bread-and-butter in DHCP, so better support than proxy, and once the host name has been (mis)resolved, nothing is involved anymore in the communication path. True, your name server might get higher CPU usage, but for home network, this should not be a problem. Can this filtering method (either RPZ or hooks) be worked around by ad networks? Sure, like anything. But changing the base domain is not fun. DNSSEC might break it (note Bind RPZ can be configure to ignore DNSSEC), but I m more worried about DNS-over-HTTPS, which I thought initially it s done for the user, but now I m not so sure anymore. Not being in control even of your own DNS resolver seems evil , but what do I know.

Combined authoritative + recursive solution This solution was provided by Guillem Jover, who uses unbound, which is a combined authoritative name server and recursive resolver in one, and dnsmasq (which is even more things, I think):

For my LANs I use unbound, and then block this kind of thing in /etc/unbound/unbound.conf.d/block.conf, with stuff like:

server:
 local-zone: adsite.example.com refuse

But then for things that are mobile, and might get out of the LAN, such as laptops, I also block with dnsmasq in /etc/dnsmasq.d/block.conf, with stuff like:

 address=/adsite.example.com/

I still use ublock-origin to block stuff at the browser level, though, for yet an extra layer of noise suppression. :)

Thanks for the info!

Happy browsing! 10 lines of Lua, and now for sure I m going to get even fatter without the this natural method will melt your belly fat in 7 days information. Or I will just throw away banana peels without knowing what I could do with hem. After a few days, I asked myself but ads are not so bad, why did I and then realised that yes, ads are not so bad anymore. And Slashdot actually loads faster So, happy browsing!

For once, I've already read and reviewed quite a few of these books. Elizabeth Bear Machine (sff)
Timothy Caulfield Your Day, Your Way (non-fiction)
S.A. Chakraborty The City of Brass (sff)
John Dickerson The Hardest Job in the World (non-fiction)
Tracy Deonn Legendborn (sff)
Lindsay Ellis Axiom's End (sff)
Alix E. Harrow The Once and Future Witches (sff)
TJ Klune The House in the Cerulean Sea (sff)
Maria Konnikova The Biggest Bluff (non-fiction)
Talia Levin Culture Warlords (non-fiction)
Yoon Ha Lee Phoenix Extravagent (sff)
Yoon Ha Lee, et al. The Vela (sff)
Michael Lewis Flash Boys (non-fiction)
Michael Lewis Losers (non-fiction)
Michael Lewis The Undoing Project (non-fiction)
Megan Lindholm Wizard of the Pigeons (sff)
Nathan Lowell Quarter Share (sff)
Adrienne Martini Somebody's Gotta Do It (non-fiction)
Tamsyn Muir Princess Florinda and the Forty-Flight Tower (sff)
Naomi Novik A Deadly Education (sff)
Margaret Owen The Merciful Crow (sff)
Anne Helen Peterson Can't Even (non-fiction)
Devon Price Laziness Does Not Exist (non-fiction)
The Secret Barrister The Secret Barrister (non-fiction)
Studs Terkel Working (non-fiction)
Kathi Weeks The Problem with Work (non-fiction)
Reeves Wiedeman Billion Dollar Loser (non-fiction) Rather a lot of non-fiction in this batch, much more than usual. I've been in a non-fiction mood lately. So many good things to read!

Year 2020. What a year! Sure, already around early January there were rumours/noise about Covid-19, but who would have thought where it will end up! Thankfully, none of my close or extended family was directly (medically) affected by Covid, so I/we had a privileged year compared to so many other people. I thought how to write a mini-summary, but prose is too difficult, so let s just go month-by-month. Please note that my memory is fuzzy after 9 months cooked up in the apartment, so things could 1 month compared to what I wrote.

Timeline

January Ski weekend. Skiing is awesome! Cancelling a US work trip since there will be more opportunities soon (har har!).

February Ski vacation. Yep, skiing is awesome. Can t wait for next season (har har!). Discussions about Covid start in the office, but more is this scary or just interesting? (yes, this was before casualties). Then things start escalating, work-from-home at least partially, etc. etc. Definitely not just intersting anymore. In Garmin-speak, I got ~700+ intensity minutes in February (correlates with activity time, but depends on intensity of the effort whether 1:1 or 2 intensity minutes for one wall-clock minute).

March Sometimes during the month, my workplace introduces mandatory WFH. I remember being the last person in our team in the office, on the last day we were allowed to work, and cleaning my desk/etc., thinking all this, and we ll be back in 3 weeks or so . Har har! I buy a webcam, just in case WFH gets extended. And start to increase my sports - getting double the intensity minutes (1500+).

April Switzerland enters the first, hard, lockdown. Or was it late March? Not entirely sure, but in my mind March was the opening, and April was the first main course. It is challenging, having to juggle family and work and stressed schedule, but also interesting. Looking back, I think I liked April the most, as people were actually careful at that time. I continue upgrading my home office - new sound system, so that I don t have to plug in/plug out cables. 1700+ intensity minutes this month.

May Continued WFH, somewhat routine now. My then internet provider started sucking hard, so I upgrade with good results. I m still happy, half a year later (quite happy, even). Still going strong otherwise, but waiting for summer vacation, whatever it will be. A tiny bit more effort, so 1800 intensity minutes in May.

June Switzerland relaxes the lock down, but not my company, so as the rest of the family goes out and about, I start feeling alone in the apartment. And somewhat angry at it, which impacts my sports (counter-intuitively), so I only get 1500 intensity minutes. I go and buy a coffee machine a real one, that takes beans and grinds them, so I get to enjoy the smell of freshly-ground coffee and the fun of learning about coffee beans, etc. But it occupies the time. On the work/job front, I think at this time I finally got a workstation for home, instead of a laptop (which was ultra-portable too), so together with the coffee machine, it feels like a normal work environment. Well, modulo all the people. At least I m not crying anymore every time I open a new tab in Chrome

July Situation is slowly going better, but no, not my company. Still mandatory WFH, with (if I recall correctly) one day per week allowed, and no meeting other people. I get angrier, but manage to channel my energy into sports, almost doubly my efforts in July - 2937 intensity minutes, not quite reaching the 3000 magic number. I buy more stuff to clean and take care of my bicycles, which I don t really use. So shopping therapy too.

August The month starts with a one week family vacation, but I take a bike too, so I manage to put in some effort (it was quite nice riding TBH). A bit of changes in the personal life (nothing unexpected), which complicates things a bit, but at this moment I really thought Switzerland is going to continue to decrease in infections/R-factor/etc. so things will get back to normal, right? My company expands a bit the work-from-office part, so I m optimistic. Sports wise, still going strong, 2500 intensity minutes, preparing for the single race this year.

September The personal life changes from August start to stabilise, so things become again routine, and I finally get to do a race. Life was good for an extended weekend (well, modulo race angst, but that s part of the fun), and I feel justified to take it slow the week after the race. And the week after that too. I end up the month with close, but not quite, 1900 intensity minutes.

October October starts with school holidays and a one week family vacation, but I feel demotivated. Everything is closing down again (well, modulo schools), and I actually have difficulty getting re-adjusted to no longer being alone in the apartment during the work hours. I only get ~1000 intensity minutes in October, mainly thanks to good late autumn weather and outside rides. And I start playing way more computer games. I also sell my PS4, hoping to get a PS5 next month.

November November continues to suck. I think my vacation in October was actually detrimental - it broke my rhythm, I don t really do sport anymore, not consistently at least, so I only get 700+ intensity minutes. And I keep playing computer games, even if I missed the PS5 ordering window; so I switch to PC gaming. My home office feels very crowded, so as kind of anti-shopping therapy, I sell tons of smallish stuff; can t believe how much crap I kept around while not really using it. I also manage to update/refresh all my Debian packages, since next freeze approaches. Better than for previous releases, so it feels good.

December December comes, end of the year, the much awaited vacation - which we decide to cancel due to the situation in whole of Switzerland (and neighbouring countries). I basically only play computer games, and get grand total of 345 activity minutes this month. And since my weight is inversely correlated to my training, I m basically back at my February weight, having lost all the gains I made during the year. I mean, having gained back all the fat I lost. Err, you know what I mean; I m back close to my high-watermark, which is not good.

Conclusion I was somehow hoping that the end of the year will allow me to reset and restart, but somehow - a few days into January - it doesn t really feel so. My sleep schedule is totally ruined, my motivation is so-so, and I think the way I crashed in October was much harder/worse than I realised at the time, but in a way expected for this crazy year. I have some projects for 2021 - or at least, I m trying to make up a project list - in order to get a bit more structure in my continued stuck inside the house part, which is especially terrible when on-call. I don t know how the next 3-6 months will evolve, but I m thankful that so far, we are all healthy. Actually, me personally I ve been healthier physically than in other years, due to less contact with other people. On the other side, thinking of all the health-care workers, or even service workers, my IT job is comfy and all I am is a spoiled person (I could write many posts on specifically this topic). I really need to up my willpower and lower my spoil level. Hints are welcome :( Wish everybody has a better year in 2021.

Focus This month I didn't have any particular focus. I just worked on issues in my info bubble.

Changes

• duck: add phrases indicating moved and inactive projects
• lintian: bump tag severity
• apt-listchanges: add missing import
• spelling dictionaries: codespell, lintian (1 2)
• Debian website: revert vertical space introduction
• Debian wiki service: update URL
• Debian screenshots: remove wxglade (Windows)
• Debian package uploads: ddccontrol
• Debian wiki pages: ath9k_htc/open_firmware, BCMHybridBTFirmware (1 2), BSP/2020/12/cn/Beijing, CategoryNotNative, DebianInstall, Derivatives/Census/Zevenet, FreedomBox/Manual/SecureShell, LowThresholdAdoption, LowThresholdNmu, MemberBenefits, Mobile, PortTemplate, QemuUserEmulation, RISC-V, Teams/DebianProFTPD, Teams/Dpkg/Spec/BundledBuildinfo, UpstreamGuide, Wine, XTaran/DistUpgradeWorkFlow
• FOSSjobs wiki pages: Resources
• open-ath9k-htc-firmware wiki pages: Troubleshooting-and-bug-reporting

Issues

• Crashes in gnome-shell-extension-hamster, libvdpau-va-gl
• Invasive signup process on SourceForge
• Missing upstream in webext-umatrix
• Features in lintian (1 2), webext-debianbuttons, cruft-ng, gparted, reportbug
• Regressions in evolution (1 2 3)
• Conffile handling in speech-dispatcher
• Misuse of /var in smartmontools
• Broken symlinks in gtk-doc-tools, plymouth-themes
• Cruft in qemu-user-static
• Typos in qml-module-org-kde-prison, libuhd4.0.0-dpdk-tests
• Broken apt sources in mariadb-10.5
• Code copies in ThermalMonitor
• New release needed for ddccontrol

Review

• Spam: reported 1 Debian bug reports and 144 Debian mailing list posts
• Debian packages: sponsored opentype-sanitiser, gtranscribe, open-ath9k-htc-firmware
• Debian wiki: RecentChanges for the month
• Debian screenshots:
  • approved fonts-jetbrains-mono geda-gschem gnome-maps gnome-shell-extension-dashtodock gnome-todo paper-icon-theme plan remmina sayonara sway wxglade
  • rejected ghostscript (wrong package), emacs-goodies-el (unrelated web browser), csv2latex (help output, bad quality), dwarf-fortress (non-free)
  • approved deletion of sdcc (another package)
  • rejected deletion of hashcat/olive-editor (spam)

Administration

• Debian: restart bacula director, ping some people about disk usage
• Debian wiki: unblock IP addresses, approve accounts, update email for accounts with bouncing email

Communication

• Respond to queries from Debian users and contributors on the mailing lists and IRC

Sponsors All work was done on a volunteer basis.

Review: Billion Dollar Loser, by Reeves Wiedeman

Publisher:	Little, Brown and Company
Copyright:	October 2020
ISBN:	0-316-46134-2
Format:	Kindle
Pages:	315

WeWork was founded in 2010 by Adam Neumann and Miguel McKelvey as a successor company to their similar 2008 GreenDesk business. (Adam's wife Rebekah is now presented as a co-founder. This seems dubious in Wiedeman's account, although Rebekah's role in the company is murky, ever-changing, and hard to pin down.) Its business model in reality was to provide turn-key, pre-furnished and stocked co-working and small office space to individuals and businesses on flexible, short-term leases. Its business model in Neumann's speeches and dreams, and represented by the later renaming of the company to the We Corporation, was nothing less than to transform the way people worked, learned, and lived. Through aggressive, money-losing expansion, WeWork grew rapidly to over 500 locations in 29 countries and became the largest office tenant in New York City. Based primarily on massive financial support from Masayoshi Son, CEO of Japanese holding company SoftBank, WeWork's private valuation rose to $47 billion. In 2019, the company attempted to go public, but its IPO collapsed, in part due to deeper analysis of the company's books. Neumann was forced out of the company (with an individual payout valued at $1.7 billion), the IPO was withdrawn, SoftBank wrote down 90% of their investment in the company and took control of it, and WeWork laid off more than 20% of its workforce. This book is a detailed history of WeWork's rise and fall, joining a genre that includes The Smartest Guys in the Room (Enron), Bad Blood (Theranos), and Super Pumped (Uber). I believe it's the first full book on WeWork, although it was preceded by several long-form stories, including "The I In We" by Wiedeman for New York magazine. As the first history, it's a somewhat incomplete cut: litigation between Neumann and WeWork is still pending, WeWork staggered into 2020 and a world-wide pandemic that made cramped open-plan offices an epidemiological disaster, and there will doubtless be new revelations yet to come. The discovery process of lawsuits tends to be good for journalists. But despite being the first out of the gate, Billion Dollar Loser reaches a satisfying conclusion with the ouster of Neumann, who had defined WeWork both internally and externally. I'm fascinated by stories of failed venture capital start-ups in general, but the specific question about WeWork that interested me, and to which Wiedeman provides a partial answer, is why so many people gave Neumann money in the first place. Explaining that question requires a digression into why I thought WeWork's valuation was absurd. The basic problem WeWork had when justifying its sky-high valuation is competition. WeWork didn't own real estate; it rented properties from landlords with long-term leases and then re-rented them with short-term leases. If its business was so successful, why wouldn't the landlords cut out the middle man, do what WeWork was doing directly, and pocket all the profit? Or why wouldn't some other company simply copy WeWork and drive the profit margins down? Normally with startups the answer revolves around something proprietary: an app, a server technology, patents, a secret manufacturing technique, etc. But nothing WeWork was doing was different from what innumerable tech companies and partner landlords had been doing with their office space for a decade, and none of it was secret. There are two decent answers to that question. One is simple outsourcing: landlords like being passive rent collectors, so an opportunity to pay someone else to do the market research on office layouts, arrange all the remodeling, adapt to changing desires for how office space should be equipped and stocked, advertise for short-term tenants, and deal with the tenant churn is attractive. The landlord can sit back and pocket the stable long-term rent. The second answer is related: WeWork is essentially doing rental arbitrage between long-term and short-term rents and thus is taking on most of the risk of a commercial real estate downturn. If no one is renting office space, WeWork is still on the hook for the long-term rent. The landlord is outsourcing risk, at least unless WeWork goes bankrupt. (One infuriating tidbit from this book is that Neumann's explicit and often-stated goal was to make WeWork so large that its bankruptcy would be sufficiently devastating to the real estate industry that it would get a bailout.) There's a legitimate business here. But that business looks like a quietly profitable real estate company that builds very efficient systems for managing short-term leases, remodeling buildings, and handling the supply chain of stocking an office. That looks nothing like WeWork's business, has nothing to do with transforming the world of work, and certainly doesn't warrant sky-high valuations. WeWork didn't build an efficient anything. It relied on weekend labor from underpaid employees and an IT person who was still in high school. And WeWork actively resisted being called a real estate company and claimed it was a tech company or a lifestyle company on the basis of essentially nothing. Wiedeman seems almost as baffled by this as I am, but it's clear from the history he tells that part of the funding answer is the Ponzi scheme of start-up investing. People gave Neumann money because other people had previously given Neumann money, and the earlier investors cashed out at the expense of the later ones. Like any Ponzi scheme, it looks like a great investment until it doesn't, and then the last sucker is left holding the bag. That sucker was Masayoshi Son, who in Wiedeman's telling is an astonishingly casual and undisciplined investor who trusted knee-jerk personal reactions to founders over business model analysis and historically (mostly) got away with it by getting extremely lucky. (I now want to read one of these books about SoftBank, since both this book and Super Pumped make it look like a company that makes numerous wild gambles for the flimsiest of reasons, pushes for completely unsustainable growth, and relies on the sheer volume of investments catching some lucky jackpots and cashing out in IPOs. Unfortunately, the only book currently available seems to be a fawning hagiography of Son.) On one hand, the IPO process worked properly this time. The sheer madness of WeWork's valuation scared off enough institutional investors that it collapsed. On the other hand, it's startling how close it came to success. If WeWork had kept the Ponzi scheme going a bit longer, the last sucker could have been the general investing public. Another interesting question that Billion Dollar Loser answers is how Neumann got enough money to start his rapid growth strategy. The answer appears to be the oldest and most obvious explanation: He made friends with rich people. The initial connections appear to have been through his sister, Adi Neumann, who is a model and hosted parties in her New York apartment (and also started dating a Rothschild heir). Adam met his wealthy wife Rebekah, cousin to actress and "wellness" scam marketer Gwyneth Paltrow, via a connection at a party. He built social connections with other parts of the New York real estate scene and tapped them for investment money. The strong impression one gets from the book is that all of these people have way more money than sense and we should raise their taxes. It won't come as a surprise that Adam and Rebekah Neumann are good friends of Jared Kushner and Ivanka Trump. Those are the questions I was the most curious about, but there's much more here. Wiedeman's style is nearly straight chronological reporting with little analysis, but the story is so wild and absurd that it doesn't need much embellishment. Neumann is obviously a megalomaniac whose delusions of grandeur got worse and worse as WeWork was apparently succeeding. Rebekah Neumann is if anything even less in touch with reality than he is, although in her case that appears to stem from having so much money that reality is an inconvenient speed bump. Miguel McKelvey, Neumann's co-founder, is an odd and interesting side note to the story; he appears to have balanced Adam out a bit in the early going but then wisely started to cash out and pocket his winnings while letting Adam dominate the stage. There are some places where I don't think Wiedeman pushed hard enough, and which cut against the view of Neumann as a true believer in his impossible growth vision. Neumann took several investment opportunities to cash out large amounts of his stock even while WeWork employees were being underpaid and told their stock options would make up for it. He clearly used WeWork as a personal piggy bank on multiple occasions. And Wiedeman documents but doesn't, at least in my opinion, make nearly enough of Neumann's self-dealing: buying real estate that WeWork then rented as a tenant, or paying himself for a license for the name We Holdings (although there at least he later returned the money). I think a good argument could be made that Neumann was embezzling from WeWork, at least morally if not legally, and I wish Wiedeman would have pressed harder on that point. But that aside, this is a great first history of the company, told in a clean, readable, and engaging style, and with a lot more detail here than I've touched on (such as Rebekah Neumann's WeGrow school). It's not as good as Bad Blood (what is), but it's a respectable entry in the corporate collapse genre. If you like this sort of thing, recommended. Rating: 7 out of 10

Like each month, here comes a report about the work of paid contributors to Debian LTS. Individual reports In November, 239.25 work hours have been dispatched among 13 paid contributors. Their reports are available:

• Abhijith PA did 12.0h (out of 12h assigned).
• Adrian Bunk did 13h (out of 22.75h assigned and 19.5h from October) and gave back 6.5h, thus carrying over 22.75h to December.
• Ben Hutchings did 11.5h (out of 16h assigned and 4.5h from October), thus carrying over 9h to December.
• Brian May did 10h (out of 10h assigned).
• Chris Lamb did 18h (out of 18h assigned).
• Emilio Pozuelo Monfort did 22.75h (out of 22.75h assigned).
• Holger Levsen did 8.0h coordinating/managing the LTS team.
• Markus Koschany did 12h (out of 22.75h assigned), thus carrying over 10.75h to December.
• Ola Lundqvist did 1h (out of 12h assigned), thus carrying over 11h to December.
• Roberto C. S nchez did 20.5h (out of 22.75h assigned), thus carrying over 2.25h to December.
• Sylvain Beucler did 22.75h (out of 22.75h assigned).
• Thorsten Alteholz did 22.75h (out of 22.75h assigned).
• Utkarsh Gupta did 22.75h (out of 22.75h assigned).

Evolution of the situation In November we held the last LTS team meeting for 2020 on IRC, with the next one coming up at the end of January.
We announced a new formalized initiative for Funding Debian projects with money from Freexian s LTS service.
Finally, we would like to remark once again that we are constantly looking for new contributors. Please contact Holger if you are interested! We re also glad to welcome two new sponsors, Moxa, a device manufacturer, and a French research lab (Institut des Sciences Cognitives Marc Jeannerod). The security tracker currently lists 37 packages with a known CVE and the dla-needed.txt file has 40 packages needing an update. Thanks to our sponsors Sponsors that joined recently are in bold.

• Platinum sponsors:
• TOSHIBA (for 63 months)
• GitHub (for 53 months)
• Civil Infrastructure Platform (CIP) (for 31 months)
• Gold sponsors:
• Blablacar (for 78 months)
• Roche Diagnostics International AG (for 74 months)
• Linode (for 68 months)
• Babiel GmbH (for 57 months)
• Plat Home (for 56 months)
• University of Oxford (for 13 months)
• Silver sponsors:
• The Positive Internet Company (for 79 months)
• Domeneshop AS (for 78 months)
• Nantes M tropole (for 72 months)
• Univention GmbH (for 64 months)
• Universit Jean Monnet de St Etienne (for 64 months)
• Ribbon Communications, Inc. (for 58 months)
• Exonet B.V. (for 47 months)
• Leibniz Rechenzentrum (for 41 months)
• CINECA (for 31 months)
• Minist re de l Europe et des Affaires trang res (for 25 months)
• Cloudways Ltd (for 14 months)
• Dinahosting SL (for 12 months)
• Platform.sh (for 7 months)
• Bauer Xcel Media Deutschland KG (for 6 months)
• Moxa Intelligence Co., Ltd.
• Bronze sponsors:
• Seznam.cz, a.s. (for 79 months)
• Evolix (for 78 months)
• Linuxhotel GmbH (for 76 months)
• Intevation GmbH (for 75 months)
• Daevel SARL (for 74 months)
• Bitfolk LTD (for 73 months)
• Megaspace Internet Services GmbH (for 73 months)
• Greenbone Networks GmbH (for 72 months)
• NUMLOG (for 72 months)
• WinGo AG (for 71 months)
• Ecole Centrale de Nantes LHEEA (for 68 months)
• Entr ouvert (for 63 months)
• Adfinis AG (for 60 months)
• Tesorion (for 55 months)
• GNI MEDIA (for 54 months)
• Laboratoire LEGI UMR 5519 / CNRS (for 54 months)
• Bearstech (for 46 months)
• LiHAS (for 46 months)
• People Doc (for 42 months)
• Catalyst IT Ltd (for 40 months)
• Supagro (for 36 months)
• Demarcq SAS (for 34 months)
• Universit Grenoble Alpes (for 21 months)
• TouchWeb SAS (for 12 months)
• SPiN AG (for 9 months)
• CoreFiling (for 5 months)
• Institut des sciences cognitives Marc Jeannerod

One comment Liked this article? Click here. My blog is Flattr-enabled.

Review: Because Internet, by Gretchen McCulloch

Publisher:	Riverhead Books
Copyright:	2019
ISBN:	0-7352-1095-0
Format:	Kindle
Pages:	276

If you're familiar with linguistics as a field of scientific study (as opposed to the tool-based fields of grammar or writing advice), you'll be familiar with the dichotomy between written and spoken language. We may spend more time thinking about written language since it is central to most types of education and carries much of the intellectual and social weight of society. Linguists, however, see spoken language as more fundamental, since speech is wired into our brains and universal in human societies. Written language is a recent and somewhat artificial invention. One also learns from linguistics that spoken language does not follow many of the rules of written language that we painstakingly memorized in school. In casual speech, people split infinitives, speak in partial and run-on sentences, ignore nit-picking pronoun case rules, and rarely notice or care about the difference between less and fewer. Spoken language does have rules, but they're more subtle and nuanced than the grammar rules we learn in school. (I think the real fun of linguistics is separating the rules that native speakers follow effortlessly from the artificial rules used as education markers.) This is, in part, because nearly all spoken language is informal, whereas nearly all written language is formal. Enter the Internet, and enter this book. For the first time in human history we have both an explosion of informal writing and easy availability of that writing to linguists for study. Informal writing is not entirely new, of course. We've had personal letters for nearly as long as we've had writing, not to mention private notes, diaries, and other writing intended for tiny audiences. But consider who wrote private letters and, on top of that historical filter, whose private letters were preserved for linguistic research. Until relatively recently, only the upper classes were literate and had access to the infrastructure to write and send letters. Someone's letters or private notes were unlikely to be preserved unless they were someone famous and important, and thus often well-educated and more likely to take a more formal tone in writing. If you compare this to the Internet-driven blizzard of work and personal email, SMS conversations, chatrooms, and social media posts, the difference is obvious in both volume and level of informality. We're all on the Internet, we all read and write with a frequency that would be staggering to the average person from even fifty years ago, and while one may take a bit of additional care with a tricky email to one's manager, the SMS message to one's friend is as informal of a use of language as a conversation over coffee. Gretchen McCulloch is a professional linguist and Because Internet is about exactly this phenomenon: the new conventions of informal writing, how it has changed and evolved, and the new subtleties and shortcuts we've invented to make written communication easier. That goes beyond words and grammar to encompass punctuation, emoji and emoticons, memes and reaction gifs, and even the subtleties of timing, whitespace, and the construction of virtual places via our choices in how and where we write. This topic is my catnip, so it's not surprising I love this book. I've been heavily involved with online communities that communicate in writing since 1993 (making me, in McCulloch's classification, an Old Internet Person; each wave of introduction to the Internet has its own conventions that can be in conflict with later waves). I've now spent more than half my life carrying out most of my social activity and most of my closest friendships primarily in writing, so I found a lot of satisfaction in a linguistic study that takes that seriously rather than treating it as a curiosity. But, even better, I was amazed at how much I didn't know, in part because I am from a specific wave. I have a deep intuition for the Usenet conventions, but not as good of an understanding of the ones from AIM and LiveJournal one wave later (the Full Internet People). And I had a lot to learn about the conventions of the Instagram and Snapchat cluster (the Post Internet People, who have never known life without the Internet). One of the things that struck me while reading this book is how most of the language innovations that McCulloch describes are addressing the old complaint that written communication is inferior to face-to-face conversation because it lacks emotional nuance. My knee-jerk reply is that, no, written communication is full of emotional nuance and the complainer is just bad at reading it, but that's somewhat unfair. A better statement of the problem is that there is not a standardized language for emotional nuance in written communication, in part because it's so new in human history. Most humans are extremely good at reading facial expressions and body language for emotional cues, and those physical expressions are largely subconscious, reliable, and similar among different people (particularly within a culture; one can get in trouble with body language variations across cultures). This is not true of writing. With friends I've talked to over chat for twenty-five years, I can read volumes about their emotional state in a couple of short lines of text. But with strangers, despite decades of Internet communications, I will still misread cues and misinterpret simple intentions. The other standard response to this complaint is that it is possible to put extensive emotional nuance into formal writing. Just get better at writing! This is true, but unhelpful. There's a reason why we give book contracts to people who are very good at investing formal writing with emotional nuance. It's difficult, time-consuming, and requires a great deal of practice. That may be appropriate for formal, paid writing, but it won't do for informal writing, which by definition needs to be as effortless as possible. It's therefore unsurprising that once millions of people were using the Internet regularly for informal writing, they started adding new mechanisms, shortcuts, and conventions for emotional nuance. The standardization is growing, but conventions still vary widely between waves of Internet users. One of the most fascinating parts of this book for me was McCulloch's explanation of why periods (and, to a lesser extent, capital letters) in short chat messages are perceived by younger users as harsh or passive-aggressive. I still have the formal writing mindset of treating proper capitalization and punctuation as a point of pride, but McCulloch makes an excellent argument for letting go of my biases and understanding how and why language is changing. The realization I had while reading this is that many of the changes that look like sloppiness or laziness to someone trained in formal writing have the effect of giving language greater dynamic range. If one always uses periods uniformly, the period becomes meaningless except as a sentence boundary (which is redundant with newlines in most short informal chat messages). If one normally doesn't use it, and then suddenly starts using it, the period can carry semantic weight. It can convey a snippy tone of voice, a note of annoyance, or other subtle shades of meaning. I still use periods in most of my Slack messages because habits are hard to break, but I'm remembering to leave them off some of the time and paying more attention to what emotional weight they're carrying when present. Because Internet is therefore the rare book that meets the bar of changing my day-to-day behavior. "lol" is another excellent example that McCulloch spends some time on. It started life as LOL, an abbreviation for "laughing out loud," and that's still how it's stuck in my head. But, as McCulloch explains, it no longer means that to newer waves of Internet users. It now carries a far more complicated and nuanced meaning that has very little to do with physical laughter and that doesn't easily translate to a single word or sentence. I went from being mildly irritated by and mildly superior towards the ubiquitous "lol" to realizing that it's a fascinating new word that carries primarily emotional nuance and that I don't understand well enough to read or use properly (yet). One more example of the type of analysis McCulloch brings to this book: emoji. The tendency when talking about emoji is to treat them as rebuses (pictures that stand in for a word, or at least a specific concept). They are sometimes used that way, but McCulloch argues that they more often function in the same role that gestures play in informal speech, including the gestures that have no simple name and no independent meaning outside of the context of the words being said at the same time. This seems obvious in retrospect, but before reading Because Internet I had never thought about what a gesture is, what function it plays in speech, and how that could be translated into informal written communication. If you're as interested in this area as I am, this is great stuff. I'd seen several mentions of this book go past on Twitter and kept holding off because I had lots of things to read and was worried it would only cover the superficial things I already knew as a long-time Internet user who has listened to a few lectures on linguistics. That was not the case at all. I learned so much from this book and had a delightful time reading it. If you're also interested in these topics, recommended. Rating: 9 out of 10

TL;DR: Some mildly tricky tricks allow you to select subgoals by name, like in Isabelle. This leads to more readable proofs, and proofs that are more robust against changes.

The need for case names Consider the following Coq proof, right out of the respected Software Foundations book, Chapter Inductively Defined Propositions (and slightly simplified):

Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re ->
  s2 =~ Star re ->
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
   generalize dependent s2.
  induction H1.
  - (* MEmpty *) discriminate.
  - (* MChar *) discriminate.
  - (* MApp *) discriminate.
  - (* MUnionL *) discriminate.
  - (* MUnionR *) discriminate.
  - (* MStar0 *)
    injection Heqre' as Heqre''. intros s H. apply H.
  - (* MStarApp *)
    injection Heqre' as Heqre''.
    intros s3 H1. rewrite <- app_assoc.
    apply MStarApp.
    + apply H1_.
    + apply IHexp_match2.
      * rewrite Heqre''. reflexivity.
      * apply H1.
Qed.

This is a very typical example for a proof by induction over an inductively defined relation (in this case, the relations s =~ re which indicates that the string s matches the regular expression re): After some preparation, the invocation of a tactic like induction (could also be inversion or others) creates a number of new goals, one of for each rule of the relation. Then the modern(!) Coq user uses proof bullets to focus the goals, one after another, in order, to solve them. We can see from this example that proof bullets (which were a big improvement) are not quite satisfactory, and the author of this proof felt the need to annotate each subproof with the case it corresponds to. But these are mere comments! This is unsatisfactory, as there is nothing keeping them correct as my proof changes. And anyone who came to Coq from Isabelle is just flabbergasted that the state of art in Coq is still at that level So, wouldn t it be great if

• I could focus goals by their name (e.g. MEmpty)
• Focus them in any order (so that refactoring of my data types do not break my proofs)
• This even worked when simultaneously inducting over or inverting multiple relations?

Simulating named goals in Coq Well, with a few tricks we can! It just takes three simple steps:

1. I load a small file full of hacks (explained below):

   Require Import NamedCases.

2. This allows me to prefix the type of the constructors of the inductive relations (i.e. the rules of the relation) with case <name>, , as follows:

   Reserved Notation "s =~ re" (at level 80).
   Inductive exp_match  T  : list T -> reg_exp T -> Prop :=
       MEmpty:
       case empty,
       [] =~ EmptyStr
       MChar:
       case char,
       forall x,
       [x] =~ (Char x)
       MApp:
       case app,
       forall s1 re1 s2 re2
       (H1 : s1 =~ re1)
       (H2 : s2 =~ re2),
       (s1 ++ s2) =~ (App re1 re2)
       MUnionL:
       case union_l,
       forall s1 re1 re2
       (H1 : s1 =~ re1),
       s1 =~ (Union re1 re2)
       MUnionR:
       case union_r,
       forall re1 s2 re2
       (H2 : s2 =~ re2),
       s2 =~ (Union re1 re2)
       MStar0:
       case star0,
       forall re,
       [] =~ (Star re)
       MStarApp:
       case star_app,
       forall s1 s2 re
       (H1 : s1 =~ re)
       (H2 : s2 =~ (Star re)),
       (s1 ++ s2) =~ (Star re)
     where "s =~ re" := (exp_match s re).

   This is the definition from the Software Foundations book; only the case <name>, lines are added.
3. Now I can change the proof: After the induction tactic I use ; name_cases to name the cases, and then I can use the relatively new named goal focusing feature ([name]: , which I suggested two years ago, and was implemented by Th o Zimmermann) to focus a specific case:

   Lemma star_app2: forall T (s1 s2 : list T) (re : reg_exp T),
     s1 =~ Star re ->
     s2 =~ Star re ->
     s1 ++ s2 =~ Star re.
   Proof.
     intros T s1 s2 re H1.
     remember (Star re) as re'.
      generalize dependent s2.
     induction H1; name_cases.
     [empty]:  
        discriminate.
      
     [char]:  
        discriminate.
      
     [app]:  
        discriminate.
      
     [unionL]:  
        discriminate.
      
     [unionR]:  
       discriminate.
      
     [star0]:  
       injection Heqre' as Heqre''. intros s H. apply H.
      
     [starApp]:  
       injection Heqre' as Heqre''.
       intros s3 H1. rewrite <- app_assoc.
       apply MStarApp; clear_names.
       + apply H1_.
       + apply IHexp_match2.
         * rewrite Heqre''. reflexivity.
         * apply H1.
       
   Qed.

   The comments have turned into actual names!

Goal focusing is now just much more reliable. For example, let me try to discharge the boring cases by using ; try discriminate after the induction. This means there are suddenly only two goals left. With bullets, the first bullet would now suddenly focus a different goal, and my proof script would likely fail somewhere. With named goals, I get a helpful error message No such goal: empty and I can t even enter the first subproof. So let me delete these goals and, just to show off, focus the remaining goals in the wrong order:

Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re ->
  s2 =~ Star re ->
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
   generalize dependent s2.
  induction H1; name_cases; try discriminate.
  [starApp]:  
    injection Heqre' as Heqre''.
    intros s3 H1. rewrite <- app_assoc.
    apply MStarApp; clear_names.
    + apply H1_.
    + apply IHexp_match2.
      * rewrite Heqre''. reflexivity.
      * apply H1.
    
  [star0]:  
    injection Heqre' as Heqre''. intros s H. apply H.
   
Qed.

I did not explain the clear_names tactic yet that I had to use after apply MStarApp. What I am showing here is a hack, and it shows these case names are extra hypothesis (of a trivially true type CaseName), and this tactic gets rid of it.

Even better than Isabelle The above even works when there are multiple inductions/inversions involved. To give an example, let s introduce another inductive predicate, and begin proving a lemma that one can do by induction on one and inversion on the other predicate.

Inductive Palindrome  T  : list T -> Prop :=
  EmptyPalin:
  case emptyP,
  Palindrome []
  SingletonPalin:
  case singletonP,
  forall x,
  Palindrome [x]
  GrowPalin:
  case growP,
  forall l x,
  Palindrome l -> Palindrome ([x] ++ l ++ [x])
.
Lemma palindrome_star_of_two:
  forall T (s : list T) x y,
  Palindrome s -> s =~ Star (App (Char x) (Char y)) ->
  s = [] \/ x = y.
Proof.
  intros T s x y HPalin HRe.
  induction HPalin; inversion HRe; name_cases.

At this point we have four open goals. Can you tell why there are four, and which ones they are? Luckily, Show Existentials will tell us their names (and Coq 8.13 will just show them in the proof state window). These names not only help us focus the goal in a reliable way; they even assist us in understanding what goal we have to deal with. For example, the last goal arose from the GrowP rule and the StarApp rule. Neat!

  [emptyP_star0]:  
    left. reflexivity.
   
  [emptyP_starApp]:  
     left. reflexivity.
   
  [singletonP_starApp]:  
    inversion HRe; clear HRe.
    inversion H5; clear H5.
    inversion H10; clear H10.
    inversion H11; clear H11.
    subst.
    inversion H3.
   
 [growP_starApp]:  
    admit. (* I did not complete the proof *)
  

Under the hood (the hack) The above actually works, but it works with a hack, and I wish that Coq s induction tactic would just do the right thing here. I hope eventually this will be the case, and this section will just be curiosity but until, it may actually be helpful.

1. The trick¹ is to leave markers in the proof state. We use a dedicate type CaseName, and a hypothesis name : CaseName indicates that this goal arose from the that case.

   Inductive CaseName := CaseNameI.

   With this, we can write StarApp: forall (starApp : CaseName), to name this case.
2. For a little bit of polish, we can introduce notation for that:

   Notation "'case' x , t" := (forall  x : CaseName , t) (at level 200).

   This allows us to use the syntax you saw above.
3. To easily discharge these CaseName assumptions when using the introduction forms, I wrote these tactics:

   Ltac clear_names := try exact CaseNameI.
   Ltac named_constructor  := constructor; [ exact CaseNameI   idtac .. ].
   Ltac named_econstructor := econstructor; [ exact CaseNameI   idtac .. ].

4. Finally I wrote the tactic name_cases. What it does is relatively simple:

   For each subgoal: Take all hypotheses of type CaseName, concatenate their names, change the name of the current goal to that, and clear these hypotheses

   Unfortunately, my grasp of Coq tactic programming is rather rudimentary, and the only way I manged to solve this is a horrible monster of Ltac2, including hand-rolled imperative implementations of string concatenation and a little nested Ltac1 tactic within. You have been warned:

   From Ltac2 Require Import Ltac2.
   From Ltac2 Require Option.
   Set Default Proof Mode "Classic".
   Ltac name_cases := ltac2:(
     (* Horribly manual string manipulations. Does this mean I should
        go to the Ocaml level?
     *)
     let strcpy s1 s2 o :=
       let rec go := fun n =>
         match Int.lt n (String.length s2) with
           true => String.set s1 (Int.add o n) (String.get s2 n); go (Int.add n 1)
           false => ()
         end
       in go 0
     in
     let concat := fun s1 s2 =>
       let l := Int.add (Int.add (String.length s1) (String.length s2)) 1 in
       let s := String.make l (Char.of_int 95) in
       strcpy s s1 0;
       strcpy s s2 (Int.add (String.length s1) 1);
       s
     in
     Control.enter (let rec go () :=
       lazy_match! goal with
         [ h1 : CaseName, h2 : CaseName  - _ ] =>
         (* Multiple case names? Combine them (and recurse) *)
         let h := concat (Ident.to_string h1) (Ident.to_string h2) in
         Std.clear [h1; h2];
         let h := Option.get (Ident.of_string h) in
         assert ($h := CaseNameI);
         go ()
         [ _ : CaseName  - _ ] =>
         (* A single case name? Set current goal name accordingly. *)
         ltac1:(
           (* How to do this in ltac2? *)
           lazymatch goal with
             [ H : CaseName  - _ ] => refine ?[H]; clear H
           end
         )
         [  - _ ] =>
         Control.backtrack_tactic_failure "Did not find any CaseName hypotheses"
       end
     in go)
   ).

   If someone feels like re-implementing this in a way that is more presentable, I ll be happy to update this code (and learn something along the way

That s all it takes!

Conclusion With some mild hackery, we can get named cases in Coq, which I find indispensable in managing larger, evolving proofs. I wonder why this style is not more common, and available out of the box, but maybe it is just not known well enough? Maybe this blog post can help a bit here.

---

1. I have vague recollections of seeing at least parts of this trick on some blog some years ago, and I do not claim originality here.

Earlier this month Daniel, Lars and myself got together to discuss Bryan Cantrill s article Rust after the honeymoon. This is an overview of what keeps him enjoying working with Rust after having used it for an extended period of time for low level systems work at Oxide, we were particularly interested to read a perspective from someone who was both very experienced in general and had been working with the language for a while. While I have no experience with Rust both Lars and Daniel have been using it for a while and greatly enjoy it. One of the first areas we discussed was data bearing enums these have been very important to Bryan. In keeping with a pattern we all noted these take a construct that s relatively commonly implemented by hand in C (or skipped as too much effort, as Lars found) and provides direct support in the language for it. For both Daniel and Lars this has been key to their enjoyment of Rust, it makes things that are good practice or common idioms in C and C++ into first class language features which makes them more robust and allows them to fade into the background in a way they can t when done by hand. Daniel was also surprised by some omissions, some small such as the ? operator but others much more substantial the standout one being editions. These aim to address the problems seen with version transitions in other languages like Python, allowing individual parts of a Rust program to adopt potentially incompatible language features while remaining interoperability with older editions of the language rather than requiring the entire program to be upgraded en masse. This helps Rust move forwards with less need to maintain strict source level compatibility, allowing much more rapid evolution and helping deal with any issues that are found. Lars expressed the results of this very clearly, saying that while lots of languages offer a 20%/80% solution which does very well in specific problem domains but has issues for some applications Rust is much more able to move towards a much more general applicability by addressing problems and omissions as they are understood. This distracted us a bit from the actual content of the article and we had an interesting discussion of the issues with handling OS differences in filenames portably. Rather than mapping filenames onto a standard type within the language and then have to map back out into whatever representation the system actually uses Rust has an explicit type for filenames which must be explicitly converted on those occasions when it s required, meaning that a lot of file handling never needs to worry about anything except the OS native format and doesn t run into surprises. This is in keeping with Rust s general approach to interfacing with things that can t be represented in its abstractions, rather than hide things it keeps track of where things that might break the assumptions it makes are and requires the programmer to acknowledge and handle them explicitly. Both Lars and Daniel said that this made them feel a lot more confident in the code that they were writing and that they had a good handle on where complexity might lie, Lars noted that Rust is the first languages he s felt comfortable writing multi threaded code in. We all agreed that the effect here was more about having idioms which tend to be robust and both encourage writing things well and gives readers tools to help know where particular attention is required no tooling can avoid problems entirely. This was definitely an interesting discussion for me with my limited familiarity with Rust, hopefully Daniel and Lars also got a lot out of it!

Twice this week I was asked how it can be okay to work on free software when there are issues like climate change and racial injustice. I have a few answers for that. You can work on injustice while working on free software. A world in which all technology is just cannot exist under capitalism. It cannot exist under racism or sexism or ableism. It cannot exist in a world that does not exist if we are ravaged by the effects of climate change. At the same time, free software is part of the story of each of these. The modern technology state fuels capitalism, and capitalism fuels it. It cannot exist without transparency at all levels of the creation process. Proprietary software and algorithms reinforce racial and gender injustice. Technology is very guilty of its contributions to the climate crisis. By working on making technology more just, by making it more free, we are working to address these issues. Software makes the world work, and oppressive software creates an oppressive world. You can work on free software while working on injustice. Let s say you do want to devote your time to working on climate justice full time. Activism doesn t have to only happen in the streets or in legislative buildings. Being a body in a protest is activism, and so is running servers for your community s federated social network, providing wiki support, developing custom software, and otherwise bringing your free software skills into new environments. As long as your work is being accomplished under an ethos of free software, with free software, and under free software licenses, you re working on free software issues while saving the world in other ways too! Not everyone needs to work on everything all the time. When your house in on fire, you need to put out the fire. However, maybe you can t help put out the first. Maybe You don t have the skills or knowledge or physical ability. Maybe your house is on fire, but there s also an earthquake and a meteor and a airborn toxic event all coming at once. When that happens, we have to split up our efforts and that s okay.

In some ways it is sad and interesting to see how personal liberty is viewed in India. And how it differs from those having the highest fame and power can get a different kind of justice then the rest cannot.

Arnab Goswami This particular gentleman is a class apart. He is the editor as well as Republic TV, a right-leaning channel which demonizes the minority, women whatever is antithesis to the Central Govt. of India. As a result there have been a spate of cases against him in the past few months. But surprisingly, in each of them he got hearing the day after the suit was filed. This is unique in Indian legal history so much so that a popular legal site which publishes on-going cases put up a post sharing how he was getting prompt hearings. That post itself needs to be updated as there have been 3 more hearings which have been done back to back for him. This is unusual as there have been so many cases pending for the SC attention, some arguably more important than this gentleman . So many precedents have been set which will send a wrong message. The biggest one, that even though a trial is taking place in the sessions court (below High Court) the SC can interject on matters. What this will do to the morale of both lawyers as well as judges of the various Sessions Court is a matter of speculation and yet as shared unprecedented. The saddest part was when Justice Chandrachud said

Justice Chandrachud If you don t like a channel then don t watch it. 11th November 2020 .

This is basically giving a free rope to hate speech. How can a SC say like that ? And this is the Same Supreme Court which could not take two tweets from Shri Prashant Bhushan when he made remarks against the judiciary .

J&K pleas in Supreme Court pending since August 2019 (Abrogation 370) After abrogation of 370, citizens of Jammu and Kashmir, the population of which is 13.6 million people including 4 million Hindus have been stuck with reduced rights and their land being taken away due to new laws. Many of the Hindus which regionally are a minority now rue the fact that they supported the abrogation of 370A . Imagine, a whole state whose answers and prayers have not been heard by the Supreme Court and the people need to move a prayer stating the same.

100 Journalists, activists languishing in Jail without even a hearing 55 Journalists alone have been threatened, booked and in jail for reporting of pandemic . Their fault, they were bring the irregularities, corruption made during the pandemic early months. Activists such as Sudha Bharadwaj, who giving up her American citizenship and settling to fight for tribals is in jail for 2 years without any charges. There are many like her, There are several more petitions lying in the Supreme Court, for e.g. Varavara Rao, not a single hearing from last couple of years, even though he has taken part in so many national movements including the emergency as well as part-responsible for creation of Telengana state out of Andhra Pradesh .

Then there is Devangana kalita who works for gender rights. Similar to Sudha Bharadwaj, she had an opportunity to go to UK and settle here. She did her master s and came back. And now she is in jail for the things that she studied. While she took part in Anti-CAA sittings, none of her speeches were incendiary but she still is locked up under UAPA (Unlawful Practises Act) . I could go on and on but at the moment these should suffice.

Petitions for Hate Speech which resulted in riots in Delhi are pending, Citizen s Amendment Act (controversial) no hearings till date. All of the best has been explained in a newspaper article which articulates perhaps all that I wanted to articulate and more. It is and was amazing to see how in certain cases Article 32 is valid and in many it is not. Also a fair reading of Justice Bobde s article tells you a lot how the SC is functioning. I would like to point out that barandbench along with livelawindia makes it easier for never non-lawyers and public to know how arguments are done in court, what evidences are taken as well as give some clue about judicial orders and judgements. Both of these resources are providing an invaluable service and more often than not, free of charge.

Student Suicide and High Cost of Education
For quite sometime now, the cost of education has been shooting up. While I have visited this topic earlier as well, recently a young girl committed suicide because she was unable to pay the fees as well as additional costs due to pandemic. Further investigations show that this is the case with many of the students who are unable to buy laptops. Now while one could think it is limited to one college then it would be wrong. It is almost across all India and this will continue for months and years. People do know that the pandemic is going to last a significant time and it would be a long time before R value becomes zero . Even the promising vaccine from Pfizer need constant refrigeration which is sort of next to impossible in India. It is going to make things very costly.

Last Nail on Indian Media Just today the last nail on India has been put. Thankfully Freedom Gazette India did a much better job so just pasting that

Information and Broadcasting Ministry bringing OTT services as well as news within its ambit.

With this, projects like Scam 1992, The Harshad Mehta Story or Bad Boy Billionaires:India, Test Case, Delhi Crime, Laakhon Mein Ek etc. etc. such kind of series, investigative journalism would be still-births. Many of these web-series also shared tales of woman empowerment while at the same time showed some of the hard choices that women had to contend to live with. Even western media may be censored where it finds the political discourse not to its liking. There had been so many accounts of Mr. Ravish Kumar, the winner of Ramon Magsaysay, how in his shows the electricity was cut in many places. I too have been the victim when the BJP governed in Maharashtra as almost all Puneities experienced it. Light would go for just half or 45 minutes at the exact time. There is another aspect to it. The U.S. elections showed how independent media was able to counter Mr. Trump s various falsehoods and give rise to alternative ideas which lead the team of Bernie Sanders, Joe Biden and Kamala Harris, Biden now being the President-elect while Kamala Harris being the vice-president elect. Although the journey to the white house seems as tough as before. Let s see what happens. Hopefully 2021 will bring in some good news. Update On 27th November 2020 Martin who runs the planet got an e-mail/notice by a Mr. Nikhil Sethi who runs the wikibio.com property. Mr. Sethi asked to remove the link pointing Devangana Kalita from my blog post to his site as he has used the no follow link. On inquiring further, the gentleman stated that it is an Updated mandate (his exact quote) from Google algorithm. To further understand the issue, I went to SERP as they are one of the more known ones on the subject. I also looked it up on Google as well. Found that the gentleman was BSing the whole time. The page basically talks about weightage of a page/site and authoritativeness which is known and yet highly contested ideas. In any case, the point for me was for whatever reason (could be fear, could be something else entirely), Mr. Sethi did not want me to link the content. Hence, I have complied above. I could have dragged it out but I do not wish Mr. Sethi any ill-being or/and further harm unduly and unintentionally caused by me. Hence, have taken down the link.

Like each month, here comes a report about the work of paid contributors to Debian LTS. Individual reports In October, 221.50 work hours have been dispatched among 13 paid contributors. Their reports are available:

• Abhijith PA did 16.0h (out of 14h assigned and 2h from September).
• Adrian Bunk did 7h (out of 20.75h assigned and 5.75h from September), thus carrying over 19.5h to November.
• Ben Hutchings did 11.5h (out of 6.25h assigned and 9.75h from September), thus carrying over 4.5h to November.
• Brian May did 10h (out of 10h assigned).
• Chris Lamb did 18h (out of 18h assigned).
• Emilio Pozuelo Monfort did 20.75h (out of 20.75h assigned).
• Holger Levsen did 7.0h coordinating/managing the LTS team.
• Markus Koschany did 20.75h (out of 20.75h assigned).
• Mike Gabriel gave back the 8h he was assigned. See below
• Ola Lundqvist did 10.5h (out of 8h assigned and 2.5h from September).
• Roberto C. S nchez did 13.5h (out of 20.75h assigned) and gave back 7.25h to the pool.
• Sylvain Beucler did 20.75h (out of 20.75h assigned).
• Thorsten Alteholz did 20.75h (out of 20.75h assigned).
• Utkarsh Gupta did 20.75h (out of 20.75h assigned).

Evolution of the situation October was a regular LTS month with a LTS team meeting done via video chat thus there s no log to be shared. After more than five years of contributing to LTS (and ELTS), Mike Gabriel announced that he founded a new company called Frei(e) Software GmbH and thus would leave us to concentrate on this new endeavor. Best of luck with that, Mike! So, once again, this is a good moment to remind that we are constantly looking for new contributors. Please contact Holger if you are interested! The security tracker currently lists 42 packages with a known CVE and the dla-needed.txt file has 39 packages needing an update. Thanks to our sponsors Sponsors that joined recently are in bold.

• Platinum sponsors:
• TOSHIBA (for 62 months)
• GitHub (for 52 months)
• Civil Infrastructure Platform (CIP) (for 30 months)
• Gold sponsors:
• Blablacar (for 77 months)
• Roche Diagnostics International AG (for 73 months)
• Linode (for 67 months)
• Babiel GmbH (for 56 months)
• Plat Home (for 55 months)
• University of Oxford (for 12 months)
• Silver sponsors:
• The Positive Internet Company (for 78 months)
• Domeneshop AS (for 77 months)
• Nantes M tropole (for 71 months)
• Univention GmbH (for 63 months)
• Universit Jean Monnet de St Etienne (for 63 months)
• Ribbon Communications, Inc. (for 57 months)
• Exonet B.V. (for 46 months)
• Leibniz Rechenzentrum (for 40 months)
• CINECA (for 30 months)
• Minist re de l Europe et des Affaires trang res (for 24 months)
• Cloudways Ltd (for 13 months)
• Dinahosting SL (for 11 months)
• Platform.sh (for 6 months)
• Bauer Xcel Media Deutschland KG (for 5 months)
• Bronze sponsors:
• Seznam.cz, a.s. (for 78 months)
• Evolix (for 77 months)
• Linuxhotel GmbH (for 75 months)
• Intevation GmbH (for 74 months)
• Daevel SARL (for 73 months)
• Bitfolk LTD (for 72 months)
• Megaspace Internet Services GmbH (for 72 months)
• Greenbone Networks GmbH (for 71 months)
• NUMLOG (for 71 months)
• WinGo AG (for 70 months)
• Ecole Centrale de Nantes LHEEA (for 66 months)
• Entr ouvert (for 62 months)
• Adfinis AG (for 59 months)
• Tesorion (for 54 months)
• GNI MEDIA (for 53 months)
• Laboratoire LEGI UMR 5519 / CNRS (for 53 months)
• Bearstech (for 45 months)
• LiHAS (for 45 months)
• People Doc (for 41 months)
• Catalyst IT Ltd (for 39 months)
• Supagro (for 35 months)
• Demarcq SAS (for 33 months)
• Universit Grenoble Alpes (for 19 months)
• TouchWeb SAS (for 11 months)
• SPiN AG (for 8 months)
• CoreFiling (for 4 months)

No comment Liked this article? Click here. My blog is Flattr-enabled.