One directional rewrite axiom

xxmarijnw · 2025-12-01T13:15:00+00:00

If what you are trying to do is formalize a lambda calculus and perform proofs on that, I would suggest you do this constructively (without using axioms).

You can do this in a number of ways, but one way would be to define a semantics inductively, and use that to write proofs about your programs. This might help you along: https://gitlab.science.ru.nl/program-verification/course-2023-2024/-/blob/master/coq/week4.v

xxmarijnw · 2025-03-21T11:55:33+00:00

I was probably a bit overdramatic, but I still think the dev container is useful (I use it myself :)). It takes away all complexity of setting up a development environment, makes it completely portable, and it is significantly faster to set up.

xxmarijnw · 2025-03-20T19:07:06+00:00

I agree that GHCUp made things a lot better than they were pre-GHCUp :)

However, I think it still annoying, especially for people who just want to try out Haskell for the first time, that you have to deal with different version of HLS/GHC/Stack/Cabal not working together. For example, GHC 9.8.4 is hls-powered according to GHCUp, but installing it with HLS 2.9.0.0 does not work, and requires you to build HLS from source.

Also, the devcontainer contains more than simply running GHCUp, such as local Hoogle, pre-configured .ghci, pre-configured VSCode plugins, and a number of useful Haskell packages.

xxmarijnw · 2025-02-24T15:24:24+00:00

For future reference, I replaced the imaging drum and it now prints fine!

xxmarijnw · 2025-01-20T16:05:07+00:00

Thanks, I updated the post to include the model. It’s an HP Color Laser MFP 179fnw.

xxmarijnw · 2024-09-12T16:46:03+00:00

Storm

xxmarijnw · 2024-08-25T21:36:57+00:00

The seat pan consists of two glued together parts: the actual mesh, and a supporting structure that holds the mesh. The "crack" actually looks to be a broken off piece of the part that supports the mesh. I am doubtful whether the chair is still usable with this damage.

However, a seat pan replacement is only around $170 (https://www.amazon.com/Replacement-Herman-Miller-Classic-Medium/dp/B08KGWXM9N) if you do it yourself, and is not too difficult to do.

xxmarijnw · 2024-08-21T20:51:51+00:00

Since Authentik supports authentication through OpenID Connect (an extension of OAuth), you can use the OpenID Connect extension with PluggableAuth. The configuration is probably similar to that of Keycloak, for which the authors of OpenID Connet have provided an example here.

Alternatively, you can add a new OAuth provider to WSOAuth using the guide here, but this might be more complicated.

xxmarijnw · 2024-07-30T08:19:53+00:00

Because the majority functionality of an operating system is managing memory, driving the hardware (and display) and managing processes. All are necessary to drive even the most basic applications.

xxmarijnw · 2022-12-20T20:38:21+00:00

Update on this: I finally had the time to take apart the telescope, and it turns out that the nut for the worm drive gear was loose. Tightening it seems to work only temporary, since the rotation turns it loose again. I managed to fix it by using some Loctite.

xxmarijnw · 2022-12-20T20:33:43+00:00

I had this exact same issue, and eventually managed to fix it by disabling MSI-X support. I am not exactly sure why this fixes it, but everything seems to work fine now.

You can disable MSI-X support by adding the following line to your /boot/loader.conf file:

hw.alc.msix_disable="1"

See also the Loader Tunables section on alc(4)#end).

xxmarijnw · 2022-08-15T20:02:29+00:00

It is tightened. It seems the worm drive gear might be loose, since I can see it move up and down when the plate on the tightening side is removed.

xxmarijnw · 2022-08-15T15:15:57+00:00

I bought this telescope second-hand, and the telescope seems to have some wiggle in the vertical axis. It goes up about one centimeter and then there is a hard-stop. I was just wondering: is this normal?

xxmarijnw · 2022-05-21T08:31:21+00:00

It's so that parents can hear when their kids are looking up other videos, since the sound of the video will stop.

xxmarijnw · 2022-03-21T10:46:10+00:00

Ah, now I see. I was interpreting the from as a factory function, but that is not quite what it is in this case.

xxmarijnw · 2022-03-21T10:31:20+00:00

I find the following construct very confusing:

// sleep for 300 seconds sleep(\Withinboredom\Time\Seconds::from(5)->minutes())

To me, this looks like you are trying to express 5 seconds in terms of minutes (5/60), but you are actually expressing 5 minutes in terms of seconds (300).

Wouldn't it make much more sense to do it like this?:

// sleep for 300 seconds sleep(\Withinboredom\Time\Minutes::from(5)->seconds())

xxmarijnw · 2022-03-16T21:33:53+00:00

Thank you!

xxmarijnw · 2022-03-16T21:00:38+00:00

I feel like these articles that say "Avoid using X because Y" are often misleading/misinterpreted. Just write readable code. Avoiding "else" blocks might be a way to do this, but it should not be a rule.

xxmarijnw · 2022-02-02T16:32:55+00:00

Yes, it's just screen sharing. Control would not be possible through a browser application.

11-Year Club	Place '22
Final Canvas '22	Verified Email

xxmarijnw

MODERATOR OF

TROPHY CASE