Installation of Agda2 under Windows ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Files containing additional information for packages and other programs: darcsinstallPublicParts.txt cabalPublicParts.txt perlwindowsinstallPublicParts.txt alexindowsinstallPublicParts.txt happywindowsinstallPublicParts.txt binaryhaskellwindowsinstallPublicParts.txt zlibhaskellwindowsinstallPublicParts.txt Limitations: The emacs version was installed. I didn't succeed yet in installing the agda program which can be run from the commandshell. I didn't succeed in installing the fonts in emacs, so only a few special symbols are available. I installed darcs (This is not necessary - one can use darcs under linux and move the files from there) Note that the latest built version I used are available from my website. However it is recommended to get the latest version using darcs, which might contain bug fixes. I got from the website of darcs the windows version. I moved it to a directory C:\Program Files\darcs I extracted it there. There are instructions for darcs configuration on the website. I added the path to darcs.exe to the path Control Panel -> System -> Advanced -> Environement Properties -> User Variables -> Path I didn't look at darcs via ssh yet I installed ghc using the windows installer from the website (easy). I needed perl (for compiling alex and happy), and installed active perl (see the file perlwindowsinstallPublicParts.txt) I got alex, and used the source distribution. (see as well the file alexindowsinstallPublicParts.txt) I then did the cabal installation runghc Setup.lhs configure runghc Setup.lhs build runghc Setup.lhs install (if one wants to install the binaries somewhere else, use runghc Setup.lhs --user --prefix=D:\ProgramFilesLinuxLike\Haskell (with the path D:\ProgramFilesLinuxLike\Haskell replaced by whatever one wants) But then one has to add D:\ProgramFilesLinuxLike\Haskell\bin to the path. The same applies to all cabal installation commands below (happy, binary,zlib,quickcheck,agda) I got happy, and used the source distribution. I then did the cabal thing (see as well happywindowsinstallPublicParts.txt) runghc Setup.lhs configure runghc Setup.lhs build runghc Setup.lhs install I got binary from (See as well binaryhaskellwindowsinstallPublicParts.txt) http://hackage.haskell.org/cgi-bin/hackage-scripts/package/binary-0.4.1 I copied it to a directory C:/Program Files/binary-haskell I used cygwin to unpack it (tar xvfz - if you don't have cygwin, to this from a windows machine, and move the directory to that place) Then I went to that directory and from a command shell (use runcommand from Startup menu and then Cmd) I went to there and didd the cabal thing: runghc Setup.lhs configure runghc Setup.lhs build runghc Setup.lhs install I got zlib from http://hackage.haskell.org/cgi-bin/hackage-scripts/package/zlib-0.4.0.1 (See as well zlibhaskellwindowsinstallPublicParts.txt) I copied it to a directory C:/Program Files/zlib-haskellpackage I used cygwin to unpack it (tar xvfz - if you don't have cygwin, to this from a windows machine, and move the directory to that place) Then I went to that directory and from a command shell (use runcommand from Startup menu and then Cmd) I went to there and didd the cabal thing: runghc Setup.hs configure runghc Setup.hs build runghc Setup.hs install Then I got agda2 using darcs get http://www.cs.chalmers.se/~ulfn/darcs/Agda2 I went to the directory and did the cabal thing runhaskell Setup.hs configure runhaskell Setup.hs build runhaskell Setup.hs install Then i tried the same (for getting the stand alone utility) from /src/main but that didn't work, because readline was missing. Attempt to solve the problem (failed) (One can provisionally live without carrying out this step: the only purpose of this step is to create a program agda.exe which allows to run agda from the command shell and allows to get a complete list of errors and warnings. For developing Agda proofs in Emacs, this step is not required, however one has to be careful not to overlook any warnings generated by the termination checker.) I went to http://gnuwin32.sourceforge.net/packages/readline.htm which had a link to the GnuWin32 files page (http://sourceforge.net/project/showfiles.php?group_id=23617&package_id=146819) From there I got an installer which I used But that didn't solve the problem, I got the same error message as before. End of failed attempt Next, as recommended in the Agda README file, I installed NTEMacs I downloaded from http://ntemacs.sourceforge.net/ the self-extracting executable ntemacs22-bin-20070819.exe The installation of additional fonts didn't work. We can avoid this by not using any special fonts. For how far I got on installing the fonts see the instructions on installing fonts at the end. Next I got the haskell-mode from http://haskell.org/haskell-mode/ untared it (using a linux machine or cygwin) and moved it to C:/ProgramFilesLinuxLike/myEmacsElisp/agdaByDate/2008/agdaJan2008/haskell-mode-2.4 Then I copied the .el files in Agda2/src/full/Interaction/emacs-mode (which is in C:/Program Files/agda2 in my installation) to C:/ProgramFilesLinuxLike/myEmacsElisp/agdaByDate/2008/agdaJan2008/ Then I created in emacs a file C:/ProgramFilesLinuxLike/myEmacsElisp/agdaByDate/2008/agdaJan2008/agdainstall.el to which I added (the paths C:/ProgramFilesLinuxLike/myEmacsElisp/agdaByDate/2008/agdaJan2008/ refer to where I have moved the .el files) (add-to-list 'load-path "C:/ProgramFilesLinuxLike/myEmacsElisp/agdaByDate/2008/agdaJan2008/") (add-to-list 'load-path "C:/ProgramFilesLinuxLike/myEmacsElisp/agdaByDate/2008/agdaJan2008/haskell-mode-2.4/") (autoload 'agda2-mode "agda2-mode" "Agda2 mode." t) (add-to-list 'auto-mode-alist '("\\.l?agda$" . agda2-mode)) (modify-coding-system-alist 'file "\\.l?agda$" 'utf-8) (add-hook 'agda2-mode-hook '(lambda nil (require 'quail) (set-input-method 'TeX) )) Since there is a problem with the fonts I modified the file C:/ProgramFilesLinuxLike/myEmacsElisp/agdaByDate/2008/agdaJan2008/agda2-mode.el as follows I modified the lines (defcustom agda2-fontset-spec (concat "-misc-fixed-medium-r-normal-*-15-*-*-*-*-*-fontset-agda2" (cond ((eq window-system 'x) "") ((eq window-system 'w32) ", ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1, to (defcustom agda2-fontset-spec (concat "-misc-fixed-medium-r-normal-*-15-*-*-*-*-*-fontset-agda2" (cond ((eq window-system 'x) "") ((eq window-system 'w32) "") ((eq window-system 'w32tmp) ", ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1, This has the effect that if the windows-system is w32, then the font set is set to "" (so no mule-fonts are set) and if the windows system is w32tmp (which doesn't exist) then the fonts are set to what it was originally -- effectively the 'w32 case is commented out. Now it works, except that special symbols like \Nbb, \alpha don't work Installing fonts for emacs ~~~~~~~~~~~~~~~~~~~~~~~~~~ The following almost worked. The problem was that there was no directory mule-fonts/packages/fonts/bitmap when downloading mule-fonts below. I created a directory C:/ProgramFilesLinuxLike so that I have a directory with no blanks, which under Linux creates a problem sometimes. Then I downloaded from http://www.cl.cam.ac.uk/~mgk25/ucs-fonts.html the tar file http://www.cl.cam.ac.uk/~mgk25/download/ucs-fonts.tar.gz to a linux machine (since we need to run make on it) There I created a directory ucs-fonts (somewhere) Then I moved the package into it. Then I unpacked it (using tar xvfz ucs-fonts.tar.gz) then I went to the directory submission cd submission And then I did make all-bdfs As said in the README file of agda, I ignored error messages about missing fonts. Then I moved this directory to n windows to C:/ProgramFilesLinuxLike/ucs-fonts/ (e.g. by doing under linux zip -r ucs-fonts.zip ucs-fonts and then moving the zip file to windows and unpacking it there but one can move the whole directory directly using winscp or a usb-stick) It turned out that I actually got the directory structure C:/ProgramFilesLinuxLike/ucs-fonts/ucs-fonts/ucs-fonts/submission and removed the intermediate ucs-fonts so that I had the structure C:/ProgramFilesLinuxLike/ucs-fonts/submission Then I downloaded under linux (because I don't have bunzip2 there) http://www.meadowy.org/meadow/dists/3.00/packages/mule-fonts-1.0-4-pkg.tar.bz2 There I created a directory mule-fonts (somewhere) moved the package into it I applied bunzip2 there bunzip2 mule-fonts-1.0-4-pkg.tar.bz2 and untarred it tar xvf mule-fonts-1.0-4-pkg.tar and moved the directory mule-fonts to windows C:/ProgramFilesLinuxLike/mule-fonts So the directory structure should look like this C:/ProgramFilesLinuxLike/mule-fonts/packages/ Then I opened the .emacs file which I got by under windows doing C-x C-f ~/.emacs (the file is located in C:/Documents and Settings/Csetzer/Application Data/ As recommended in the README file of agda2 I added the following to this file (If you had a different directories for ucs-fonts, mule-fonts, just make sue that the path in the first command point to directories within ucs-fonts and mule-fonts (setq bdf-directory-list '( "c:/ProgramFilesLinuxLike/ucs-fonts/submission" "c:/ProgramFilesLinuxLike/mule-fonts/packages/fonts/intlfonts" "c:/ProgramFilesLinuxLike/mule-fonts/packages/fonts/efonts" "c:/ProgramFilesLinuxLike/mule-fonts/packages/fonts/bitmap" "c:/ProgramFilesLinuxLike/mule-fonts/packages/fonts/CDAC" "c:/ProgramFilesLinuxLike/mule-fonts/packages/fonts/AkrutiFreeFonts" )) (setq w32-bdf-filename-alist (w32-find-bdf-fonts bdf-directory-list)) (create-fontset-from-fontset-spec "-*-fixed-Medium-r-Normal-*-15-*-*-*-c-*-fontset-bdf, ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1, latin-iso8859-2:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-2, latin-iso8859-3:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-3, latin-iso8859-4:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-4, cyrillic-iso8859-5:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-5, greek-iso8859-7:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-7, latin-iso8859-9:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-9, mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, japanese-jisx0208:-JIS-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0208.1983-0, japanese-jisx0208-1978:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISC6226.1978-0, japanese-jisx0212:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0212.1990-0, latin-jisx0201:-*-*-medium-r-normal-*-16-*-*-*-c-*-jisx0201*-*, katakana-jisx0201:-Sony-Fixed-Medium-R-Normal--16-120-100-100-C-80-JISX0201.1976-0, thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1, lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1, tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0, tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1, korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0, chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0, chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0, chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0, chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0 " t) (setq font-encoding-alist (append '( ("JISX0208" (japanese-jisx0208 . 0)) ("JISX0212" (japanese-jisx0212 . 0)) ("CNS11643.1992.1-0" (chinese-cns11643-1 . 0)) ("GB2312" (chinese-gb2312 . 0)) ("KSC5601" (korean-ksc5601 . 0)) ("VISCII" (vietnamese-viscii-lower . 0)) ("MuleArabic-0" (arabic-digit . 0)) ("MuleArabic-1" (arabic-1-column . 0)) ("MuleArabic-2" (arabic-2-column . 0)) ("muleindian-1" (indian-1-column . 0)) ("muleindian-2" (indian-2-column . 0)) ("MuleTibetan-0" (tibetan . 0)) ("MuleTibetan-1" (tibetan-1-column . 0)) ) font-encoding-alist)) ;;;;;;; end of quoted elisp code I tested it by executing in Emacs M-x eval-expression RET (set-default-font "fontset-bdf") RET M-x view-hello-file And noticed that there were boxes for most special characters