Cannot get Agda 2.6.0 to work

[isti115]

I've installed (actually, built) Agda [2.6.0] on Windows [10], the binaries are in the cabal\bin directory, they seem to work perfectly on their own, but when I try to connect to Agda from Atom [1.36.1] (either by giving the full path or just the executable name, as the environmental variables are also set) I only get the following error message:

Found something at "agda" but it doesn't seem quite right: Command failed: agda

[banacorn]

Thanks for reporting this!

[isti115]

Do you have any idea about what I could try? I don't want to go back to Emacs. 😟😞

[banacorn]

I have no problem running Agda-2.6.0 on Windows 10. Could you run agda in the terminal and show me what it is printing?

[isti115]

Thanks for taking the time to look into this!

The output of the agda command is the following:

Microsoft Windows [Version 10.0.17763.437]
(c) 2018 Microsoft Corporation. All rights reserved.

C:\Users\isti115>agda
Agda version 2.6.0

Usage: agda [OPTIONS...] [FILE]

  -V         --version                         show version number
  -?[TOPIC]  --help[=TOPIC]                    show help for TOPIC (available: warning)
  -I         --interactive                     start in interactive mode
             --interaction                     for use with the Emacs mode
             --interaction-json                for use with other editors such as Atom
             --compile-dir=DIR                 directory for compiler output (default: the project root)
             --vim                             generate Vim highlighting files
             --latex                           generate LaTeX with highlighted source code
             --latex-dir=DIR                   directory in which LaTeX files are placed (default: latex)
             --html                            generate HTML files with highlighted source code
             --html-dir=DIR                    directory in which HTML files are placed (default: html)
             --css=URL                         the CSS file used by the HTML files (can be relative)
             --html-highlight=[code,all,auto]  whether to highlight only the code parts (code) or the file as a whole (all) or decide by source file type (auto)
             --dependency-graph=FILE           generate a Dot file with a module dependency graph
             --ignore-interfaces               ignore interface files (re-type check everything)
  -i DIR     --include-path=DIR                look for imports in DIR
  -l LIB     --library=LIB                     use library LIB
             --library-file=FILE               use FILE instead of the standard libraries file
             --no-libraries                    don't use any library files
             --no-default-libraries            don't use default libraries
             --no-forcing                      disable the forcing optimisation
             --only-scope-checking             only scope-check the top-level module, do not type-check it
             --show-implicit                   show implicit arguments when printing
             --show-irrelevant                 show irrelevant arguments when printing
             --no-unicode                      don't use unicode characters when printing terms
  -v N       --verbose=N                       set verbosity level to N
             --allow-unsolved-metas            succeed and create interface file regardless of unsolved meta variables
             --no-positivity-check             do not warn about not strictly positive data types
             --no-termination-check            do not warn about possibly nonterminating code
             --termination-depth=N             allow termination checker to count decrease/increase upto N (default N=1)
             --type-in-type                    ignore universe levels (this makes Agda inconsistent)
             --omega-in-omega                  enable typing rule Set<stdout>: commitBuffer: invalid argument (invalid character)

I have just noticed when copying this, that there seems to be some extra output after the description of the last flag that I haven't realized until now, because it isn't separated by a newline! Do you know what that means?

[isti115]

Hmm, a bit of search led me to this issue: https://github.com/commercialhaskell/stack/issues/1870 In which they mention a solution for windows that switches the codepage to 65001, and it does indeed make it work in the command window, an omega appears where the output was ended earlier and the rest of the flags show up that I haven't seen before, but I cannot manage to make it permanent or set it in the execution environment of Atom. Do you have any idea on how to do that?

[isti115]

Yay, I've managed to make it the default and thus fix it in Atom as well by going to the system's Language settings, selecting Administrative language settings, clicking Change system locale... and checking the Beta: Use Unicode UTF-8 for worldwide language support box! I can now happily start working with Agda again without the hassle of adjusting to Emacs! ;) Now the only thing I'm missing is a bit better syntax highlighting that at least makes a distinction between parameters and constructors. Thank you very much for your input in the solution to this issue!

[banacorn]

Thank you for solving this mystery!

Following your description, It seems like the output was choked by the unicode character ω

             --omega-in-omega                  enable typing rule Setω : Setω (this makes Agda inconsistent)

I shall add this to the readme for troubleshooting!

[banacorn]

This issue was resolved by not asking Agda to print all those stuff out. All we really need was that version number Agda version 2.6.0 anyway