search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

agda not working well with ghci 7.0.3 , haskell platform haskell2010-1.0.0.0 . #410

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From denghao8...@gmail.com on April 23, 2011 02:28:07

The problem : Here is the ghci buffer after load agda : 

 Prelude> :set -package Agda-2.2.10

Prelude> ioTCM "/Users/dh/agda/1.agda" Nothing ( cmd_write_highlighting_info "/Users/dh/agda/1.agda" "/tmp/emacs/agda2-mode533g4u" )

:1:1: Not in scope: `ioTCM' after I manually added : Prelude> :m + Agda.Interaction.GhciTop it seems fine. so it seemed that the behavior of :set -package changed. _Original issue: http://code.google.com/p/agda/issues/detail?id=410_
UlfNorell commented 10 years ago

From nils.anders.danielsson on April 23, 2011 01:42:05

Can you please provide more detailed information?

Status: InfoNeeded

UlfNorell commented 10 years ago

From denghao8...@gmail.com on April 23, 2011 04:50:56

GHCi, version 7.0.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Loading package ffi-1.0 ... linking ... done. Prelude> :set -package Agda-2.2.10 package flags have changed, resetting and loading new packages... Loading package extensible-exceptions-0.1.1.2 ... linking ... done. Loading package transformers-0.2.2.0 ... linking ... done. Loading package mtl-2.0.1.0 ... linking ... done. Loading package old-locale-1.0.0.2 ... linking ... done. Loading package time-1.2.0.3 ... linking ... done. Loading package random-1.0.0.3 ... linking ... done. Loading package array-0.3.0.2 ... linking ... done. Loading package containers-0.4.0.0 ... linking ... done. Loading package pretty-1.0.1.2 ... linking ... done. Loading package template-haskell ... linking ... done. Loading package QuickCheck-2.4.0.1 ... linking ... done. Loading package bytestring-0.9.1.10 ... linking ... done. Loading package binary-0.5.0.2 ... linking ... done. Loading package filepath-1.2.0.0 ... linking ... done. Loading package old-time-1.0.0.6 ... linking ... done. Loading package unix-2.4.2.0 ... linking ... done. Loading package directory-1.1.0.0 ... linking ... done. Loading package terminfo-0.3.1.3 ... linking ... done. Loading package utf8-string-0.3.6 ... linking ... done. Loading package haskeline-0.6.4.0 ... linking ... done. Loading package process-1.0.1.5 ... linking ... done. Loading package haskell98-1.1.0.1 ... linking ... done. Loading package cpphs-1.11 ... linking ... done. Loading package haskell-src-exts-1.9.6 ... linking ... done. Loading package syb-0.2.2 ... linking ... done. Loading package xhtml-3000.2.0.1 ... linking ... done. Loading package zlib-0.5.3.1 ... linking ... done. Loading package Agda-2.2.10 ... linking ... done. Prelude> ioTCM "/Users/dh/agda/monoid.agda" (Just "/tmp/emacs/agda2-mode229QGC") ( cmd_load "/Users/dh/agda/monoid.agda" ["."] )

:1:1: Not in scope: `ioTCM' :1:75: Not in scope: `cmd_load' # ghc-pkg return nothing MacBookAir:~ dh$ ghc-pkg check MacBookAir:~ dh$ MacBookAir:~ dh$ ghc-pkg list /Library/Frameworks/GHC.framework/Versions/7.0.3-i386/usr/lib/ghc-7.0.3/package.conf.d Cabal-1.10.1.0 GLUT-2.1.2.1 HTTP-4000.1.1 HUnit-1.2.2.3 OpenGL-2.2.3.0 QuickCheck-2.4.0.1 array-0.3.0.2 base-4.3.1.0 bin-package-db-0.0.0.0 bytestring-0.9.1.10 cgi-3001.1.7.4 containers-0.4.0.0 deepseq-1.1.0.2 directory-1.1.0.0 extensible-exceptions-0.1.1.2 ffi-1.0 fgl-5.4.2.3 filepath-1.2.0.0 ghc-7.0.3 ghc-binary-0.5.0.2 ghc-prim-0.2.0.0 haskell-platform-2011.2.0.1 haskell-src-1.0.1.4 haskell2010-1.0.0.0 haskell98-1.1.0.1 hpc-0.5.0.6 html-1.0.1.2 integer-gmp-0.2.0.3 mtl-2.0.1.0 network-2.3.0.2 old-locale-1.0.0.2 old-time-1.0.0.6 parallel-3.1.0.1 parsec-3.1.1 pretty-1.0.1.2 process-1.0.1.5 random-1.0.0.3 regex-base-0.93.2 regex-compat-0.93.1 regex-posix-0.94.4 rts-1.0 stm-2.2.0.1 syb-0.3 template-haskell-2.5.0.0 text-0.11.0.6 time-1.2.0.3 transformers-0.2.2.0 unix-2.4.2.0 xhtml-3000.2.0.1 zlib-0.5.3.1 /Users/dh/.ghc/i386-darwin-7.0.3/package.conf.d Agda-2.2.10 binary-0.5.0.2 cpphs-1.11 haskeline-0.6.4.0 haskell-src-exts-1.9.6 syb-0.2.2 terminfo-0.3.1.3 utf8-string-0.3.6 Mac OS X 10.6.7
UlfNorell commented 10 years ago

From denghao8...@gmail.com on April 23, 2011 05:26:05

I forget to mention that I'm using agda 2.2.8

MacBookAir:~ dh$ agda -V Agda version 2.2.8

UlfNorell commented 10 years ago

From nils.anders.danielsson on April 23, 2011 12:22:26

The Emacs mode should insert the command

:mod + Agda.Interaction.GhciTop

before the call to cmd_load. Can you debug the Emacs Lisp code, please?

  1. Open and load an Agda file (in Emacs).
  2. Open agda2-mode.el, place the cursor in the body of agda2-restart and type C-u C-M-x.
  3. Switch back to the Agda file and restart Agda (C-c C-x C-r).
  4. Step through agda2-restart (SPC SPC SPC...).

What I would like to know is why the penultimate line of agda2-restart ((agda2-call-ghci ":mod +" agda2-toplevel-module)) is not executed properly.

UlfNorell commented 10 years ago

From denghao8...@gmail.com on April 24, 2011 02:34:51

I found the problem . I'm mixing agda 2.2.8 and agda-mode 2.2.10

It's confusing that cabal install agda only install agda-mode, and you have to do cabal install agda-executable.

Is it really necessary to split it in two haskell packages ?

Regards. Hao Deng

UlfNorell commented 10 years ago

From nils.anders.danielsson on April 24, 2011 04:21:04

I found the problem . I'm mixing agda 2.2.8 and agda-mode 2.2.10

I don't see how this can cause the symptoms you reported. The agda executable is not used by the Emacs mode.

It's confusing that cabal install agda only install agda-mode, and you have to do cabal install agda-executable.

Is it really necessary to split it in two haskell packages ?

Cabal does not fully support packages containing both libraries and executables: http://hackage.haskell.org/trac/hackage/ticket/656

Status: WontFix

UlfNorell commented 10 years ago

From denghao8...@gmail.com on April 24, 2011 04:56:10

Thanks nils.anders.danielsson for the time and effort.

Here is the situation: I installed agda 2.2.8 a long time ago.

then yesterday, cabal install agda , which upgrade agda-mode to 2.2.10, but left agda in 2.2.8 then above problem appears.

after cabal install agda-executable , everything is fine.

Happy agdaing!

UlfNorell commented 10 years ago

From denghao8...@gmail.com on April 24, 2011 17:03:00

I'm able to reproduce the bug after a restart. In fact , the above error is not the first error. The first error is following, which I failed to mention before.

Loading /Users/dh/.viper...done Loading /Users/dh/haskellmode-emacs/haskell-site-file.el (source)...done Loading /Users/dh/ProofGeneral-4.0/ProofGeneral/generic/proof-site.el (source)...done Loading /Users/dh/.cabal/share/Agda-2.2.10/emacs-mode/agda2.el (source)...done For information about GNU Emacs and the GNU system, type C-h C-a. Loading quail/latin-ltx...done Starting GHCi process `ghci'. (No changes need to be saved) File mode specification error: (file-error "Opening output file" "No such file or directory" "/tmp/emacs/agda2-mode1639iL")

so after I manually mkdir /tmp/emacs

and restart emacs , everything is fine.

so the question is : did you created /tmp/emacs ? do you have access right to create a fold at /tmp/ ?

UlfNorell commented 10 years ago

From nils.anders.danielsson on April 25, 2011 14:58:45

The Emacs mode creates temporary files in the directory specified by the variable "temporary-file-directory". If this variable points to a non-existent directory, then I am not surprised if things go wrong.

You may want to modify this variable:

M-x customize-variable RET temporary-file-directory RET