could someone revert https://github.com/coq/coq/pull/19174 once light CI is done?

I merged https://github.com/coq/coq/pull/19114 but should have rerun CI to get coq_lsp to run, now it's broken

@Gaëtan Gilbert I can also push the overlay to coq_lsp?

shouldn't that be easier?

https://github.com/ejgallego/coq-lsp/pull/765

does that work? I wasn't sure if deriving works on functions

TBH I merged a bit quickly and now I'm not even sure if we want to implement the printing that way

CI on your overlay passed, are you merging?

Sure

Gaëtan Gilbert said:

does that work? I wasn't sure if deriving works on functions

In that case it is just for errors, so it is not really used, it will indeed produce a problem, but the contract for this kind of stuff in serlib tells users you cannot expect the seralization to always suceed.

Indeed maybe we want to do the printing differently, but for now the CI is fixed I hope.

Thanks.

I don't understand what this PR is trying to hack around.

(the original one I mean, not the revert)

the main problem is that we're letting UGraph internal exceptions reach toplevel, otherwise this should be wrapped in the proper exception that has access to the current evarmap

I'm also not extremely confident about the runtime cost of having to allocate a big tuple

(in particular, the reworking of the conversion internals to use a result type should help tracking this kind of mess)

Last updated: Oct 13 2024 at 01:02 UTC