Valentin Robert

Is it a goal that should be solved immediately? What happens under other Coq IDEs?

I see. In general it is indeed a bad idea to call `firstorder` without a timeout (or actually, all tactics). I'll try to look into implementing a timeout safety, I...

This seems to be the cause of the problem: https://github.com/haskell/haskell-mode/blob/80225e09bf06ab3962b24812f014f948218e0c80/haskell-align-imports.el#L105

I encountered the same problem, and thought I could solve it by just: ``` pip install -r ${./requirements.txt} ``` so as to have the `requirements.txt` path be resolved w.r.t. where...

Actually, it works with an empty requirements file. What fails is when the derivation attempts to do impure things, like `git clone`-ing a repository, or reaching out to the Python...

This would be much appreciated! In the meantime, is there any information on where to look, even manually, to know either what is being watched, or what is currently on...

Maybe the example in this issue makes this look too benign, but this bug makes Emacs w/ Haskell LSP completely unusable on projects that use Unicode. For instance with this...

I could be bothered enough to attempt a fix over the weekend, though I'm not quite sure where to begin. Do you think the solution would look more or less...

Almost immediately running into an odd situation. Consider: https://github.com/haskell/haskell-language-server/blob/9565d0b2d0b7d2ddf5a982269c103b6fd0a781a0/ghcide/src/Development/IDE/GHC/Error.hs#L89-L91 My gut feeling is this is the place that is ripe for column confusion: supposedly, the `srcLocCol` is 1-based and code...

Having a quick look at the Lean breakage, it's breaking because the inductive definition of `instruction` in `Defs.lean` is missing a `BEq` derivation clause, which is now necessary since `ExecuteAs`...