Pinned toot

I rarely use GIFs when writing private messages, but when I do they always picture Merida

Pinned toot
Pinned toot

Hardware? It’s just someone else’s software

A wild “close-enough approach paper” appears

~lthms boosted
~lthms boosted
~lthms boosted

Slow, imperfect progress is better than none at all.

~lthms boosted

We're nearing the end of #RustBeltRust, so it's time for a software release!

utf8-norm, a command line tool to normalize Unicode UTF-8 data, inspired by a phenomenal talk by @j41manning@twitter.com.

git.nora.codes/nora/utf8-norm

I rarely use GIFs when writing private messages, but when I do they always picture Merida

~lthms boosted

This is official, I hate writing double-columns articles.

Deadline day is in two days, and I continue to run into “obvious” error in my framework.

T_T

~lthms boosted

Currently writing the program I have been eager to write for months.

~lthms boosted

RT @Teymour_Ashkan@twitter.com
The look of the White House Italian translator as Trump says President Mozzarella for the Italian President and says U.S. and Italy have been allies since Ancient Rome.

Not surprisingly, I was able to greatly improve the performance of the typeclass instance search just by using typeclass priorities.

Instance my_instance : C|10 := ...

Here, 10 is the priority of the instance (otherwise decided by based on the number of variables the instance needs).

Coq uses instances with a low priority number first, so by setting a high number to instances less likely to succeed, I was able to cut my build time from ~33s to ~8s on my work laptop.

\o/

By the way, I ran into an… interesting problem yesterday and I don’t really know how to deal with it.

I have a typeclass of the form C (f : a -> b) : Prop := { pred : forall (x : a), P (f x) }, and I have a function g : c -> a -> b such that I can prove that forall x, C (g x) -> False, so basically, I would like a way to tell Coq to trust me on this one, and just cut the search and backtrack if it finds itself in a situation where it searches for such goal.

Once upon a time, I didn’t know how to use `Hint` commands. Now, I find myself in a position where I convinced myself I *need* them every now and then.

Ah, ça faisait longtemps que je n’étais pas tombé sur la pub des flexitariens ; me fais toujours rire de savoir que c’est le lobby de la viande derrière cette blague.

~lthms boosted

Genie: You have ONE WISH.

Me: Alright, I have one, but it's very detailed.
Genie: As long as it is only one wish, you're allowed to spend as much time as you want detailing it.

Me: Alright, here we go. *Grabs notebook and takes a deep breath* The key words MUST, MUST NOT, REQUIRED, SHALL, SHALL NOT, SHOULD, SHOULD NOT, RECOMMENDED, MAY, and OPTIONAL are to be interpreted as described in [RFC2119].

Genie: Wait, is that...?

Me: *Flips notebook* Chapter 1. Preamble.

~lthms boosted

As a computer scientist with some self-respect, I just spent 30 minutes to do download 15 files with wget , where I could have spent 3 minutes by clicking on each of them.

Eh folks. What do you think of this greeny editor colorscheme?

Eh Mastodon, tu aimes le dessin, la musique chill et tu t’ennuies ?

twitch.tv/redily_

\o/

Show more
Mastodon

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!