The Unclear Impact

@tuxedocomputers one more silly question about the firmware: if I get the ibp 14 gen8 without an nvidia GPU, will it still boot with secure boot enabled if i load my custom PK and KEK?

i understand that you don’t distribute kernel images signed by microsoft for your own distro (https://www.tuxedocomputers.com/en/TUXEDO-OS_1.tuxedo – “Secure Boot must be disabled in your computer’s UEFI firmware”), but i’m planning to sign my own kernel images anyway and get rid of the microsoft PK/KEK entirely

this works nicely on my ibp 14 v4 (apparently it doesn’t have anything onboard that needs a microsoft KEK to initialize properly with uefi), but that’s a clevo motherboard, not a uniwill one. does the ibp 14 gen8 firmware has anything signed with microsoft’s keys that would break if i removed the keys?

@juliank the tricky thing is what would happen if you backtrack and the clauses that were in conflict get removed (if you remove versions of packages you decide not necessarily to install on backtracking).

in this case the conflict cause would become useful once you decide to install the same package at some other branch of the search when the variables and clauses get added back again. until then, some variables would be “dangling” (appear in the lemma, but not in the problem proper)

but i guess this is not actually a problem if variables can be uniquely identified (so it is apparent when they are re-added to the problem) and you never branch on “dangling” variables

SAT solvers are weird, man

@juliank ah, materializing further clauses sound reasonable, especially if solutions have a fairly regular structure. i guess your alternative would be to pull in clauses for all transitive dependencies, which sounds a lot more painful

a tricky thing is how to represent useful lemmas (CDCL-style) when some variables from the learned clause might not even be in the original problem (pulled in by a transitive dependency in your case).

the very least, i’m having a lot of trouble with that on the first-order model generator that we’re working on (i can’t even pull in all clauses eagerly in the beginning, because i don’t know the model size in advance and a FOL quantifier could match any model element)

2**32 levels of backtracking.

holy (super) cow! is that a state space of 2**(2**32)?

@juliank A->B|...|Z looks suspiciously like a dual-Horn clause !A | B | ... | Z (although I don’t know what to make of A->!B, other than just !A | !B). but it’s defnitely no accident that your algorithm is pretty much DPLL, given that your input is already basically in CNF

maybe this is a good time for CDCL?

@tuxedocomputers

btw (commenting here because i’m not logging into my reddit account any time soon after the API debacle), it seems like the issue you linked in https://old.reddit.com/r/tuxedocomputers/comments/14noz4v/infinity_book_pro_14_gen8_cannot_find_disable/jqqd2nv/ is not publicly accessible. i assume this should land in the next firmware update anyways?

mopidy lets me queue #bandcamp song previews with mopidy-bandcamp, but is currently nearly broken with #ncpmcpp for my use-cases (like the tag editor)

i resolved this conundrum for now by https://linx.marussy.com/bandcamp-queue.py (using bandcamp-dl and python-mpd2)

this doesn’t support adding V0 streams for songs i bought, but i don’t really need that. all songs i bought are downloaded in flac anyways. however, listening to 128k previews before i buy stuff bandcamp friday come is comfy

#mpd or #mopidy

second student so far in the exam i’m correcting who claims that graph isomorphism is NP-complete

either they know something i don’t or they prepared for the exam… poorly

not sure if i’m doing #pleroma -> #lemmy federation right

@ShittyKopper arch linux with sandboxed systemd units for most purposes. I should really set up podman to be rootless, but for now I can still enjoy running containers as systemd services, albeit unsandboxed on the systemd level

@tuxedocomputers @tylerwolf is this still on the radar?

Is there any chance of an IBP 14 gen8 with an ANSI keyboard, or is this the final nudge for me to get into Colemak Mod-DH?

yt-dlp -x -f bestaudio -o "%(playlist_index)02d. %(title)s.%(ext)s" 

is so comfy

realizing I need Emacs for playing around with Agda, I spent a good chunk of today declaring Emacs bankruptcy and setting up a new init.el

I have a much more lightweight but functional Emacs config now

I still don’t know Agda