laurent.orseau
2021-10-4 16:55:52

Bogdan, next year: “I remade the universe, it runs 10x as fast as the previous one, and now there’s a debugging console to fix things live.”


spdegabrielle
2021-10-4 17:56:39

@popa.bogdanp ^


soegaard2
2021-10-4 18:33:24

@popa.bogdanp Watched the video. This is a great idea and execution.


popa.bogdanp
2021-10-4 18:41:02

Thanks! :smile:


sorawee
2021-10-4 19:09:48

@cperivol it’s “A formal foundation for symbolic evaluation with merging”


jbclements
2021-10-4 19:41:09

I just pushed a commit with a commit message that described only a very small part of the changes that were in that commit. I see that force-pushes are not a thing:


jbclements
2021-10-4 19:41:13

remote: error: GH006: Protected branch update failed for refs/heads/master. remote: error: Cannot force-push to this protected branch To <http://github.com:/racket/htdp\|github.com:/racket/htdp> ! [remote rejected] master -&gt; master (protected branch hook declined) error: failed to push some refs to '<http://github.com:/racket/htdp\|github.com:/racket/htdp>'


jbclements
2021-10-4 19:42:00

… so I’m wondering what the best way to associate information with this commit is. Removing the protection seems like a bad idea. I could make a tiny bogus commit with a message that refers to this one, that’s the best I’ve got at this point.