I replaced my 1080 Ti recently too (early 2025). I had kept it as my daily GPU since 2017. It was still viable and not in urgent need of a replacement, even though my 1080 Ti is an AIO liquid cooled model from EVGA, so I'm surprised it hasn't leaked yet. It's been put through a lot of stress from overclocking too, and now it lives on inside a homelab server.
The 5090 I replaced it with has not been entirely worth it. Expensive GPUs for gaming have had more diminishing returns on improving the gaming experience than ever before, at least in my lifetime.
Termux can access the full file system if you have root access, which is how I play around with it; however, running a VM is a safer and easier route, especially as smartphone manufacturers are making it tougher to root the device you own.
SPARK is practically just a restricted version of Ada with a few added features for formal verification. You can write a program primarily in SPARK but disable said restrictions based on circumstance by setting the `SPARK_Mode` pragma/aspect to `off` on a package, procedure, function, etc. Mixing Ada and SPARK is trivial.
I guess it is similar to Rust code that uses `unsafe {}` as the other poster mentioned (maybe `unsafe fn` for a closer analogy). My knowledge of Ada/SPARK is much greater than what I know about Rust, so I might be guessing wrong.
So in Rust an unsafe block and an unsafe function mean two different things. An unsafe block allows you to do things that are unsafe, such as dereference raw pointers, access union fields, calling unsafe functions, etc.
Unsafe functions mark that the caller is responsible for upholding the invariants necessary to avoid UB. In the 2021 and earlier editions, they also implicitly created an unsafe block in the body, but don't in 2024.
Or, in a more pithy tone: an unsafe block is the "hold my beer" block, while an unsafe function is a "put down your beer" function.
You don't have to use AdaCore's GNAT Studio. You can quickly get going with Ada/SPARK using Visual Studio Code, as there is an LSP extension for it published by AdaCore themselves.
I'd suggest `-Oz` instead, as it optimises for size above all else at the cost of performance, unlike `-Os` which is less aggressive (but likely produces similar code anyway). `-Oz` is somewhat new if I remember correctly, so it depends on the GCC version.
You can use the T420/T520's keyboard in a T430/T530 with modifications to the firmware, some plastic around the keyboard part itself, and the ribbon cable (just pin isolation with tape). It lets you go with Ivy Bridge over Sandy Bridge.
I have a T430 with the T420's keyboard and it lasted me 7 years of daily use before battery life became too big of an issue for me (even with a single DDR3L RAM module and a slice battery), so I put it aside. The typing experience was really excellent.
Upgrading the CPU to a quad-core model (ideally one that consumes 35W over 45W) is one of the best upgrades to make for anyone still using these machines.
Do you know an exceedingly credible source for the firmware modifications?
(Last time I looked, it had the air of the XDA-style culture: "To root your phone, download this package from a `.ru` piracy site, run the `.exe` on your PC, then install and run the closed blobs on your phone, including rooting and replacing your bootloader with one, we know you will trust us." Though, in their defense, if they were organized crime, they would probably make an effort to look more legitimate, rather than gratuitously suspicious. And all the forum comments were always lapping it up, appearing to be doing reckless things, while removing much of the demand and contributors for more-credible efforts.)
That is the general nature of reverse engineering efforts, but this one has been documented enough that you don't need to blindly trust completely random executables or code from strange places.
You can manually recreate the process of building a patch for the embedded controller instead of just following instructions: https://github.com/hamishcoleman/thinkpad-ec. Here's the presentation by the author himself at linux.conf.au (what used to be the biggest local Linux conference for those of us in Australia and NZ): https://www.youtube.com/watch?v=Fzmm87oVQ6c. This is of course not supported by Lenovo.
Unlocking the BIOS is definitely more like what you described. It's the price to pay for freely playing around with processor power limits, getting AES-NI instruction set support, etc. I have not checked since 2019, so there might be a clearer way.
Any idea if you can get a quad core into the T420 itself ? I have a dual core i5 that is still doing decently (probably because they still sold i5 CPUs with hyper threading back then) but a quad core 35w CPU with HT would be a great pair with the dedicated Nvidia graphics.
There's also the W520, which looks like a T520, but is set up for a larger PSU, and had quad-core and better GPUs as factory options. (I own a few each of T520 and W520, but don't like the huge power bricks of the W. So I'm using the T as daily driver, until I really need something in the W.)
Would it be any less safe than a Molex connector? They sometimes still come with brand new PSUs for compatibility. They have 12 volt pins too (yellow wire) if I remember correctly that can be very loose. Back when they were more standard, I'd seen sparks go off after they touched a case's chassis, as a cable to the PSU could have multiple unused/unplugged Molex connectors on it just hanging somewhere. The older PSUs I've used never came with full covers for them, so wrapping them in electrical tape was the "fix".
I think one of the reasons why someone might think it's hard to write code in Ada is its Pascal-style syntax and verbosity, which might give the false impression that it's an "outdated legacy language". I've written a few hobbyist projects in Ada (SPARK to be specific) during my spare time and now I greatly enjoy the language, but my very first impression of it wasn't enthusiastic (coming from a C background). I don't fully understand why Ada lacks popularity compared to Rust, outside of Rust having a more vibrant community.
Nim (https://nim-lang.org also mentioned elsethread) was largely inspired by trying to make a more concise Ada with Python-like lexical sensibilities/ergonomics and support for first class meta-programming. Compilers for Nim are sadly not as mature as things like say the gnat Ada compiler.
Not that it matters, but isn't that technically ANSI C(89)? If I remember correctly, the first ISO C standard is instead C90, which is basically identical to C89.
There are also 1 GiB pages in long mode, but support depends on the processor and CPUID's output. Almost all modern x86 processors in the last several years should have it, I think.
Some also technically support it, but it doesn't gain you a whole lot as the TLB will split it down to a 2MB TLB entry. Could save a bit of L2 for the page table entries under the right conditions, but you've already lost if invoking your page walk hardware is in your fast path to begin with.
The 5090 I replaced it with has not been entirely worth it. Expensive GPUs for gaming have had more diminishing returns on improving the gaming experience than ever before, at least in my lifetime.