idris-hackers / idris-mode Goto Github PK

Would just be nice if the metavariable names were links to start the prover.

On GNU Emacs 24.2.1 (x86_64-pc-linux-gnu, GTK+ Version 3.6.4):

Done (Total of 16 files compiled, 1 failed, 1 skipped)

Compiling file /home/hars/.emacs.d/elpa/idris-mode-20140130.2349/idris-warnings-tree.el at Tue Feb  4 17:19:48 2014
idris-warnings-tree.el:134:1:Warning: Unused lexical variable `conc-name'

In with-struct:
idris-warnings-tree.el:134:64:Warning: `(reader (slot) (intern (concat
    (symbol-name conc-name) (symbol-name slot))))' is a malformed function
idris-warnings-tree.el:196:1:Error: Invalid function: (reader (slot) (intern (concat (symbol-name conc-name) (symbol-name slot))))
```

:exec in idris-mode should cause Idris to generate a binary, and pass its path back to Emacs. Then, the resulting binary can be run in a comint buffer, to support user interaction in a straightforward manner.

I might be missing something obvious, but how do I save a proof?

> :addproof
Error: command not recognized or not supported.

I can get an "Idris-REPL" buffer from M-x idris-repl or from C-c C-l in an Idris buffer, but the repl buffer is inert and doesn't actually run any of the lines I send to it. Here are the contents of idris-events after C-c C-l:

1387047754.348 -> ((:load-file "/home/alyssa/idris-toys/ElemSearch.idr")
 3)
1387047754.445 <- (:set-prompt "*/home/alyssa/idris-toys/ElemSearch 3)
1387047754.467 <- (:return
 (:ok "loaded /home/alyssa/idris-toys/ElemSearch.idr")
 3)

New events don't seem to appear in response to input in the repl buffer, and C-c C-l doesn't catch blatant type errors like

which : a -> a
which = S 'b'

so I'm assuming it's just not running idris at all.

When I load an Idris file with C-c C-l, and then try to open the Idris Emacs menu before loading has completed, I get the ol’ beach ball (this is on OS X), and it continues to beachball even after Idris has apparently finished (looking at its CPU usage).

If I uncomment out (require 'idris-mode) in my ~/.emacs, and then open a .idr file in emacs, I get

Warning (initialization): An error occurred while loading `/afs/csail.mit.edu/u/j/jgross/.emacs':

Symbol's function definition is void: defvar-local

To ensure normal operation, you should investigate and remove the
cause of the error in your initialization file.  Start Emacs with
the `--debug-init' option to view a complete error backtrace.

When I turn on --debug-init, I get

Debugger entered--Lisp error: (void-function defvar-local)
  (defvar-local idris-warnings (quote nil) "All warnings in the current buffer")
  eval-buffer(#<buffer  *load*<4>> nil "/afs/csail.mit.edu/u/j/jgross/idris-mode/idris-warnings.el" nil t)  ; Reading at buffer position 13$
  load-with-code-conversion("/afs/csail.mit.edu/u/j/jgross/idris-mode/idris-warnings.el" "/afs/csail.mit.edu/u/j/jgross/idris-mode/idris-wa$
  require(idris-warnings)
  eval-buffer(#<buffer  *load*<3>> nil "/afs/csail.mit.edu/u/j/jgross/idris-mode/inferior-idris.el" nil t)  ; Reading at buffer position 11$
  load-with-code-conversion("/afs/csail.mit.edu/u/j/jgross/idris-mode/inferior-idris.el" "/afs/csail.mit.edu/u/j/jgross/idris-mode/inferior$
  require(inferior-idris)
  eval-buffer(#<buffer  *load*<2>> nil "/afs/csail.mit.edu/u/j/jgross/idris-mode/idris-mode.el" nil t)  ; Reading at buffer position 198
  load-with-code-conversion("/afs/csail.mit.edu/u/j/jgross/idris-mode/idris-mode.el" "/afs/csail.mit.edu/u/j/jgross/idris-mode/idris-mode.e$
  require(idris-mode)
  eval-buffer(#<buffer  *load*> nil "/afs/csail.mit.edu/u/j/jgross/.emacs" nil t)  ; Reading at buffer position 130
  load-with-code-conversion("/afs/csail.mit.edu/u/j/jgross/.emacs" "/afs/csail.mit.edu/u/j/jgross/.emacs" t t)
  load("~/.emacs" t t)
  #[0 "^H\205\262^@     \306=\203^Q^@\307^H\310Q\202;^@ \311=\204^^^@\307^H\312Q\202;^@\313\307\314\315#\203*^@\316\202;^@\313\307\314\317#$
  command-line()
  normal-top-level()

In Version 20140106.1002 of Idris mode does not highlight case arrows => properly.

This is due to the complicated nature of building a regexp for operators, and including user defined operators.

Taking a leaf from Haskell Mode, a hacky-ish fix could be defining an explicit list of reserved operators---see https://github.com/haskell/haskell-mode/blob/master/haskell-font-lock.el#L272-L278. Then dealing with user defined operators in another way.

Is there a reason these are set to somewhat brutish foreground colors (e.g. green, red, blue) instead of inheriting from font-lock faces or something similar? This makes the output in the REPL pretty hard to read depending on the background color.

We should have some kind of prover support above what we have today, even if it just wraps the current REPL-style. Better would be a ProofGeneral-style setup.

Tried loading the simplest "Hello world" from Idris tutorial. The command ":x main" gave me the cryptic "error in process filter: Assertion failed: (plusp length)".

This is probably because string literals are handled by the built-in font-lock stuff but comments aren't. I'm going to switch to something more along those lines; alas, documentation and examples along those lines are spotty.

I looks to me like the REPL does a whole lot of work to implement its completion support. In particular, there are functions to manually control the completions buffer, and these aren't even correct: clicking on a completion inserts the entire thing rather than just the portion that should be added, leading to duplicate characters.

The implementation for Idris source buffers [1] works better and is significantly shorter, but I wonder if there's a reason why that technique can't be used in the REPL. Any feedback from those who know better? (ie @hannesm)

[1]

I think this is related to PR #119 – when I see a link for /full/path/to/idris-crypto/src/Data/Crypto/Encryption/ARC4.idr line 32 col 17:, clicking on it opens a buffer that points at (the nonexistent) /full/path/to/idris-crypto/src/full/path/to/idris-crypto/src/Data/Crypto/Encryption/ARC4.idr – duplicating everything up to the directory the .ipkg file is in.

Currently comments are not highlighted properly. This is just a note that it needs fixing.

This causes the type checker to loop forever:

module Death
import Providers
%language TypeProviders


%assert_total
forever : IO (Provider Bool)
forever = forever

%provide (crap : Bool) with forever

Without looking at top, we can't really see that Idris never finished type checking.

Module headers seem to be looking for a "where", reflecting the Haskell roots of the indentation code. So pressing Enter doesn't move the cursor to the left.

Perhaps of interest to @trillioneyes :0)

I now get

user error (Can't find import /Data/Crypto/Util.idr)

when I try to load from an idris buffer. It seems to be treating the path from the ipkg as absolute, rather than relative. Maybe related to the fix for #125?

Reaching for a mouse in emacs of all the editors is pretty silly. It'd be great if there was a way to view type errors and such without the mouse.

I think showing the errors in REPL (like GHCi does) or at least a key when hovering over a type error to show it would be great.

Is there a reason why idris-mode derives from fundamental-mode, not prog-mode? I would expect my global programming mode customisations to apply to idris too.

Appreciate the work all. :)

Some keymap definitions (at least idris-indentation-mode-map and idris-repl-mode-map) contain bindings that don't take effect. As far as I can tell, this is because of the form of the key specifier. Bindings defined like:

(define-key map [?\C-a] 'idris-repl-begin-of-prompt)

or

(define-key keymap [?\r] 'idris-newline-and-indent)

work for me, but bindings defined like

(define-key keymap [backspace] 'idris-indentation-delete-backward-char)

or

(define-key map [return] 'idris-repl-return)

do not seem to take effect, at least in the way you'd expect them to.
This is also the solution to #28: idris-repl-mode-map contains an entry ([return] . idris-repl-return), but this entry is not a valid binding of the enter/return key.

For example, point on ?foo_bar-2 should return ?foo_bar

Right now, it's hard to see if the communication to the compiler has finished.

This can be implemented in two ways:

1. When starting communication, set a status var, and when the continuation is popped, set it otherwise
2. Use the size of the continuation stack to indicate ongoing communication directly

The latter option will force us to be disciplined about leaving communications behind on the stack, but it avoids odd race conditions and the like.

I’ll sometimes load a file while the idris-notes buffer is already frontmost. But it can be hard to see if it’s been updated with new errors, or just hasn’t finished loading yet. Clearing it immediately will make it easier to tell.

this is a todo item for me to solve really soon now!

1. Create a simple file

module Hello

main : Integer -- IO ()
main = putStrLn "hello"

C-c C-l

The message buffer shows

error in process filter: idris-tree-insert: Symbol's function definition is void: with-struct
error in process filter: Symbol's function definition is void: with-struct

Happens consistently on every reload. HEAD version, didn't happen in the past.

This would allow recovering from broken state. Something like M-x idris-exit.

(this was in the old repo, which I removed)

several solutions come to mind:

• an option -pall for idris to load all packages
• heuristic to find packages
• specify used packages inside of source file (first line, with some special notation)

The indentation code is a rough copy of Haskell-mode, and it's just been hacked a bit. It really needs a principled fix.

The "Loaded" bit is set when a file fails to load. This causes two problems:

1. The modeline shows that it is loaded, even though it isn't
2. If fixing the problem involves doing something outside of the file, such as installing a dependency, then the file needs to be modified in order to load again

Right now, when browsing idris-mode from package-list-packages, the README window for idris-mode is empty. This should at least show the text from the standard README, mention Idris compiler version compatibility, etc.

@purcell any hints?

This is useful when wanting to quickly check that a change didn't introduce type errors.

For example, "if" in "shift" is highlighted

Right now, the code is a bit of a mix between the parts that implement the underlying protocol (continuation stack, request ids, etc) and the parts that deal with actual Idris commands. Make inferior-idris.el only do the former, and move the latter elsewhere.

The latest release of Idris comes with new tooling for interactive editing (cf. agda-mode). See this blog post for more details. Although, the new feature has been implemented in VIM, the Idris REPL does the heavy lifting apparently. Can this new functionality be integrated, easily, within the idris-mode for emacs?

idris-mode dosn't install out of the box from melpa, looks like the dependency on cl is not declared.

If I have a file with many mistakes, the compiler notes buffer shows the last one first.

What license is idris-mode available under? I'd like to incorporate some indentation code from haskell-mode, but that would involve making the whole thing GPL. Is that OK?

I’m used to SLIME – C-c C-z quickly jumps me from a source buffer to the repl. Something like this would be helpful.

I've made a tiny Flycheck checker for Idris and it's been really useful but I can only figure out a way to get a single line of the error message:

(flycheck-define-checker idris
  "An Idris syntax and type checker."
  :command ("idris" "--check" "--nocolor" "--warnpartial" source)
  :error-patterns
  ((warning line-start (file-name) ":" line ":" column ":Warning - " (message) line-end)
   (error line-start (file-name) ":" line ":" column ":" (message) line-end))
  :modes idris-mode
  )

The problem is that there's no clear separation between error messages reported by Idris:

Idris> :l /tmp/Test.idr 
Type checking /tmp/Test.idr
/tmp/Test.idr:1:1:No type declaration for Main.x
/tmp/Test.idr:2:1:No type declaration for Main.y

A filename is how we recognise a new error but I haven't found a way to use that as a regex in the checker.

Any ideas?

Certain interactive editing commands that create new variables (for example, metavars on the RHS) do not reload the buffer, which means that C-c C-t on the metavar doesn't return anything until a C-c C-l has been performed. Idris should reload the buffer after these commands.

since it still uses putStrLn...

in the REPL, the output should appear just before the prompt:

> bla
^C^L

result is output of load-file is inserted before output/result of bla.

rethink and adjust markers and their movement!

When loading a file with a misspelled import, idris-mode simply reports in the minibuffer that the file was not loaded, but the specific error does not appear.

Loading the same file in the command-line REPL shows:

idris ErrorReflectionDemo.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.10.1-git:5eda188
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

user error (Can't find import Langauge/Reflection/Utils)
*ErrorReflectionDemo> 

Having obsolete error messages hang around can be confusing.

I have a file called hello.idr:

main : IO ()
main = putStrLn "Hello, world"

If I try to load this with C-c C-l I get:

(No changes need to be saved)
Connected. Ship if it typechecks!
error in process filter: idris-receive: Assertion failed: (plusp length)
error in process filter: Assertion failed: (plusp length)
Idris quit unexpectly: exited abnormally with code 1

The next time I type C-c C-l in any idris buffer, I get the same error and emacs shows the busy icon until I press C-g, then I get:

Debugger entered--Lisp error: (quit)
  accept-process-output(#<process idris> 0.1)
  byte-code("\306\307!\306\310!^X\211^Y\nL\21^KL\210\311\31J\313\314\315\316\317D\31D\316      D\320\257^EEE\f\"\210*\321\322^]^^^Y\323\f!\324=\203:^@\325\326!\210\327\f\330\"\210\202.^@" [--cl-sexp-- --cl-tag-- tag sexp idris-process inhibit-quit make-symbol "--tag--" "--sexp--" idris-dispatch-event :emacs-rex lambda (&rest --cl-rest--) apply quote #[(G89052 G89053 G89048) \211^Y@^Z  AESC\n\306=\203[^@^K\211^\\203^\^@\f\211A^T@\202#^@\307\310\311\fGD\"^]\f\211A^T@^^^X\f\2039^@\307\310\311\312\fG\\D\"\210^N^YJ^N^Z\235\204L^@\313\314^N^YJ^NESCJ#\210\315^N^YJ\316^M^N^XBD\"+\202\237^@\n\317=\203\233^@^K\211^^^\G\320U\203q^@^N^\@\202y^@\307\310\311^N^\GD\"^^^]\321^N^^\235\203\215^@\322 \203\215^@\323\324\325!!\210\315^N^YJ\313\326^N^]E\"*\202\237^@\313\327    \"+\207" [G89048 tmp-89051 op-89049 rand-89050 --cl-rest-- value :ok signal wrong-number-of-arguments nil 2 error "Reply to canceled synchronous eval request tag=%S sexp=%S" throw identity :error 1 warnings-tree idris-list-compiler-notes pop-to-buffer idris-buffer-name :notes "%s (synchronous Idris evaluation failed)" "ELISP destructure-case failed: %S" spans G89053 idris-stack-eval-tags G89052 --cl-rest-- condition idris-warnings-printing] 6] --cl-rest-- t nil process-status exit error "Idris process exited unexpectedly" accept-process-output 0.1 debug-on-quit] 11)
  idris-eval((:interpret ":cd /home/hars/source/idris/"))
  idris-switch-working-directory("/home/hars/source/idris/")
  idris-load-file()
  call-interactively(idris-load-file nil nil)

the leading count is a character-count, which is pretty useless.

three options:

• switch to byte count
• escape newlines in strings and no count
• use a different special character (like ^L) and no count

I cloned the idris-mode in ~/git/idris-mode/.
Then, I added the following to my ~/.emacs

(add-to-list 'load-path "~/git/idris-mode/")
(add-to-list 'auto-mode-alist '(".idris'" . idris-mode))
(require 'idris-mode)

When I reload emacs, I get :

Warning (initialization): An error occurred while loading `/Users/cog/.emacs':
Symbol's function definition is void: cl-loop

The emacs version is

GNU Emacs 24.2.1 (x86_64-apple-darwin, NS apple-appkit-1038.36) of 2012-08-27 on bob.porkrind.org

Don't know where to go from there.

When a REPL buffer's window is resized, it should set the output width of the underlying Idris process accordingly, in order to get proper pretty-printing line breaks.