科学者をやっていると、
いや、
やればやるほど
わからないことに遭遇する。
研究という仕事に限らず、
無論、
ソクラテスの言葉「無知の知」のような高尚な話ではなく、
日常の何気ないことでも
自分の知性や理解の浅はかさに嘆くときがある。
最近だと、酔わないウメッシュのCMがわからない。
どこに向かっているのかわからない。
https://youtu.be/klHx0EZSozo
これはバンド編。
編で終わるからには他のものもある。
https://youtu.be/HGF4pVsvTEs
こちらはデュオ編。
さらにミュージックビデオ
「ワタシは酔わない」なんてのもある。
歌詞の冒頭は
「You Wanna 酔わないウメッシュ」
こういうのをガデムモーター超フル回転と言うのだろうか。
混乱した為かわからないが、最近寝ぼけて、
妻のお尻のにおいをかいだ。
この話はまた今度。
Coq 8.5が公式にリリースされました。
そして、Windows版の SSReflect, MathComp もリリースされました。
早速インストール＆動作確認しました。
基本的にはインストーラをクリックするだけなのですが、
ノウハウとして
入手方法やインストールの方法を
メモしておきます。
気を付けることは、
これまでに Coq と SSReflect, MathComp をインストールしていた場合、
・アンインストールをする
もしくは
・これまでのCoqとは異なるフォルダに
新しい Coq 8.5 をインストールする
ということです。
◆Coq 8.5の入手方法とインストール
Windows版は 32ビット版と64ビット版の二つのインストーラが提供されました。
２０１６年１月２２日現在では、どちらも
https://coq.inria.fr/download
から入手可能です。
ここからインストーラをダウンロードして、起動します。
あとはインストーラの指示に従うだけでOKです。
途中でインストール先を選択する画面が現れます。
上に述べましたが、
もしも他のバージョンの Coq が既にインストールされていたら、
・それらをアンインストールする
もしくは
・Coq 8.5 を他のCoqとは異なるフォルダにインストールする
のどちらかにすると良いでしょう。
◆SSReflect/MathCompの入手方法とインストール
Windows版 Coq 8.5 をインストーラからインストールした場合、
SSReflectやMathCompのバージョンは 1.6 を使うことになります。
こちらにもWindows版インストーラが用意されています。
下のURIからダウンロードできます。
http://ssr.msr-inria.inria.fr/FTP/
インストーラは３２ビット版と６４ビット版の両方が提供されています。
それぞれ
ssreflect-mathcomp-installer-1.6-win32.exe
ssreflect-mathcomp-installer-1.6-win64.exe
という名前がつけられています。
先のURIの先にあるHPの下の方にあります。
インストールはインストーラをクリックするだけでできます。
途中でインストール先を選択する画面が現れます。
その際には、Coq 8.5で指定したディレクトリ名をそのまま指定してください。
以上でインストールは終わりです。
◆動作確認
Coqを起動するには
スタートメニューなどから
CoqIDE
を選んでください。
SSReflect/MathCompを読み込むには
CoqIDEのスクリプトエリアに
From mathcomp
Require Import ssreflect.
と入力し、CoqIDEの一行読み込みボタンをクリックしてください。
上部にあるアイコンのうち、左から３番目の ↓ のことです。
入力した上の２行「From … ssreflect.」が緑色に変われば
正しく動作しています。
年明けは紅白の恵比寿ビールでめでたさ一杯に過ごした
萩原です。
おはようございます。
前回のブログで、今年の目標を書きました。
早速、１つ、進展しました。
論文１編、アクセプトの連絡を受け取りました。
ありがてぇ。
本当にありがてぇ。
そんな喜びの中、新年会を開催しました。
千葉大理学部数学科の同級生たちと。
つまり、９３年４月～９７年３月の間、
キャンパスライフを共にした仲間たち。
さらに、当時、線形代数の講義をしてくださった教員も。
それがこの写真！
ババーン！！
同級生と教員で飲む楽しさ。
とにかく、笑いまくりました。
楽しかった。
ちなみに、当時お世話になった教員は一番右です。
あとは同級生です。
さて、話は変わって、
娘の話でも。
長女は４歳、次女は２歳。
まぁ、ふてぶてしいものです。
ほら。
二人とも。
ほら。
ところで最近、
長女（まりな、４歳）の数字好きが頭角を現してきました。
登りながら階段を数えたり、
本に出てくるキャラクターを数えたり。
時々、足し算や引き算のような問題を楽しむことも。
そんな長女が、私に問題を出してきました。
まりな「パパ、問題だよ」
わたし「はい、どうぞ」
まりな「スカイツリーが８個あります」
わたし どうして、そんなに沢山あるんだ？
まりな「２個なくなりました。
いくつになったでしょう」
わたし「なんでなくなったの？」
まりな「そんなことは聞いてません」
わたし「６個」
まりな「正解です」
わたし「なんで８個もあって、２個なくなったの？」
まりな「次の問題です」
