Erik Martin-Dorel comments

Results 344 comments of


                                            Erik Martin-Dorel

actions/checkout should have a `sudo: true` option that enables the action to work on non-root-user containers with passwordless sudo access

Hi @JasonGross ! Thanks for opening these two issues! I'm in vacation now and away from keyboard this WE so I won't be able to commit much tonight (apart from...

actions/checkout should have a `sudo: true` option that enables the action to work on non-root-user containers with passwordless sudo access

Sorry folks, I realize I replied to @JasonGross's issue while believing that it was posted as an issue in my https://github.com/coq-community/docker-coq repo. Will then copy it there, and hide my...

coq-simple-io.dev : remove dune upper bound

Hi @liyishuai ! thanks for the ping. Sure, this is easy to do. Which version of Dune would be OK?

coq-simple-io.dev : remove dune upper bound

Maybe 3.13.1 ? unless the latest releases 3.15.0 / 3.15.1 would fix the issue you speak about? https://github.com/ocaml/dune/releases

coq-simple-io.dev : remove dune upper bound

Hi @liyishuai, the downgrade is complete, see e.g.: * [https://explore.ggcr.dev/?blob=coqorg/coq@sha256:…&mt=application%2Fvnd.docker.container.image.v1%2Bjson&size=11512&manifest=coqorg/coq:dev@sha256:…](https://explore.ggcr.dev/?blob=coqorg/coq@sha256:efc39f70af390282861ab1a38f94d4faf92b803982b3191dec74af8a15a9a645&mt=application%2Fvnd.docker.container.image.v1%2Bjson&size=11512&manifest=coqorg/coq:dev@sha256:0f92df0e921c1981287cf35f299c29913b6fe7b5956a4613d653ffd4d625a1ea) * (URL generated from https://explore.ggcr.dev/?image=coqorg/coq:dev ) Do you think you could file an issue in Dune's repo if it is...

Updating PG way to communicate with Coq

Thanks @Alizter for your heads-up ! This indeed deserves some dedicated discussion in some upcoming PG telco, Cc @Matafou @hendriktews A few questions/comments: * A migration to coq-lsp looks like...

Updating PG way to communicate with Coq

> I'm not sure how PG interacts with Coq today (I vaguely know it is going through `coqtop`). Exactly. To give a few more details, * PG first does some...

Usage stability

Hi @alphapapa, > Does it work when you only connect one account, or do you still have to go through all those steps? Yes: I'm using org-gcal.el with a single...

Usage stability

> Does this mean what I think it means, that you have to be very careful to not run the fetch command on the wrong Org file? No, `M-x org-gcal-fetch`...

Implement pre-compilation of exercises and graders

> gentle ping, have you been able to make progress on integrating this PR? @gasche sure! as said previously, this PR is a priority! in particular as soon as the...