Valentin Robert

Hi Clément. Sadly, I believe I had pretty much taken the unpleasant approach of re-implementing the pretty-printing myself for dealing with notations, and I don't remember having a good story...

I don't quite understand it either. There seem to be many flags: https://github.com/coq/coq/blob/trunk/toplevel/coqtop.ml#L493 `-async-proofs on` seems like the first step.

Seems like this would work for me, I would be able to link the CoqExn back to the sentence that failed and perform the proper error highlighting. Why the synchronous...

Anyway, at the moment I have to send my `StmAdd` synchronously either way (because my HTTP server runs its handlers in parallel and the writes to sertop are not done...

A bit unrelated: Is there a name for the decimal-encoded bytes that Coq seems to use? i.e. how do I go from "\206\179" to "γ" in JavaScript? :-)

@cpitclaudel yeah I realized it was UTF-8, but can't seem to lookup for UTF-8 decoding libraries that don't assume the `\uCEB3` encoding over this decimal encoding... @ejgallego For instance: `(Control...

Yeah, I don't think you need to change anything about this. I just need to find a way to convert it back on my end... Sorry for this derailing of...

Well, at least I don't feel alone, as I am also experiencing the `expectJust getLinkDeps` on some Template Haskell code! :-(

Happened to me today on a quite large but not huge project (64 modules): https://github.com/GaloisInc/what4 (though some modules are fairly huge, e.g. https://github.com/GaloisInc/what4/blob/master/what4/src/What4/Expr/Builder.hs ) It also happened in this issue...

I agree with this issue. In fact I would even go a little further and suggest that the keys be removed. I'm not sure what they provide to the user,...