Arnaud Bailly
Arnaud Bailly
Hi Jacek, It is for me, useful when hacking on the elisp side. I must admit I am not very proficient at emacs-lisp so I would hardly be able to...
@stackcats is this still relevant? There has been fixes to columns indices lately that might have fixed this.
@zenntenn I can't reproduce locally using Idris 1.1.1 and Emacs 25.3.
@Abhiroop This seems like an issue within idris itself. idris-mode itself does not know how to typecheck Idris and interacts with a background idris process. But I agree this is...
When I do `:t Main.hole` at the command-line it shows: ``` :t Main.hole k : Nat j : Nat _rewrite_rule : plus k j = plus j k -------------------------------------- Main.hole...
@david-christiansen I tracked this to the `runIdeModeCommand` function called with command `Metavariables` in `REPL.hs` which is pretty daunting. I was unable to understand why the application is not properly reduced....
@dstechenko is this still bugging you?
@XStargate Still relevant?
How about using github actions for that?
Could it be related to this: https://support.apple.com/en-us/HT204899 ? Googling lead me to this issue https://github.com/nteract/nteract/issues/1523 which seems to expose a similar issue. Alternatively, digging into racket docs showed this: https://download.racket-lang.org/docs/5.1/html/foreign/Loading_Foreign_Libraries.html...