/*********************************/
/*                               */
/*    この通りにやることぉ！     */
/*                               */
/*********************************/

☆Isabelle/HOLを動かすのじゃ☆

♪環境変数設定を設定する。
  export SMLNJ_CYGWIN_RUNTIME=1
　もしくは/etc/profileに↑を書いとく

♪インストール先を指定（デフォルトの場合）
  mkdir /opt
  d=/opt/smlnj
  mkdir $d
  cd $d

♪SMLNJのソースファイルを取ってくる。
  wget http://smlnj.cs.uchicago.edu/dist/working/110.57/config.tgz

♪解凍する
  tar -C ./ -zxf config.tgz
 ---------もしくは-----------------
  gunzip <config.tgz | tar xf -
 ----------------------------------

♪実行する（/opt/smlnjへインストール）
  config/install.sh
  （補足）こいつはpwdでカレントディレクトリを取得し、
  　　　　そこへインストールしようとする。
          'pwd'のところを'/bin/'に書き換えることで標準インストールも可

♪解凍するだけ（イザベルのファイルは自分で取ってきて）
  tar -C /opt -xvzf Isabelle2005.tar.gz 
  tar -C /opt -xvzf ProofGeneral.tar.gz

♪コメント(#<-これ)を外す
  # Standard ML of New Jersey 110 or later
  SMLNJ_CYGWIN_RUNTIME=1
  ML_SYSTEM=smlnj-110
  ML_HOME="/opt/smlnj/bin"
  ML_OPTIONS="@SMLdebug=/dev/null"
  ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
♪ビルドする(めっちゃ時間かかる）
  cd /opt/Isabelle 
  build FOL (約2分56秒　P4_2.8G）
  build ZF (約2分17秒　P4_2.8G）
  build HOL (約7分26秒　P4_2.8G）
  （補足）ZFは集合論の公理系、FOLは一階論理？の公理系、HOLは高階論理の公理系
  　　　　ただ、ほとんどHOLしか使わない。

♪パスの設定(いちいち長いPATHを入力するのがイヤなんで）
  /etc/profileのここを
  PATH=/usr/local/bin:/usr/bin:/bin:/usr/X11R6/bin:$PATH
  export PATH
  こんな感じに書き換えてPATHを追加☆
  PATH=/usr/local/bin:/usr/bin:/bin:/usr/X11R6/bin:/opt/Isabelle2005/bin:$PATH
  export PATH

♪実行する（これをやんないとXモードで起動しない）
  startxwin.sh

♪出てきたウィンドウで・・・
  /opt/Isabelle/bin/isabelle-interface &

♪XSymbolsの設定
  Proof-General->Options->Xsymbol
  にチェックをつけて
  Proof-General->Options->Save Options

♪終了＾＾ｖおめでとーーーー！！

補足：
  http://cygwin-je.sourceforge.jp
  CYGWIN日本語パッケージ

X-Symbolのサイズ変更
  C:\cygwin\opt\ProofGeneral-3.6pre050930\isar\interface
  XSYMBOL_FONTSIZE="24"

快速X-Window起動
  次のシェルを作る
  file name: xwin------------------------
  #!/bin/bash

  startxwin.sh
  --------------------------------------


快速イザベル起動
  次のシェルを作る
  file name: isa------------------------
  #!/bin/bash

  /opt/Isabelle/bin/isabelle-interface &
  --------------------------------------

♪PDFドキュメントの作り方
  isatool mkdir フォルダの名前

 フォルダが生成されるのでその中のROOT.MLファイルに 
 証明したいTheoryの名前を書き込む。
 たとえば、Message.thyならば。。
 ---ROOT.ML----------------------------
 use_thy "Message";
 (*コメント*)
 --------------------------------------
 PDF化したくない場合はno_document use_thyを使う。
isatool make