lthms @lthms@mastodon.social

My better half, genuinely : “Oh right, you’re old, you don’t know that.

My– dealing with dependencies is hard

Hier, j’ai enfin terminé « La crise de la masculinité : autopsie d’un mythe tenace ». Ça m’a pris facilement un an de lecture épisodique… pas parce que le livre est mauvais (au contraire ! il est infiniment intéressant), mais parce que les réalités qu’il décrit se suivent et se ressemblent et laissent un sentiment d’impuissance et de gâchis énorme

https://livre.fnac.com/a12362450/Francis-Dupuis-Deri-La-crise-de-la-masculinite

TIL you can use "type:<input type>" in place of a complicated input name listed by swaymsg -t get_inputs (#sway tips)

Oh, it’s this time of the year when I want to redesign my blog from scratch, because I can and I feel bored with the old one.

I will eventually do it… and I wonder what it will look like then

I should release coqffi.1.0.0~beta4, right?

https://github.com/coq-community/coqffi/blob/main/CHANGES.md#unreleased

Generating 37,444 lines of valid Coq is fun

(okay, so after further investigation, I could have found the issue much sooner if only I haven’t had removed the generated mli file… this one is on me)

I ran into the perfect example of why a tool like coqffi is necessary, and why you should never configure Coq extraction mechanism manually. I lost almost 2h before understanding what the issue was…

And it was that `a * b * c` in OCaml and `a * b * c` in Coq are not equivalent as far as the extraction mechanism is concerns, but everything compile just fine because of the amount of `Obj.magic` that the extraction uses…

That being said, I need to fix coqffi now 😅 (https://github.com/coq-community/coqffi/issues/56)

Week-eeeend