What have you found for these years?

2008-11-28

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 相性不太合....

2 retries:

Josh Ko said...

欸,可是用 emacs mode 和用 Agda-executable 的生產力差距非常地大,足以改變對於 Agda 的觀感…

godfat 真常 said...

那... 明天再來灌灌看吧 @@
如果熟悉了神的編輯器,或許能躍升為神 XD

Post a Comment

All texts are licensed under CC Attribution 3.0