Uncaught Error: This socket has been ended by the other party

[jeremy-w]

I'm not finding any crash report for the idris executable.

1. Enter this code (I'm working on the "Well-Typed Interpreter" example):

import Data.Vect

-- Start by representing our universe as a product type.
data Ty = TyInt | TyBool | TyFun Ty Ty

interpret : Ty -> Type
interpret TyInt = Int
interpret TyBool = Bool
interpret (TyFun A T) = interpret A -> interpret T

-- G represents our expression environment.
let Env = Vect n Ty
using (G: Env)
    data Expr : Env -> Ty -> Type

1. Try to typecheck it. You'll see a "process crashed" message about the idris process exiting with code 1.
2. Try to typecheck it again. This and each further attempt gives this error about writing to a socket whose other end is closed. This error seems to recur each time I try to typecheck.

I have no idea how to try to restart the connection short of relaunching the entire editor. Suggestions:

• Add a "relaunch idris" command
• Relaunch and reconnect to it automatically (at least a couple times, to avoid spinning on repeated crashers) when it's detected as having exited, since much of the package functionality relies on it

Atom Version: 1.0.5
System: Mac OS X 10.10.4
Thrown From: language-idris package, v0.2.4

Stack Trace

Uncaught Error: This socket has been ended by the other party

At events.js:141

Error: This socket has been ended by the other party
  at Socket.writeAfterFIN [as write] (net.js:275:12)
  at IdrisIdeMode.send (/Users/jeremy/.atom/packages/language-idris/lib/idris-ide-mode.coffee:24:20)
  at IdrisModel.prepareCommand (/Users/jeremy/.atom/packages/language-idris/lib/idris-model.coffee:64:16)
  at IdrisModel.load (/Users/jeremy/.atom/packages/language-idris/lib/idris-model.coffee:68:6)
  at IdrisController.typecheckFile (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:70:8)
  at /Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:1:1
  at atom-text-editor.<anonymous> (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:51:7)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at CommandPaletteView.module.exports.CommandPaletteView.confirmed (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/command-palette/lib/command-palette-view.js:159:32)
  at CommandPaletteView.module.exports.SelectListView.confirmSelection (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-space-pen-views/lib/select-list-view.js:338:21)
  at space-pen-div.atom.commands.add.core:confirm (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-space-pen-views/lib/select-list-view.js:109:19)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at KeymapManager.module.exports.KeymapManager.dispatchCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:524:16)
  at KeymapManager.module.exports.KeymapManager.handleKeyboardEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:347:22)
  at HTMLDocument.module.exports.WindowEventHandler.onKeydown (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/window-event-handler.js:177:20)

Commands

     -0:47.6.0 core:move-right (atom-text-editor.editor.is-focused)
  3x -0:47.4.0 editor:select-to-beginning-of-word (atom-text-editor.editor.is-focused)
     -0:45.9.0 core:save (atom-text-editor.editor.is-focused.autocomplete-active)
     -0:45.7.0 core:move-down (atom-text-editor.editor.is-focused)
  4x -0:45.4.0 editor:move-to-end-of-word (atom-text-editor.editor.is-focused)
  3x -0:44.2.0 editor:select-to-beginning-of-word (atom-text-editor.editor.is-focused)
     -0:42.7.0 core:save (atom-text-editor.editor.is-focused.autocomplete-active)
     -0:25 editor:move-to-end-of-screen-line (atom-text-editor.editor.is-focused)
     -0:23.1.0 core:save (atom-text-editor.editor.is-focused)
  2x -0:15 language-idris:typecheck (atom-text-editor.editor.is-focused)
     -0:08.5.0 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -0:08.5.0 core:cancel (atom-text-editor.editor.is-focused)
     -0:06.1.0 command-palette:toggle (atom-text-editor.editor.is-focused)
     -0:04.7.0 core:backspace (atom-text-editor.editor.mini.is-focused)
     -0:01.1.0 core:confirm (atom-text-editor.editor.mini.is-focused)
     -0:01.1.0 language-idris:typecheck (atom-text-editor.editor)

Config

{
  "core": {
    "themes": [
      "atom-material-ui",
      "atom-material-syntax"
    ]
  },
  "language-idris": {
    "pathToIdris": "/usr/local/bin/idris"
  }
}

Installed Packages

# User
atom-material-syntax, v0.2.2
atom-material-ui, v0.5.13
autocomplete-haskell, v0.4.5
haskell-ghc-mod, v0.8.9
ide-haskell, v0.7.1
language-haskell, v1.3.1
language-idris, v0.2.4

# Dev
No dev packages

[jeremy-w]

I just ran idris interpreter.idr directly, and got this error:

idris: src/Idris/ParseHelpers.hs:429:20-46: Irrefutable pattern failed for pattern (x : xs)

This is against Idris version 0.9.18- as installed via Homebrew.

[archaeron]

Thanks for reporting this.

How about:

• a "relaunch idris" command
• if the compiler is not running before a command, start it once.

I don't think it makes sense to restart instantly because it is very probable that it will just crash again. This way you can make your changes to the file and then use a command.

[david-christiansen]

In the Emacs mode, Idris is always started as a side effect of a user-issued command, such as "case split this" or "type check this". If it fails to start, or crashes, then the command fails and gives the user an error message. If Idris has crashed, then the next command will attempt to restart it, but it won't get stuck in a loop of repeatedly starting Idris.

[archaeron]

This was what I tried to explain :)
I'm glad you're doing the same thing, thanks! :)

[david-christiansen]

For what it's worth, this is how Slime and friends work as well.

[jeremy-w]

So it sounds like the decision was:

• Each user command that needs to interact with idris should first try to ensure it has an idris process to talk to. If the process dies, that should be reported, but the next command will try to launch it again.

This means that each user interaction is effectively a restart attempt if the process has exited.

In IRC, davidwlewis reports that sometimes idris starts eating 100% CPU, so they'd like to be able to restart/kill the process from Atom. This suggests that we might actually want a terminate process command, as well.

[david-christiansen]

Each user command that needs to interact with idris should first try to ensure it has an idris process to talk to. If the process dies, that should be reported, but the next command will try to launch it again.

each user interaction is effectively a restart attempt if the process has exited.

That's how it works in Emacs. It's been fairly effective. Emacs also has an idris-quit command to terminate the subprocess.

[archaeron]

first draft here: #54

[archaeron]

this is now in v0.2.5

[goofballLogic]

I'm getting crashes ( idris 0.11, language-idris 0.4..4 ) but they link me to this issue saying it has already been reported. Who do I believe?

[archaeron]

could you describe your issue?