星之一角: happy 灌不起來真不 happy (2)

[quote="Josh Ko"]
我猜 cabal install happy 應該成功了。happy 會有個執行檔，而不會現身為 Haskell package。
2008年11月27日下午 9:18
[/quote]

我也覺得應該成功了，可是 agda configure 不過，
以為一定要是 ghc package. 改改看 configure 看看好了，
如果他只是要執行檔的話，應該跳過檢查即可
2008年11月27日下午 9:59

Hmm...
godfat ~/p/Agda> ./configure --with-happy ~/.cabal/bin/happy

configure: error: happy version 1.14 or later required

很好，修改 configure:
> if test "$fp_num1" -ge "0"; then
拜託，1.18 應該大於 1.14 吧...

重跑之後，configure 真的過了，只是 make 沒過

感謝，這樣就可以繼續試了 @@
2008年11月27日下午 10:04

QuickCheck 2.1.0.1 灌不起來
根據：
http://lists.osuosl.org/pipermail/darcs-users/2008-November/015959.html
成功 build 起來。

把 QuickCheck/build/* 移動到
~/.cabal/lib/QuickCheck-2.1.0.1/ghc-6.10.1 裡面
rm 掉 1.2.0.0

修改 ~/.ghc/i386-darwin-6.10.1/package.conf
把 QuickCheck-1.2.0.0 的字全改成 QuickCheck-2.1.0.1

修改 /opt/local/lib/ghc-6.10.1/package.conf
把上面的 package.conf 中的 InstalledPackageInfo
全部 copy 到最下面，小心別 copy 錯了
godfat ~/p/Agda> make
runhaskell Setup.hs configure
Configuring Agda-2.1.3...
Setup.hs: At least the following dependencies are missing:
binary >=0.4.4 && <0.5, haskeline ==0.3.*
make: *** [dist/setup-config] Error 1
終於只欠兩樣東西了...
由 godfat 真常於 2008年11月27日下午 10:52 張貼在星之一角 2.3.3

binary 0.4.4 原來是忘記 copy

haskeline 需要降級，下載 build 之後，
依樣畫狐狸，copy haskeline 0.4 的所有東西，
全部改成 0.3.2, 希望 signature 沒變...

godfat ~/p/Agda> make
runhaskell Setup.hs configure
Configuring Agda-2.1.3...
Setup.hs: happy version >=1.15 && <2 is required but it could not be found.

make: *** [dist/setup-config] Error 1

唉，又卡關了
由 godfat 真常於 2008年11月27日下午 11:08 張貼在星之一角 2.3.3

我出運了！！
godfat ~/p/Agda> set PATH $PATH ~/.cabal/bin/
godfat ~/p/Agda> make
runhaskell Setup.hs configure
Configuring Agda-2.1.3...
runhaskell Setup.hs build
Preprocessing library Agda-2.1.3...
Building Agda-2.1.3...
[ 1 of 177] Compiling Agda.Version ( src/full/Agda/Version.hs, dist/build/Agda/Version.o )
[...]
耶，洗澡去...
由 godfat 真常於 2008年11月27日下午 11:11 張貼在星之一角 2.3.3
[...]
[177 of 177] Compiling Agda.Main ( src/full/Agda/Main.hs, dist/build/Agda/Main.o )
ar: creating archive dist/build/libHSAgda-2.1.3.a
runhaskell Setup.hs register --user --inplace
Registering Agda-2.1.3...
Reading package info from "dist/inplace-pkg-config" ... done.
Writing new package config file... done.
make -C ./src/main
runhaskell Setup.hs configure --user
Configuring Agda-executable-2.1.3...
Rebuilding executable...
runhaskell Setup.hs build
Preprocessing executables for Agda-executable-2.1.3...
Building Agda-executable-2.1.3...
[1 of 1] Compiling Main ( Main.hs, dist/build/agda/agda-tmp/Main.o )
Linking dist/build/agda/agda ...
make -C ./src/core
mkdir -p ../../out/core
mkdir -p ../../out/core/Thierry
bnfc -haskell -d Core.cf
make[1]: bnfc: Command not found
make[1]: *** [../../out/core/Core/Par.y] Error 127
make: *** [core] Error 2
啥鬼？

http://www.cs.chalmers.se/Cs/Research/Language-technology/BNFC/

直接下載 binary, 懶得 compile 了
ln -s bndc-2.4b-macosx-i386 ~/.cabal/bin/bnfc
godfat ~/p/Agda> make
make -C ./src/core
bnfc -haskell -d Core.cf
The BNF Converter, 2.4b
(c) Bjorn Bringert, Johan Broberg, Paul Callaghan, Markus Forsberg,
Ola Frid, Peter Gammie, Patrik Jansson, Kristofer Johannisson,
Antti-Juhani Kaijanaho, Ulf Norell, Michael Pellauer
and Aarne Ranta 2002 - 2008.
Free software under GNU General Public License (GPL).
Bug reports to {markus,aarne}@cs.chalmers.se.


Reading grammar from Core.cf
33 rules accepted

Creating directory Core
writing file Core/Abs.hs
writing file Core/Lex.x
(Use Alex 2.0 to compile.)
writing file Core/Par.y
(Tested with Happy 1.15)
writing file Core/Doc.tex
writing file Core/Doc.txt
writing file Core/Skel.hs
writing file Core/Print.hs
writing file Core/Layout.hs
writing file Core/Test.hs
writing file Core/ErrM.hs
Done!
rm -rf ../../out/core/Core
mv Core ../../out/core
yes -agc --info=../../out/core/Core/Par.happy.out ../../out/core/Core/Par.y -o ../../out/core/Core/Par.hs
-agc
-agc
-agc
-agc
[...]
..........
一直瘋狂吐出 -agc 之類的
ctrl + c => interrupt

terminal 看起來快當了，真是一波萬折啊...
由 godfat 真常於 2008年11月27日下午 11:23 張貼在星之一角 2.3.3

注意到好像是因為他 invoke yes...
godfat ~/p/Agda> which yes
/usr/bin/yes

不知道是啥鬼？
暫時移掉
godfat ~/p/Agda> sudo mv /usr/bin/yes /usr/bin/yes.bak
godfat ~/p/Agda> make
make -C ./src/core
bnfc -haskell -d Core.cf
[...]

writing file Core/ErrM.hs
Done!
rm -rf ../../out/core/Core
mv Core ../../out/core
yes -agc --info=../../out/core/Core/Par.happy.out ../../out/core/Core/Par.y -o ../../out/core/Core/Par.hs
make[1]: yes: Command not found
make[1]: *** [../../out/core/Core/Par.hs] Error 127
rm ../../out/core/Core/Par.y
make: *** [core] Error 2
很好，那我就來偽造 yes 成 happy.
godfat ~/p/Agda> ln -s ~/.cabal/bin/happy ~/.cabal/bin/yes
godfat ~/p/Agda> make
make -C ./src/core
bnfc -haskell -d Core.cf
[...]

yes -agc --info=../../out/core/Core/Par.happy.out ../../out/core/Core/Par.y -o ../../out/core/Core/Par.hs
unused terminals: 1
alex -g ../../out/core/Core/Lex.x -o ../../out/core/Core/Lex.hs
ghc --make -o ../../out/core/agdacore -odir ../../out/core -hidir ../../out/core -i../../out/core -O -Wall -Werror -fno-warn-missing-signatures -fno-warn-name-shadowing -fno-warn-simple-patterns -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports -fno-warn-type-defaults -fno-warn-orphans -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns Main.hs
[1 of 6] Compiling Core.Lex ( ../../out/core/Core/Lex.hs, ../../out/core/Core/Lex.o )
[2 of 6] Compiling Core.Abs ( ../../out/core/Core/Abs.hs, ../../out/core/Core/Abs.o )
[3 of 6] Compiling Core.Print ( ../../out/core/Core/Print.hs, ../../out/core/Core/Print.o )
[4 of 6] Compiling Core.ErrM ( ../../out/core/Core/ErrM.hs, ../../out/core/Core/ErrM.o )
[5 of 6] Compiling Core.Par ( ../../out/core/Core/Par.hs, ../../out/core/Core/Par.o )
[6 of 6] Compiling Main ( Main.hs, ../../out/core/Main.o )
Linking ../../out/core/agdacore ...
rm ../../out/core/Core/Par.y
(cd ./src/transl; runhaskell Setup.hs build)
Setup.hs: Run the 'configure' command first.
make: *** [transl] Error 1
.....重來
godfat ~/p/Agda> runhaskell Setup.hs configure
Configuring Agda-2.1.3...
godfat ~/p/Agda> make
runhaskell Setup.hs build
Preprocessing library Agda-2.1.3...
Building Agda-2.1.3...

ar: creating archive dist/build/libHSAgda-2.1.3.a
runhaskell Setup.hs register --user --inplace
Registering Agda-2.1.3...
Reading package info from "dist/inplace-pkg-config" ... done.
Writing new package config file... done.
make -C ./src/main
make[1]: Nothing to be done for `default'.
make -C ./src/core
make[1]: Nothing to be done for `default'.
(cd ./src/transl; runhaskell Setup.hs build)
Setup.hs: Run the 'configure' command first.
make: *** [transl] Error 1
這次只針對 transl:
godfat ~/p/Agda> cd ./src/transl; runhaskell Setup.hs configure
Configuring Agda1to2-2.0.1...

Setup.hs: At least the following dependencies are missing:
Agda >=2.0.1
昏倒... 為什麼灌到一半會需要自己？
由 godfat 真常於 2008年11月27日下午 11:41 張貼在星之一角 2.3.3

中間還重灌了 bnfc, 根據：

http://www.cs.chalmers.se/Cs/Research/Language-technology/BNFC/

darcs get --partial http://www.cs.chalmers.se/Cs/Research/Language-technology/darcs/BNFC/

結果他說改用 http://code.haskell.org/bnfc

改用之後 make 成功建成 bnfc, 丟一個 hard link 到 ~/.cabal/bin

都要凌晨了，明早繼續好了... >_<
本來要十點睡的...

由 godfat 真常於 2008年11月27日下午 11:46 張貼在星之一角 2.3.3

ok, 想到 transl 應該不是 agda 本體，沒灌應該沒差，安裝看看：

godfat ~/p/Agda> runhaskell Setup.hs install
Setup.hs: /usr/local/share/doc/Agda-2.1.3: createDirectory: permission denied (Permission denied)

改灌到現在目錄：

godfat ~/p/Agda> runhaskell Setup.hs configure --user --prefix=/Users/godfat/projects/Agda/
Configuring Agda-2.1.3...

godfat ~/p/Agda> runhaskell Setup.hs build
Preprocessing library Agda-2.1.3...
Building Agda-2.1.3...
ar: creating archive dist/build/libHSAgda-2.1.3.a
godfat ~/p/Agda> runhaskell Setup.hs install
Installing library in /Users/godfat/projects/Agda//lib/Agda-2.1.3/ghc-6.10.1
Registering Agda-2.1.3...
Reading package info from "dist/installed-pkg-config" ... done.
Writing new package config file... done.

真的安裝好了耶？試試看：

godfat ~/p/Agda> ghc-pkg list
/opt/local/lib/ghc-6.10.1/./package.conf:
    Cabal-1.6.0.1, HTTP-3001.1.4, HUnit-1.2.0.3, QuickCheck-1.2.0.0,
    QuickCheck-2.1.0.1, array-0.2.0.0, base-3.0.3.0, base-4.0.0.0,
    binary-0.4.3.1, binary-0.4.4, bytestring-0.9.1.4,
    containers-0.2.0.0, directory-1.0.0.2, (dph-base-0.3),
    (dph-par-0.3), (dph-prim-interface-0.3), (dph-prim-par-0.3),
    (dph-prim-seq-0.3), (dph-seq-0.3), editline-0.2.1.0,
    extensible-exceptions-0.1.1.0, filepath-1.1.0.1, (ghc-6.10.1),
    ghc-prim-0.1.0.0, haddock-2.3.0, haskeline-0.3.2, haskeline-0.4,
    haskell-src-1.0.1.3, haskell98-1.0.1.0, hpc-0.5.0.2, html-1.0.1.2,
    integer-0.1.0.0, mtl-1.1.0.2, network-2.2.0.1, old-locale-1.0.0.1,
    old-time-1.0.0.1, packedstring-0.1.0.1, parallel-1.1.0.0,
    parsec-2.1.0.1, pretty-1.0.1.0, process-1.0.1.0, random-1.0.0.1,
    regex-base-0.72.0.2, regex-compat-0.71.0.1, regex-posix-0.72.0.3,
    rts-1.0, stm-2.1.1.2, syb-0.1.0.0, template-haskell-2.3.0.0,
    terminfo-0.2.2.1, time-1.1.2.2, unix-2.3.1.0, utf8-string-0.3.3,
    xhtml-3000.2.0.1, zlib-0.5.0.0
/Users/godfat/.ghc/i386-darwin-6.10.1/package.conf:
    Agda-2.1.3, QuickCheck-2.1.0.1, binary-0.4.4,
    extensible-exceptions-0.1.1.0, haskeline-0.3.2, haskeline-0.4,
    terminfo-0.2.2.1, utf8-string-0.3.3

那執行檔咧？

godfat ~/p/Agda> out/core/agdacore 
agdacore: user error (Pattern match failure in do expression at Main.hs:13:8-13)

不是這個嗎？跑測試看看：

godfat ~/p/Agda> make test
======================================================================
===================== Suite of successfull tests =====================
======================================================================
AbsurdLam.agda
AbsurdPattern.agda
Berry.agda
builtin.agda
builtinInModule.agda
[...]
Testing Termination/Tuple.agda... 
ok
======================================================================
======================= Suite of failing tests =======================
======================================================================
BadInductionRecursion1.agda
BadInductionRecursion1.tmp.2 BadInductionRecursion1.tmp.3 differ: char 220, line 1
== Old error ===
BadInductionRecursion1.agda:8,8-9
D is not strictly positive, because it occurs in the first clause
in the definition of D′, which occurs to the left of an arrow in
the type of the constructor d in the definition of D
== New error ===
BadInductionRecursion1.agda:8,8-9
D is not strictly positive, because it occurs in the first clause
in the definition of D′, which occurs to the left of an arrow in
the type of the constructor d in the definition of D.
rm -f BadInductionRecursion1.tmp
rm -f BadInductionRecursion1.tmp.2
make[1]: *** [BadInductionRecursion1] Error 1
make: *** [fail] Error 2

看起來正常，一定有執行檔，或是另外的執行方式。查看 Makefile:

tests :
 @echo "======================================================================"
 @echo "======================== Internal test suite ========================="
 @echo "======================================================================"
 $(AGDA_BIN) --test

這表示肯定有執行檔，到底在哪？加個 echo 進去看看：

@echo $(AGDA_BIN)

加在 tests 最前面

godfat ~/p/Agda> make tests
======================================================================
======================== Internal test suite =========================
======================================================================
./src/main/dist/build/agda/agda
./src/main/dist/build/agda/agda --test
QuickCheck test suite:
Agda.Compiler.MAlonzo.Encode
+++ OK, passed 100 tests.
+++ OK, passed 100 tests.

我看到了！可是為什麼放在 src 裡，不是放在 dist 或 out 裡？？

godfat ~/p/Agda> src/main/dist/build/agda/agda
Agda 2

Usage: agda [OPTIONS...] FILE

  -V      --version               show version number
  -?      --help                  show this help
  -i DIR  --include-path=DIR      look for imports in DIR
  -I      --interactive           start in interactive mode
  -c      --compile               compile program to Haskell (experimental)
          --agate                 use the Agate compiler (only with --compile)
          --alonzo                use the Alonzo compiler (only with --compile)
          --malonzo               use the MAlonzo compiler (DEFAULT) (only with --compile)
          --malonzodir=DIR        set the directory for MAlonzo output
          --test                  run internal test suite
          --vim                   generate Vim highlighting files
          --emacs                 generate Emacs highlighting files
          --ignore-interfaces     ignore interface files (re-type check everything)
          --ghc-flag=GHC-FLAG     use GHC-FLAG for compilation
  -v N    --verbose=N             set verbosity level to N
          --show-implicit         show implicit arguments when printing
          --proof-irrelevance     enable proof irrelevance (experimental feature)
          --allow-unsolved-metas  allow unsolved meta variables (only needed in batch mode)
          --no-positivity-check   do not warn about not strictly positive data types
          --no-termination-check  do not warn about possibly nonterminating code
          --no-coverage-check     do not warn about possibly incomplete pattern matches
          --type-in-type          ignore universe levels (this makes Agda inconsistent)
          --sized-types           use sized datatypes

Plugins:

啊！真感動，看看 interactive mode:

godfat ~/p/Agda> src/main/dist/build/agda/agda -I
                 _        ______
   ____         | |      |_ __ _|
  / __ \        | |       | || |
 | |__| |___  __| | ___   | || |
 |  __  / _ \/ _  |/ __\  | || |   Agda 2 Interactive
 | |  |/ /_\ \/_| / /_| \ | || |
 |_|  |\___  /____\_____/|______|  Type :? for help.
        __/ /
        \__/

The interactive mode is no longer supported. Don't complain if it doesn't work.

只是最下面那行有點蠢...... 我喜歡 interactive mode 說。
安裝 std-lib

godfat ~/p/Agda> make std-lib
make: `std-lib' is up to date.

對不起，我跑過了，訊息沒留下來... 總之他就只是用 darcs 抓下來到 std-lib 裡。
上面那跟 cd std-lib; darcs pull; 的意思應該一樣。

跑跑看 Josh 的 Derivation:

godfat ~/p/Agda> src/main/dist/build/agda/agda -i std-lib/ ~/projects/haskell/Derivation.agda 
Checking Data.Product ( /Users/godfat/projects/Agda/std-lib/Data/Product.agda )
Checking Data.Function ( /Users/godfat/projects/Agda/std-lib/Data/Function.agda )
Checking Relation.Nullary.Core ( /Users/godfat/projects/Agda/std-lib/Relation/Nullary/Core.agda )
Checking Data.Empty ( /Users/godfat/projects/Agda/std-lib/Data/Empty.agda )
Checking Relation.Binary.PropositionalEquality ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/PropositionalEquality.agda )
Checking Relation.Binary ( /Users/godfat/projects/Agda/std-lib/Relation/Binary.agda )
Checking Data.Sum ( /Users/godfat/projects/Agda/std-lib/Data/Sum.agda )
Checking Relation.Binary.PropositionalEquality.Core ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/PropositionalEquality/Core.agda )
Checking Relation.Binary.Core ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/Core.agda )
Checking Relation.Binary.Consequences.Core ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/Consequences/Core.agda )
Checking Relation.Binary.Consequences ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/Consequences.agda )
Checking Relation.Binary.FunctionLifting ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/FunctionLifting.agda )
Checking Relation.Binary.EqReasoning ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/EqReasoning.agda )
Checking Relation.Binary.PreorderReasoning ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/PreorderReasoning.agda )
Checking Data.List ( /Users/godfat/projects/Agda/std-lib/Data/List.agda )
Checking Data.Nat ( /Users/godfat/projects/Agda/std-lib/Data/Nat.agda )
Checking Relation.Nullary ( /Users/godfat/projects/Agda/std-lib/Relation/Nullary.agda )
Checking Data.Bool ( /Users/godfat/projects/Agda/std-lib/Data/Bool.agda )
Checking Data.Unit ( /Users/godfat/projects/Agda/std-lib/Data/Unit.agda )
Checking Category.Monad ( /Users/godfat/projects/Agda/std-lib/Category/Monad.agda )
Checking Category.Monad.Indexed ( /Users/godfat/projects/Agda/std-lib/Category/Monad/Indexed.agda )
Checking Category.Applicative.Indexed ( /Users/godfat/projects/Agda/std-lib/Category/Applicative/Indexed.agda )
Checking Category.Functor ( /Users/godfat/projects/Agda/std-lib/Category/Functor.agda )
Checking Relation.Binary.PartialOrderReasoning ( /Users/godfat/projects/Agda/std-lib/Relation/Binary/PartialOrderReasoning.agda )
Checking Data.Maybe ( /Users/godfat/projects/Agda/std-lib/Data/Maybe.agda )
Checking Algebra ( /Users/godfat/projects/Agda/std-lib/Algebra.agda )
Checking Algebra.FunctionProperties ( /Users/godfat/projects/Agda/std-lib/Algebra/FunctionProperties.agda )
Checking Algebra.Structures ( /Users/godfat/projects/Agda/std-lib/Algebra/Structures.agda )
Checking Data.Nat.Properties ( /Users/godfat/projects/Agda/std-lib/Data/Nat/Properties.agda )
Checking Algebra.RingSolver.Simple ( /Users/godfat/projects/Agda/std-lib/Algebra/RingSolver/Simple.agda )
Checking Algebra.RingSolver.AlmostCommutativeRing ( /Users/godfat/projects/Agda/std-lib/Algebra/RingSolver/AlmostCommutativeRing.agda )
Checking Algebra.Morphism ( /Users/godfat/projects/Agda/std-lib/Algebra/Morphism.agda )
Checking Algebra.Props.Ring ( /Users/godfat/projects/Agda/std-lib/Algebra/Props/Ring.agda )
Checking Algebra.Props.AbelianGroup ( /Users/godfat/projects/Agda/std-lib/Algebra/Props/AbelianGroup.agda )
Checking Algebra.RingSolver ( /Users/godfat/projects/Agda/std-lib/Algebra/RingSolver.agda )
Checking Algebra.RingSolver.Lemmas ( /Users/godfat/projects/Agda/std-lib/Algebra/RingSolver/Lemmas.agda )
Checking Algebra.Operations ( /Users/godfat/projects/Agda/std-lib/Algebra/Operations.agda )
Checking Data.Fin ( /Users/godfat/projects/Agda/std-lib/Data/Fin.agda )
Checking Data.Vec ( /Users/godfat/projects/Agda/std-lib/Data/Vec.agda )
Checking Data.List.NonEmpty ( /Users/godfat/projects/Agda/std-lib/Data/List/NonEmpty.agda )
godfat ~/p/Agda>

都過了！看來應該正常可用，可喜可賀，可喜可賀。
不過我不想灌 emacs mode orz 實在跟 emacs 相性不太合....

禁止餵食

日期分類

標籤分類

星之一角

2008-11-28

happy 灌不起來真不 happy (2)

2 retries:

Post a Comment

favorite albums