What was your last RTFM adventure? Tinker this, read that, make something smoother! Or explodier.
As for me, I wanted to see how many videos I could run at once. (Answer: 60 frames per second or 60 frames per second?)
With my sights on GPUizing some ethically sourced motion pictures, I RTFW, graphed, and slapped on environment variables and flags like Lego bricks. I got the Intel VAAPI thingamabob to jaunt by (and found that it butterized my mpv videos)
$ pacman -S blahblahblahblahblahtfm
$ mpv --show-profile=fast
Profile fast:
scale=bilinear
dscale=bilinear
dither=no
correct-downscaling=no
linear-downscaling=no
sigmoid-upscaling=no
hdr-compute-peak=no
allow-delayed-peak-detect=yes
$ mpv --hwdec=auto --profile=fast graphwar-god-4KEDIT.mp4
# fucking silk
But there was no pleasure without pain: Mr. Maxwell F. N. 940MX (the N stands for Nvidia) played hooky. So I employed the longest envvars ever
$ NVD_LOG=1 VDPAU_TRACE=2 VDPAU_NVIDIA_DEBUG=3 NVD_BACKEND=direct NVD_GPU=nvidia LIBVA_DRIVER_NAME=nvidia VDPAU_DRIVER=nvidia prime-run vdpauinfo
GPU at BusId 0x1 doesn't have a supported video decoder
Error creating VDPAU device: 1
# stfu
to try translating Nvidia VDPAU to VAAPI – of course, here I realized I rtfmed backwards and should’ve tried to use just VDPAU instead. So I did.
Juice was still not acquired.
Finally, after a voracious DuckDuckGoing (quacking?), I was then blessed with the freeing knowledge that even though post-Kepler is supposed to support H264, Nvidia is full of lies…
______
< fudj >
------
\ ‘^----^‘
\ (◕(‘人‘)◕)
( 8 ) ô
( 8 )_______( )
( 8 8 )
(_________________)
|| ||
(|| (||
and then right before posting this, gut feeling: I can’t read.
$ lspci | grep -i nvidia
... NVIDIA Corporation GM108M [GeForce 940MX] (rev a2)
# ArchWiki says that GM108 isn't supported.
# Facepalm
SO. What was your last RTFM adventure?
I’m very intrigued. Could you please explain it? Even if you abandoned it, you still learned valuable knowledge.
Yes, that’s true and a better way to look at it, thanks!
Well, I was amazed by proof systems like Coq or Isabelle, that let one formally verify the correctness of their code. I learnt Coq and coded a few toy projects with it, but doing so felt pretty cumbersome. I looked at other options but none of them had a really good workflow.
So, I attempted to design one from scratch. I tried to understand Coq’s mathematical foundation and reimplement it into a simpler language with more familiar syntax and a native compiler frontend. But I rushed through it and turns out I had barely scratched the surface of the theory. Not just regarding the proof system, but also with language design in general.
I did learn a lot though. Since then I’ve been reading more about proof systems and language design in my spare time, and I’ve collected quite the stack of notes and drafts. Recently I’ve begun coding a way more polished version of that project, so on to round two I guess!
Round two, hell yeah.
The aesthetica of a stack of notes, born from a “dead end”, is secretly an odd motivator. You look back and see
and then beyond you, the effort lays itself out in a pretty trusswork.
_or_maybe_i_just_think_well-used_notebooks_are_pretty
Haha yeah, absolutely! Might be too messy to consider it “well used” though… But it does motivate me, seeing all the signs I put there and imagining one day I will conquer that mountain. Maybe not even on the second attempt, but definitely one day.