Having trouble with idris-mode

[zenten]

I'm trying a switch over to Emacs from Vim, and I'm having trouble getting idris-mode to work.  It just always says "(Idris (Not loaded)" in the bar.  I couldn't figure out how to change the config parameter to go from idris to /usr/bin/idris , so I tried editing the .el file and recompiling the byte code, and that didn't help either.

[David Christiansen]

I would recommend installing idris-mode from MELPA - that way, you don't
have to muck around with keeping track of .el files.

In any case, the simplest way for new Emacs users to configure the Idris
path is using Customize. In the Idris menu at the top of the Emacs
window, select "Customize idris-mode". Then, scroll down to "Idris
Interpreter Path" (it's the 6th entry in my Emacs, but this can vary a
bit). Click the little triangle to show the setting, and type the path
you want into the text box and click the "Apply and Save" button at the
top of the Customize buffer.

To load an Idris file into the compiler, which runs the type checker,
use C-c C-l or M-x idris-load-file.

Please let me know if this doesn't work for you. Welcome to Emacs :)

/David

[zenten]

Ok, so with the attached screen shot does this mean it's working properly?  It still says (not loaded)

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[David Christiansen]

> Ok, so with the attached screen shot does this mean it's working properly?
> It still says (not loaded)[image: screenshot_20170814_204754.png]

This is not doing what it should. If it had loaded correctly, then all
data constructors, type constructors, bound variables, and user-defined
names would have their own respective colors.

There's a few things to check.

1. What happens if you do M-x idris-repl in a directory without a .ipkg
file in itself nor in any parent directory? (this is the simplest case
to start it up)

2. What if you enter a hello world file and load that with C-c C-l, also
without a .ipkg file?

3. What are the contents of the *idris-events* buffer if you do M-x
idris-quit followed by C-c C-l in your source buffer?

4. Do you have the buffers *idris-process* and *idris-connection* after
attempting to load the file?

Also, I'm excited by what your source file implies :-)

/David

[zenten]

Replies below, mostly in the form of screen shots.  Hope that's OK.

On Mon, Aug 14, 2017 at 9:28 PM David Christiansen <da...@davidchristiansen.dk> wrote:

> Ok, so with the attached screen shot does this mean it's working properly?
> It still says (not loaded)[image: screenshot_20170814_204754.png]

This is not doing what it should. If it had loaded correctly, then all
data constructors, type constructors, bound variables, and user-defined
names would have their own respective colors.

There's a few things to check.

1. What happens if you do M-x idris-repl in a directory without a .ipkg
file in itself nor in any parent directory? (this is the simplest case
to start it up)

 

2. What if you enter a hello world file and load that with C-c C-l, also
without a .ipkg file?

 

3. What are the contents of the *idris-events* buffer if you do M-x
idris-quit followed by C-c C-l in your source buffer?

 

4. Do you have the buffers *idris-process* and *idris-connection* after
attempting to load the file?

I do have these processes when I try to exit from emacs at least:

 

Also, I'm excited by what your source file implies :-)

:)  

I'm pretty slow going, and this is my first open source project, so I don't want to get anyone's hopes up. 

[zenten]

OK, if I do C-c C-l, then let everything load up, then in the buffer with my source code I do C-c C-l *again* it works the second time.

[David Christiansen]

This is a bit unsettling!

Can you try reproducing the behavior in a clean Emacs config? And if
so, please report a bug. If not, then it's a matter of enabling bits of
your config one at a time until the issue is found.

/David

[zenten]

OK, I created a new user account just for this, only installed idris-mode, and I'm getting the same behaviour.

Should I be including my .emacs config in the bug?