bobgus (17) [Avatar] Offline
I have clicked all over Idris space for help in using Atom-Idris and Vim-idris. It has been a mostly frustrating experience.

With Vim, following the instructions in, under the case-splitting example, when I get to the point where I type '\d' nothing happens. None of the '\x' commands seem to work.

Throughout the book, you refer to the REPL. I look for a definition (yes, I know it, but a newby probably would not). Beyond the definition of REPL, there is the question of how to get one started. Is it automatically there when you type 'idris hello.idr', or is there another incantation necessary (like doing 'idris' in one terminal window and then 'idris --client hello.idr' in another window.

It seems as though Idris is useful and the editors can help a lot, but (at least for me), there seems to be a basic layer of knowledge that is missing, like how to successfully get the tools running. Tools are very important for the future acceptance of Idris.

I'm using a Mac air with OS X 10.11.5 - perhaps that is the problem?
Edwin Brady (65) [Avatar] Offline
The REPL, including how to start it up, what REPL stands for, etc, is introduced in Section 1.2. In particular, it says "Once Idris is installed, you can start the REPL by typing idris at a shell prompt" then it goes on to give some examples you can try. Maybe there is something missing from this section?

There isn't really room in the book to go into the details of all the editing tools, so I've focussed on Atom since it is (in my opinion) the easiest editor to get started with. One thing to note is that, because of the limitations of vimscript, you need to have a running idris instance for the editing commands to work.

If you have more specific questions about the tools, either the mailing list or the irc channel should be helpful.
bobgus (17) [Avatar] Offline
Edwin Brady wrote:One thing to note is that, because of the limitations of vimscript, you need to have a running idris instance for the editing commands to work.

Yes, it is nice to know that you need a running idris instance, but a suggestion of how would be helpful. (Run idris in a separate terminal window?)
bobgus (17) [Avatar] Offline
Edwin Brady wrote:..then it goes on to give some examples you can try. Maybe there is something missing from this section?.

I can type on my terminal everything up to example 3.1 with no divergence between your book and what I have on my screen.

The divergence occurs at the point where I have to type commands into Atom to cause things to happen on the screen.

When I follow your instructions:

2. (Define) In Atom, move the cursor over the name word_lengths and press Ctrl-Alt-A.

I get nothing extra on my screen. This is even after I have started up a REPL in another terminal by typing idris.

Ahah, I have the secret!

First you must define EDITOR in the terminal window you are using.

export EDITOR=/usr/local/bin/atom

(Note that this Atom must have the language-idris package installed and enabled)

Then start up idris (REPL ?) in the same terminal window.

idris wordlen.idr (ignore error message..)

Then, at the Idris prompt, type :e


This will open up the EDITOR which has been previously defined as atom.

Then, in the atom window, type in the text

word_lengths : List String -> List Nat

Then, being careful not to introduce any spaces or newlines, move cursor over 'word_lengths' and press ctrl-alt-a

Wonder of all wonders, the correct response magically appears below on line 2, just as in the book.

(If anything else appears, check for added spaces or newlines. Delete extraneous characters, then try again)


I think I have solved my own problem and can work through the rest of your book.
Edwin Brady (65) [Avatar] Offline
Have you installed the Atom mode (as described in Appendix A)?
bobgus (17) [Avatar] Offline
See the additions I snuck in while you were replying.
bobgus (17) [Avatar] Offline
I am backtracking on my process for getting idris and atom to work together.

It seems that defining export EDITOR is not necessary.

I rebooted my computer to clear out all pre-defined shell definitions.

Then - in a terminal window - 'atom wordlen.idr' and then when atom opens up, in the same terminal window, type 'idris wordlen.idr'

It seems that the file wordless.idr must exist prior to executing the above, but I'm testing this assumption too.

Changing the code in atom and issuing ctrl-alt commands works well. For ctrl-alt-t, there is a slight delay and then a new pane opens at the bottom of the main editing window containing the information (new pane because the information is not part of the code)

To get idris to work in the terminal window as in the book, it is necessary to 'save' any changes done in atom first. This seems obvious, but may not be for a first time user (me).

Chapter 3 of the book is very important. (I say this now because I'm still working with Chapter 3).