Trying to use emacs agda-mode context error C-c C-,

[UlfNorell]

From Alexande...@gmail.com on October 28, 2013 22:01:07

When I load the file and check the context and the goal, the status field shows nothing useful. I tried to install agda in many ways and adga-mode compile and setup many times It will not work correctly? Any one knows?

Attachment: Agda error.png

Original issue: http://code.google.com/p/agda/issues/detail?id=928

[UlfNorell]

From Alexande...@gmail.com on October 28, 2013 14:03:43

I am using GHC 7.6.3 and agda 2.3.2.1 , emacs 24.3.1

[UlfNorell]

From nils.anders.danielsson on October 29, 2013 05:40:15

I get the following output:

Goal: .P ———————————————————————————————————————————————————————————— q : .Q p : .P .Q : Set .P : Set

Can you please show us the contents of the agda2 buffer after running "C-c C-,"? What happens if you execute the following command instead?

M-x agda2-goal-and-context RET

Status: InfoNeeded
Labels: Type-Defect Emacs

[UlfNorell]

From Alexande...@gmail.com on October 29, 2013 05:58:59

It seems that it just give the P as my goal when I press C-c C-, in the curly braces. I tries same thing on my another computer, it shows the same goal as you give. But on my current computer Just ?0 :.P\n. Not sure the problem, I don't know what stupid things I did.

Attachment: emacserror.png

[UlfNorell]

From Alexande...@gmail.com on October 29, 2013 06:03:33

after I try the command I get Agda2> IOTCM "c:/Users/Song/Home/Agda/Test.agda" None Indirect ( Cmd_goal_type_context Normalised 0 noRange "" ) (agda2-status-action "") (agda2-status-action "")

it seems that nothing happened

[UlfNorell]

From nils.anders.danielsson on October 30, 2013 02:37:17

You wrote that you "tried to install agda in many ways and adga-mode compile and setup many times". What happens if you delete everything and do a (single) clean install?

[UlfNorell]

From nils.anders.danielsson on October 30, 2013 08:43:02

Oh, you're using Windows. That explains things (see issue 757 ). Can you please try the following tar-ball instead? http://code.haskell.org/Agda/Agda-2.3.2.2.tar.gz I haven't released 2.3.2.2 yet, because AFAIK this tar-ball has not been tested on Windows.

[UlfNorell]

From Alexande...@gmail.com on October 30, 2013 09:02:48

2.3.2.2 works!!! you guys rock!!!

Attachment: emacs work.png

[UlfNorell]

From nils.anders.danielsson on October 30, 2013 09:51:22

Thanks for your help. I've released Agda 2.3.2.2 now.

Status: Duplicate
Mergedinto: 757