Error: The file ssreflect.vo contains library ssreflect and not library theories.ssreflect

After installing ssreflect, its libraries for Coq are installed in /usr/local/lib/coq/user-contrib/theories. When ever I want to import libraries of ssreflect in CoqIDE (ssrcoqide), I get the following error messages:

Error: The file /usr/local/lib/coq/user-contrib/theories/ssreflect.vo
  contains library ssreflect and not library theories.ssreflect
Error: The file /usr/local/lib/coq/user-contrib/theories/eqtype.vo
  contains library eqtype and not library theories.eqtype
......

There are two ways to solve this problem.  I don't know which one is better.

Method 1

Move all the ssreflect libraries for Coq from /usr/local/lib/coq/user-contrib/theories to /usr/local/lib/coq/user-contrib.

Method 2

Add "-I /usr/local/lib/coq/user-contrib/theories" to launch ssrcoq and ssrcoqide. Actually, I rename ssrcoq and ssrcoqide to ssrcoq.opt and ssrcoqide.opt respectively, and use the following two scripts to launch them.

The script /usr/local/bin/ssrcoq:

#!/bin/bash

/usr/local/bin/ssrcoq.opt -I /usr/local/lib/coq/user-contrib/theories $*

The script /usr/local/bin/ssrcoqide:

#!/bin/bash

/usr/local/bin/ssrcoqide.opt -I /usr/local/lib/coq/user-contrib/theories $*

Failed to Install camlp5 in Gentoo Linux - "make inconsistent assumptions over implementation Pretty"

When I use emerge to install camlp5-5.14 with ocaml-3.11.2 (or camlp5-5.12 with ocaml-3.10.2) and with ocamlopt enabled in Gentoo Linux, I get the following error message:

File "_none_", line 1, characters 0-1:
Error: Files prtools.cmx and ../lib/pretty.cmx
       make inconsistent assumptions over implementation Pretty

To solve this problem, I temporarily move /usr/lib/ocaml/pretty.cmx to some other place (or rename it). Don't forget to move the file back after camlp5 is installed successfully.

Added on 2010/11/29: I found the reason. The error message occurs because I installed the libraries of CIL in /usr/lib/ocaml by a self-written ebuild file. To prevent this error every time upgrading camlp5, I should install the CIL libraries in a separate folder.

L2TP IPSec VPN + NAT on Gentoo Linux with Single Network Adapter

This article describes how I setup an NAT server and an L2TP IPSec VPN server on Gentoo Linux with only one network adapter. Assume

• 12.34.56.78 is the public IP of the server,
• 12.34.56.1 is the gateway of the server,
• 192.168.0.1 is the private IP of the server, and
• 192.168.0.0/24 is the internal network.

華南銀行 Lite in NTU

話說一月中去巴黎、馬德里的航班是晚上，當天早上想多補一些歐元，於是到了離實驗室最近的銀行：華南銀行。當時的對話大約如下：

『先生，不好意思喔，現在買的話要晚上六點才能拿。』

『阿，為甚麼？』

『我們這邊沒有歐元，要從別的分行調過來。』

恩，晚上要拿的話還得特地拖著行李走過來拿，算了，我去別的地方換吧。

從馬德里回來以後，發現我當初顧慮太多了，結果歐元剩一堆。剛剛想去 7-11 買吃的，順道再去華南銀行賣看看，沒有歐元庫存，總該有台幣可以把歐元買回去吧。

『先生，我先看看您要賣的幣值......不好意思喔，我們這邊不收 20 元的。我們這邊只賣 50 元跟 10 元的，您當初不是在我們這邊買的吧？』

『是阿，我是在別的地方買的，不過都有收 50 元跟 10 元，竟然沒有 20 元的！？』

太低的幣值不收我可以理解，不過 10 元都收了，怎麼不收 20 元的。更何況賣 50 元給客人，也有可能出國花一花找回來 20 元的阿。

就這樣去了華南銀行兩次，兩次都是碰釘子回來，心裡只覺得台大裡面的華南銀行還真像是 AppStore 裡面那些 Lite 版應用程式。恩，我的 iPhone 上那些 Lite 版應用程式好像都是嘗鮮玩一兩下就刪除了。

JCBR: Java Chinese Book Reader

Name: JCBR (Java Chinese Book Reader)

Latest Version: 0.8.0

Platform: Mac OS X, Windows (since 0.8.0), Linux (since 0.8.0)

Supported Files: PDB, uPDB

Download: 0.8.1 Mac, 0.8.1 Windows/Linux

Note: This application is specially for eBooks made by mPDB.
Previous Versions: 0.6, 0.6.1, 0.7.0, 0.8.0 Mac, 0.8.0 Windows/Linux

JCBR 是最近寫的一個中文直式閱讀軟體，目前作業系統僅支援 Mac OS X ，而檔案格式僅支援由 mPDB 所製作的 PDB/uPDB 檔案。為什麼要寫這個軟體呢？由於本人一直很喜歡看武俠小說，前不久正好發現 iPhone 上的一個免費電子書軟體：cBook Lite ，透過這個軟體又發現了好讀網站。好讀網站上除了電子書以外，還有好用的中文電子書製作軟體 mPDB 與直式閱讀軟體。這些閱讀軟體有 Windows 版、WinCE 版、Palm 版、SONY CLIE 版、網頁版、iPhone 版與 Andriod 版，雖然有這麼多平台的閱讀軟體，但其中就是少了 Mac OS 。這對上個星期狠心買下 MacBook Pro 的我來說便造成一點困擾。於是花了點時間來為 Mac 寫一個對我來說還算堪用的直式閱讀軟體。

2009.08.21-2009.08.24 台東之旅 - 羅山、六十石山、小野柳

8/23 早上，一樓大廳擺著民宿主人買來的三明治早餐，雖然不是民宿主人自己做的，不過也省了我們到市區買早餐的時間。今天的第一站是距離民宿約 70 公里的花蓮縣富里鄉羅山泥火山（剛剛才知道原來這裡已經到花蓮了），在這漫漫長路上，我只覺得一直被後面的車超車，明明我都已經開到速限了......。從台九線轉景坪產業道路（路口有寫羅山遊憩區），開了一段山路後終於抵達羅山泥火山所在地。

在泥火山前是一個相當大的鯉魚池，池旁有一超小型停車場，大概可以停個六七台車吧。我們剛到沒多久，就看到一票人走出來，瞬間這邊的遊客就剩下我們兩人。

2009.08.21-2009.08.24 台東之旅 - 初鹿牧場、鹿野高台

其實本來只打算在台東待兩天的，不過太晚訂票，出發跟回來的時間都不太好，只好往前往後各延一天。雖然說這一趟台東之旅是從 8/21 到 8/24 ，扣掉晚上才到台東的 8/21 ， 8/22 笨笨要上班的早上，以及 8/24 離開台東的一大早，實際上能玩的時間只有一天半。感覺這一天半裡面有一半的時間都在開車......。

8/22 原本的計畫是騎噗噗先去初鹿牧場，晚上再到民宿 Check in ，因為 Check in 的時間是在下午三點以後。不過中午笨笨上完班回來以後，民宿的老闆娘就打電話過來請我們去 Check in （笨笨說老闆娘怕我們跑掉不去住了）。討論一下之後，決定改變原先的計畫，租一天半的車，先去民宿，然後再出去玩。

租車的地點是新生路的明美租車，因為笨笨的學長認識老闆，所以可以算我們便宜一點。剛上車時，我還搞不清楚怎麼調整座位，結果老闆又過來指點一二，順便教我怎麼開冷氣跟收音機。看到我這個開車經驗屈指可數的客人，不知道老闆會不會擔心他的車。