lyxia @lyxia@mamot.fr
Haskell and Coq programmer
Joined Dec 2019
I just verified that an S-expression parser recognizes only S-expressions.
Implementation: 250 LOC
Spec: 125 LOC
Proof: 700 LOC
Apparently parser combinators in total languages with dependent types is still a widely open research problem. Projects that need parsing just roll their own stuff, and rarely verify it...
To git rebase whenever you pull, add in ~/.gitconfig :
[pull]
rebase = true
Communication is hard. I don't want to sound like an obnoxious smartass when disagreeing with someone at work.
I just realized I have a Windows machine, that I could use to test the portability of stuff. I didn't realize earlier because I spend so much time in a Linux VM...
Un truc que je ne comprends pas sur les trous noirs
@MartinShadok
J'y connais techniquement rien, donc à prendre avec des gros grains de sel. Je crois que les singularités ce sont plutôt des phénomènes qui apparaissent dans les modèles théoriques, qui indiquent qu'on est à des échelles où ces modèles ne sont pas fiables. Bref, quand des équations disent que quelque chose tend vers l'infini, en réalité il y a probablement un mécanisme inconnu qui prend les devants.
coqdoc is packaged as part of Coq, so projects stuck on older versions don't benefit from bugfixes and new features. That's sad. I've been wanting to split it off[1] but actually the whole thing should be redesigned from scratch[2] so it doesn't seem worth it to break things only to break them again shortly after.
[1] https://github.com/coq/coq/issues/10597
[2] A related discussion https://coq.discourse.group/t/would-coq-benefit-from-docstrings/849/3 and an idea floating around is to build something on top of OCaml's odoc.
@lthms
Great! Thanks!
@lthms
That's the third thing I broke with that patch... I should work on some tests around that part...
@lthms
Oh I see. I misunderstood the syntax of begin details, thought it was a standalone tag like the others. Sorry about that.
@lthms
new_lines is called to update the current position for errror reporting, so it might be something else I did...
@freetux@mastodon.tetaneutral.net
Ça se défend aussi 🙂
@freetux@mastodon.tetaneutral.net
Apparement c'est pas possible en CSS https://stackoverflow.com/questions/21367441/make-scroll-bar-take-no-space
Possiblement avec du javascript.
Si le but c'est que du contenu ne saute pas d'une page à l'autre à cause de la barre de défilement, il me semble que le mieux c'est d'utiliser une largeur fixe (peut-être deux ou trois pour s'adapter aux téléphones et tablettes, mais juste pas une page complêtement élastique) et d'accepter un peu d'espace vide. Désolé si ça ne répond pas à ta question.
lyxia
boosted
@jsoo
Not yet!
Just made a new site https://coq.pl-a.net
lyxia
boosted
Proving Algebraic Datatypes are “Algebraic” in #Coq
https://soap.coffee/~lthms/posts/AlgebraicDatatypes.html
It was fun to write, hope you enjoy reading it. I tried to spellcheck it, but tbh I wouldn’t be surprise to find mistakes… If you notice some, feel free to tell me!
woohoo, 4h to the deadline, arguing with coauthors about whether a proof is correct (luckily entirely nonessential either way)...
lyxia
boosted
I’ve finally started to work on my next blogpost: Why algebraic datatypes are “algebraic,” explained.
Inspired by @na and her nice write-up (in French, here https://blog.gelez.xyz/type-produit/)
Proofs are done[§], I need to actually write the explanation now x).
[§]: https://gist.github.com/lthms/8f93f3c4b9527b97997cada2a05b8902
Haskell and Coq programmer
Joined Dec 2019
