unexpectedtrap
Joined 3 years ago
Karma
54
Submissions
22
Member since
Jul 19
Recent submissions
Comment · 1 month ago
Ironically enough, the UNIX fathers themselves realized that the hidden files idea was terrible and in the 90s kicked them off completely out of Plan 9 and moved user configs to the $home/lib. And yet we still have our home directories being insanely cluttered with dot files.
Comment · 1 month ago
That’s just the aberration, no? I.e., you can simply smash A and observe some rotation. Since there are no non-collinear accelerations in this case, it’s certainly not the required effect (which is called Wigner rotation).
In the sources I see that the acceleration is applied simply by utilizing a velocity‐addition formula (see https://github.com/dbrant/relativity/blob/fcc20fb18381959ac2...), so no Wigner rotation appears. I guess all the fancy stuff related to how time passes in an accelerating frame (like https://en.wikipedia.org/wiki/Twin_paradox#Difference_in_ela...) is also wrong in this simulation because of that.
You can however observe a mathematically equivalent effect in hyperbolic games, e.g., in Hyperbolica. Hyperbolica even has a quest about rotating a chest by moving it along the axes. On the hyperbolic plane it’s of course not about acceleration but about a winding number you’re doing around some point, but it’s still fun.
Comment · 2 months ago
Plan 9 is essentially exactly that, which clearly was inspired by the Oberon’s GUI. By the way, does then Emacs count as such? Or maybe you should take a look at Genera, however, I’ve never really tried it.
Also the original Metro design as in WP 7/8/8.1 or Windows 8/8.1 relied heavily on the pure text, and the only place populated with a lot of icons was that iconic tiled start screen, although this is probably not what you mean.
Comment · 3 months ago
Using LLMs to generate piles of code and/or proofs of dubious quality is very questionable thing, and I understand these non-stop debates about it.
But in this case, as using plain brute force is already quite a common thing in searching for counterexamples, using LLMs as a sort of more advanced brute force seems to be just the right thing to do, so I struggle to understand so much hostility to this approach.
Comment · 6 months ago
>I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it?
The reason is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important.
>Requiring explicit proofs for every subtraction was presumably seen as too onerous.
Lean can deduce proofs implicitly as well. It’s just not a very reliable mechanism. That is, imagine your code breaking after an update, because Lean suddenly can’t deduce `a ≥ b` automatically for you anymore.
>Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".
What is a standard subtraction over natural numbers at all? As you know, under a standard addition natural numbers form a monoid but not a group.
Comment · 6 months ago
>It definitely is a bad convention because it's highly surprising.
You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising about choosing zero as a default value here? Do you expect it to panic or what?
Comment · 6 months ago
No, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel, this part of a codebase has hardly changed since Lean 3). Almost all the space in the package (more than 2.5 GiB) is taken up by .olean/.ilean/.ir files, approximately 1 GiB of which is generated from the code of Lean’s frontend itself (i.e., parser, elaborator, core tactics, and so on) and the other 1 GiB from a standard library. As you might guess, these files are IR and essentially a compiled Lean’s environment (something like a Lisp image), so that Lean can load them straight up without recompiling and rechecking everything.
There were some proposals like compressing all the .olean files, but (as far as I know) none of them were implemented. Well, even if some proposals were implemented, their contribution was effectively negated anyway.
Comment · 6 months ago
Who said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that this proof will most likely be an implicit argument, that would be a really annoying thing to use.
On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:
def x := #[1, 2, 3, 4]
#check x[7]
Comment · 6 months ago
Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
Comment · 8 months ago
Glad to see Rust project under AGPL-3.0. I wish to see more Rust projects under (A)GPL, because (A)GPL is rare in the Rust community for some reason.
Comment · 8 months ago
So instead of using programming languages designed specifically to effectively express algorithms and data structures, we are going to use natural language like English that is clearly not expressive enough for this? It’s like rewriting a paper about sheaf cohomology in plain English without any mathematical notation and expecting it to be accessible to everyone.
Comment · 9 months ago
I saw this DSL on HN yesterday, and this syntax is total garbage. It’s some stupid mixture of different PLs. Are you seriously OK with this so that you keep posting it here? I don’t even want to look through source code knowing what garbage it is at the surface level.
Comment · 9 months ago
It’s funny to see that even nowadays just a few people understand Windows 8’s UI, while the majority in these comments just blindly shits at it. Not surprising, though, since there are so many happy users of crap UI’s like KDE around.
Sadly, this clone looks very‐very bad, just like millions of WP8‐like launchers compared to the actual WP8.
Comment · 11 months ago
They now provide at least somehow working x86_64 images. It’s of course funny for a project started in the 90s to get x86_64 support only in the 2020s, but it’s still progress in relative terms.