C-c C-n

[jonaprieto]

It seems that nothing that I define shows the normalizations, and in emacs does.

data Bool : Set where
  False   : Bool                    
  True    : Bool 

¬_ : Bool → Bool
¬ True  = False
¬ False  = True

C-c C-n with ¬ True, atom doesn't show the normal form.

Some Idea? In emacs, it works fine.

[banacorn]

That's weird, because it works on my machine.

Does the panel at the bottom give you a weird normal form, or if it just disappeared? If it's the latter case, then maybe it's some UI-related bug.

p.s. I can't type check¬_ : Bool → True so I tried to reproduce the issue with ¬_ : Bool → Bool.

[jonaprieto]

It Just appears the title, "Compute Normal Formal", not result or anything else.

@banacorn Yes, I was a typo ¬_ : Bool → Bool.

[banacorn]

Thanks for reporting this.

Does this problem happen all the time? Or if it only occurs under certain situation? Because I can't reproduce it :(

[jonaprieto]

Yes, it is happening in every single agda file. The Atom version is the last, 1.12.3.

[banacorn]

May I know which version of Agda you are using?

agda -V

And the configs of agda-mode and core

cat .atom/config.cson 

It looks like that agda-mode has not received any reply :\

[ruhatch]

I am getting this same issue with the development version of Agda (2.6.0-4be18df).

My .atom/config.cson isn't very interesting but I'll post it anyway

"*":
  "agda-mode":
    executablePath: "/home/rupert/.local/bin/agda"
    maxBodyHeight: 496
  core:
    autoHideMenuBar: true
    disabledPackages: [
      "wrap-guide"
      "autohide-tree-view"
      "project-ring"
      "project-jump"
    ]
    packagesWithKeymapsDisabled: [
      "tree-view"
    ]
    telemetryConsent: "limited"
    themes: [
      "arc-ui"
      "one-light-syntax"
    ]
  editor:
    fontFamily: "Input Mono"
    softWrap: true
    softWrapHangingIndent: 2
  "exception-reporting":
    userId: "19a752f3-7afe-157f-1802-8e2fe0557989"
  "git-plus":
    splitPane: "Right"
  "haskell-ghc-mod": {}
  hidpi: {}
  "ide-haskell": {}
  "ide-haskell-repl":
    commandArgs: [
      "ghci"
    ]
    commandPath: "stack"
  latextools:
    forwardSync: false
    keepFocus: false
    linux: {}
    refAddParenthesis: true
  linter: {}
  "pdf-view":
    fitToWidthOnOpen: true
  "project-manager":
    alwaysOpenInSameWindow: true
    includeGitRepositories: true
  "spell-check":
    grammars: [
      "source.asciidoc"
      "source.gfm"
      "text.git-commit"
      "text.plain"
      "text.plain.null-grammar"
      "text.tex.latex"
    ]
  term3:
    colors:
      background: "#282c34"
    fontFamily: "Input Mono"
  "tree-view":
    hideVcsIgnoredFiles: true
  "vim-mode": {}
  welcome:
    showOnStartup: false
  wordcount:
    extensions: [
      "md"
      "markdown"
      "readme"
      "txt"
      "rst"
      "adoc"
      "log"
      "msg"
      "tex"
    ]
    hidechars: true
".c2hs.source":
  editor:
    softWrapHangingIndent: 2
".cabal.source":
  editor:
    softWrapHangingIndent: 2
".diff":
  editor:
    softWrapHangingIndent: 2
".diff.source":
  editor:
    softWrapHangingIndent: 2
".haskell.hint":
  editor:
    softWrapHangingIndent: 2
".haskell.hint.message":
  editor:
    softWrapHangingIndent: 2
".haskell.hint.type":
  editor:
    softWrapHangingIndent: 2
".haskell.latex.tex.text":
  editor:
    softWrapHangingIndent: 2
".haskell.source":
  editor:
    softWrapHangingIndent: 2
".hsc2hs.source":
  editor:
    softWrapHangingIndent: 2

Any help would be much appreciated!

[ruhatch]

The output in the developer console is

Agda parse error: IOTCM,/home/rupert/github/HoTT-Agda/theorems/groupoids/SymmetricHIT2.agda,NonInteractive,Direct,Cmd_compute,False,0,noRange,f (g b)

[banacorn]

That parse error is really helpful! It seems that the parsing has gone wrong. In case you are in the development mode, you should see that there's a button here on the right of the panel.

If you open it you will see two columns, it would be nice if you could identify the string where the parser panics.

Thanks!!

[ruhatch]

My output is

(sorry for the large screenshot!)

[banacorn]

After some further investigation, I found that the issue @ruhatch had reported is related to some protocol updates in Agda 2.6. We should move to #41.