Update PVS on Apple silicon build instructions

Author: kai-e

.gitignore

@@ -5,3 +5,4 @@
 *.log
 *.el
 auto
+/.DS_Store

ReadMe.md

@@ -2,13 +2,13 @@
 
 ## Work
 
-As a verification architect I
+As an aspiring verification architect I'd
 - devise roadmaps for building trustworthy systems,
 - re-discover or create verification techniques tailored to these roadmaps,
 - design and implement tool prototypes to aid in executing roadmaps, and
 - foster an engineering culture where trustworthiness of the product is a key ingredient.
 
-This often means I do things somewhat differently. If that is the case and the cost/benefit trade-off looks promising, I help with educating engineers how to do things differently, too.
+This often means I do things somewhat differently. If that is the case and the cost/benefit trade-off looks promising, I help with educating colleagues how to do things differently, too.
 
 
 ### Pubs
@@ -37,6 +37,8 @@ Most recent work is sequestered in [ARM](https://www.arm.com), [QualComm](https:
 
 ### Misc
 
+**News 2026/01/22:** Updated [Build instructions for PVS on ARM Macs](misc/PVS/ARMbuild/).
+
 **News 2023/05/03:** The 2022 iteration of the [ACM Software System Award](https://awards.acm.org/software-system) goes to our team of authors of [seL4: formal verification of an OS kernel](https://doi.org/10.1145/1629575.1629596).
 
 **News 2023/04/03:** [Build instructions for PVS on ARM Macs](misc/PVS/ARMbuild/).

misc/PVS/ARMbuild/ReadMe.md

@@ -1,5 +1,33 @@
 # PVS Build Instructions for ARM-Based Macs
 
+## Season 2
+
+Pulled some PVS updates (8.0) via git and attempted to rebuild. That did not work.
+
+### SBCL trouble
+
+Homebrew `sbcl` is broken (`mmap: Operation not permitted`). I do not know for how long that has been the case and whether it's entirely my own botching of my setup. 
+
+Either way, I sourced `sbcl-2.4.0-arm64-darwin-binary.tar.bz2` from [SBCL on sourceforge](https://sourceforge.net/projects/sbcl/), unpacked it, and installed it locally (with `INSTALL_ROOT=/Users/kaie/local sh install.sh`).
+
+Building the newer SBCL as per the old instructions would still fail because SBCL's `make-config.sh` calls a naked `sbcl` which would still be the broken homebrewed version. I prefixed my `$PATH` with `/Users/kaie/local/bin`. building then succeeded.
+
+Finally, installed the newly built SBCL locally with
+`INSTALL_ROOT=/Users/kaie/opt/sbcl sh install.sh`.
+
+### PVS
+
+Re-building PVS fails as usual with problems in compiling ancient C files. In the meantime both Xcode's and homebrew's llvm updated.
+
+```
+$ pushd~ ~/src/PVS
+$ cd /opt/homebrew/Cellar/llvm
+$ ln -s 21.1.8 17.0.0
+$ popd
+```
+
+The [patch](0001-Fix-C-errors-for-the-SBCL-based-ARM-Mac-build.patch) still appears to both be necessary and work.
+
 ## Preparation
 
 I have Xcode, its command line utilities, [Emacs for Mac OS X](https://emacsformacosx.com/), and [homebrew](https://brew.sh/) installed.