search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

error from /bin/sh #107

Closed zraffer closed 5 years ago

zraffer commented 5 years ago

After fresh install of atom-1.39.0-0.1.x86_64 and language-agda@1.0.9 it says in a new "connection not established" window:

Error: Error from the stderr
error message:

/bin/sh: ml: line 1: syntax error: unexpected end of file
/bin/sh: error importing function definition for `ml'
/bin/sh: module: line 1: syntax error: unexpected end of file
/bin/sh: error importing function definition for `module'

The agda executable is also fresh build from current github master and is usable from command-line and visible in PATH.

banacorn commented 5 years ago

I'm not sure if this is related to agda-mode.

/bin/sh: ml: line 1: syntax error: unexpected end of file
/bin/sh: error importing function definition for `ml'
/bin/sh: module: line 1: syntax error: unexpected end of file
/bin/sh: error importing function definition for `module'

This 4 lines are what Agda wrote to stderr, when agda-mode is trying to run Agda. Could you invoke Agda from your terminal and see if it prints the same stuff?

zraffer commented 5 years ago

The pane has "Connection to Agda" heading, so it is should be from agda-mode, shouldn't it?

From terminal it says:

$ agda Lib.agda
Checking Lib (/usr/local/github/AndrasKovacs/preordertt/cxt/Lib.agda).
banacorn commented 5 years ago

Yes that error was reported by agda-mode, but I'm not sure if it's from agda-mode.

It was trying to validate Agda's version and stuff (by running just agda)

zraffer commented 5 years ago

Identified! The plugin finds agda when atom is started from bash, but not when sterted from desktop environment menu. Seemingly the PATH was not set, because .bashrc did not used by desktop environmnt. But also I should note, that agda-mode cannot find out-of-PATH executable even when path is manually entered into the respective edit field in the connection pane, with the strange error message from /bin/sh as above.

banacorn commented 5 years ago

Here's how the plugin connects with Agda:

  1. it connects with the path read from the settings (Settings > Packages > agda-mode > Agda)
  2. if 1. is empty or that path doesn't work, it looks for the path with which agda (PATH).
  3. if 2. doesn't work either, it asks the user for the path from the panes you see, it will keep asking the user if the given path doesn't work either.

You can try to fill in the fields from Atom's package settings and see if the path works!

zraffer commented 5 years ago

The plugin seems working after update. Thank you. Closing.

banacorn commented 5 years ago

I DID modified some code regarding Agda connection, but I didn't expect this issue to be fixed 😂