Some apps Will draw their own cursor and there’s nothing you can do about it. However, what’s happening here might be something else, so, are these apps in flatpak?

I’ll give you a fast-forward of the subjects you need to study to actually learn this stuff (with links). Many of these are part of typical computer science curriculums. However, most will exclude at least some of this to its fullest. Note that it’s a lot of knowledge, you might find it frustrating to just deep dive into it on your own, don’t take it the wrong way, maybe follow an actual course and you will be guided into all of this. Maybe I’ll also try to give a run-down, skipping the preupedeitic knowledge… later… if I have time.

P.s.: to get the general feeling you don’t really need to know all of this tho. Just skim it. And dive deeper if you like it.

• Any respectable computer scientist needs to know at least some first order logic https://en.wikipedia.org/wiki/First-order_logic
  • Read the semantics part. You don’t need everything, but you must understand what it means for a Formula to be a logic consequence of a set of formulas
  • Read a bit the deductive systems part. I find “natural deduction” (in detail here https://en.wikipedia.org/wiki/Natural_deduction) easier to understand (more… Natural) however, your mileage may vary, many people find it confusing, hence why “sequent calculus” was invented. We’ll use the sequent calculus later
• You need to know lambda calculus https://en.wikipedia.org/wiki/Lambda_calculus If you know any functional programming language it will be easier, but it’s optional
  • You can learn it on its own, but it fits better as part of a “foundations of computer science” course. I don’t have a link for that.
• You also need to know a bit of programming in basically any strongly-typed language. This will give you some kind of general idea of what types and type systems are.
• Now you can put together what you know of types and sequent calculus, and learn what type derivation rule are https://en.wikipedia.org/wiki/Typing_rule
  • Now you understand the meme
  • You can also check out what type systems are as a whole https://en.wikipedia.org/wiki/Type_system
  • We have skipped Curry-Howard, but you can see how typing rules look a lot like logic deduction rules, in particular sequent calculus
• Hooray, time for Curry-Howard https://en.wikipedia.org/wiki/Curry–Howard_correspondence they basically notice the same similarity you just noted, but take it a step further, they can do it because they know other logics other than first order logic
• The next step, if you are interested, are theorem provers, which are the direct application of the correspondence https://en.wikipedia.org/wiki/Proof_assistant
  • Check out rocq or agda

I was aware of that, but I didn’t want to do a full write-up from zero knowledge to type theory…

Maybe I’ll do it later tho. Because I enjoy explaining this stuff.

Anyway, despite the comedic delivery, that comment should give a 1st year CS student all the keywords they need to research the subject. Especially the letters between Curry and Howard, which are referred to as the “Curry-Howard correspondence”

https://feddit.it/comment/20528152

Oooooohhh! That’s my field of study!

So, you know how in programming you have data types (like int, float, structs etc…) well, they are actually math.

In math, more specifically in logics, there’s these things called “judgement derivation systems”. They are basically sets of rules that tells you if you can derive a judgement, from a set of hypothetical judgement. The most notorious are sequent calculus and natural deduction. Both are used to determine if a logic formula is consequence of a set of hypothesis.

You see, one day Mr Howard wrote to Mr Curry: “I was working on a type system for lambda calculus, and I noticed it kinda look like natural deduction” and curry answered: “wow, that’s cool, I’ll tell you more, a type system for this other thing kinda looks like combinatory logics” and then they both went “could it be that every type system is actually a logic deduction system, and every logic deduction system is actually a type system?” And this is what modern type theory (and theorem provers) are based on.

Now, formal type systems are often defined as judgement systems. More specifically, they look like sequent calculus, and they use a “context” object, which is often identified with the letter gamma.

deleted by creator

☝️You, probably

Two pairs of scissors

There’s a company that sells “reasonably good” replacement pads for most headphone models, and they include links to tweets and posts of people who bought those pads to prove that they fit properly. I don’t remember the name tho

Said the British, living right at the edge of the heat dome

Well, instead of stealing from the drivers, to give to a corporation, it steals from tourists to give to drivers. I say it’s not good but it’s still less bad

Yeah, we are a bureaucracy machine.

People (especially us) often make fun of how convoluted our bureaucracy is, but this has made us extremely good at paper moving. If any country had a go at being us, they would collapse.

Italy. Because you need a license to be a taxi driver, and a random company cannot hand them out (and the taxi drivers union is powerful and corrupt). And because the government gotta know who is renting a room where, you can’t just go wherever you want without anyone knowing, especially foreigners. Whenever you rent a room in Italy, the owner will take a picture of your ID/passport, and send your data to the local government. Also you gotta pay taxes on the rooms you rent.

It doesn’t have to be like this though.

Here, for example, Uber is not allowed and Airbnbs are regulated

Short side because it’s TV facing (in my living room). Edge seat because I like the arm rest. It would be even better If the arm rest was to the right, but my sofa is a reverse L.

I have sad news for you. Not even the sperm is stored in the balls, it’s just produced there. It’s stored in a separate sack inside your body.

Can you install different OSes. Or are you limited to the vendor provided build of osmc?

Don’t use a raspberry pi.

RPI5 only has h265 decoding, everithing else is handled by the cpu. Which is fine for 1080 as long as that’s all the sbc is doing, but if you are also running some server, or you want anything h264 above 1080 you are out of luck.

RPI4 should be a little better, it has h264 and h265, don’t know the supported resolutions/framerates, but the cpu is considerably less powerful. Also, the cpu lacks encryption acceleration, so if your are getting your movies over https that’s gonna take a toll.

Older Pis are goint to be unsupported by kodi and jellyfin, so don’t get those.

None of these is a dead no-go, listen to other peoples experiences. But I personally would advise against any Raspberry Pi. Maybe and Orange Pi is better? I don’t know. My suggestion is to avoid the SBC, and get a cheap second hand Intel pc instead (possibly a very low power one). Intel’s quicksynk video accelerator is gonna run laps around any sbc at any resolution, and it’s gonna support more decoders, and even some encoders if you want to run transcoding in a jellyfin server.

Edit: If intel sold a quicksink pcie card, I would put one in my rpi5. But it don’t.

Edit 2: I should add that some streaming services block 4k on Linux

If it’s a Wayland application it will support global shortcuts.

For X11 apps. If you are on KDE there’s this menu:

Other DEs have different ways to deal with this.

And if you are on Gnome, change DE. Gnome will always follow its own philosophy, because apparently it doesn’t align with yours, you should use something else.

Btw, I gave the same answer in the previous comment.

Also, on the “how can you consider this polished”… Wayland supports global shortcuts, this is a fact. What it doesn’t support is “global shortcuts for apps that use a protocol that is not Wayland”. I think I made my point

https://github.com/X11Libre/xserver/pull/56

Here is the x11libre dev not understanding what the ^ operand does in C. Would you trust running this person’s code as a display server?

Sure. No one expects anyone to know everything from the start, and people improve with time. But this was metux’s understanding of C when he forked off xorg thinking he could do better than freedesktop.