Home > Archives > 2012年10月

2012年10月

今日も再び

移動中は論文修正と技術的なポイントの改善とかで…… 海外パケホが便利だなぁと感じる今日この頃.まぁ,1日3千円ってのはちと高いのだけど.

明日も頑張ってですまーち.

モンサンミッシェル、水位比較

ちょうど同じ辺りで撮影した写真を発見したので比較.水位が低い方は満潮の4時間半前で,高い方は満潮から1時間過ぎた頃だけど,それでもだいぶ違うもんだなぁ.

http://www.ot-montsaintmichel.com/en/horaire-marees/mont-saint-michel.htm によると31日の朝の水位は 12.80m で,2週間前の新月の時には14.00mとあるから,写真からさらに1.2mも水位が上がるってことか.やっぱ新月時にもう一回行かないとダメだな.

モンサンミッシェル、朝

モンサンミッシェル朝バージョン.方角的にあんまり朝焼けしてないので残念.モンサンミッシェルを東ないし西に見られる位置で構えられないとダメだなぁ.

水逆流中.

日の出.

モンサンミッシェルの縁まで水が来ているの図.

辛うじて道以外が水に囲まれていることを確認できるの図.

入り口.地面の濡れ具合からして昨日の夜と同じくらいか? 夜だと暗いので朝に観察するのが良い気がする.次回は中のホテルにでも泊まろうかね.

そして8時半過ぎくらいなのでガラガラ.でもこの直後に日本のツアー団体が大挙して来て…… 落ち着いて見て回るには早朝の散歩が良い気がする.

んで,お帰りはバスでレンヌに行ってそこからTGVで.帰りのバスは 12.10ユーロを現金で払って乗れた.

閑話休題.

レンヌと Dol de Bretagne 以外にも Pontorson と行き来するバスがあるらしく,こいつは1回2ユーロで乗れるっぽいし本数も多くわずか20分で駅につくらしい.ひょっとすると電車で Pontorson まで頑張るってのも有りかもしれない.電車の本数が有るかどうかわからんけど.とりあえずバックパッカーの人達が利用してた.つか,この駅までは歩けない距離でもないな……

5年ぶりにモンサンミッシェルへ

TGVでRennesまで行ってそこからバスで.とりあえず午後1時くらいに到着.もう少し良い天気だと良かったのだけど.

相変わらずの狭さと込み具合.そしてなにげに登りなのでダウンしている人もいたり.

修道院のなか.入り口の待ち行列がとても長かった…… グループで入れると楽なのかもしれない.

中庭の柱.交互になってるのが面白い.

んで中庭.季節的にちょっと残念なのだろうか? 天気が良ければもっと違う印象なのかも.

石造りの柱と螺旋階段.

外に出てきて工事中を眺める.

ホテル Le Relais Du Roy の部屋より.一応モンサンミッシェルが見える.どこぞのホテルの半額で泊まれて場所も悪くない.エレベーターも無いけど.

ホテルから見えた橋の上より.ライトアップ+夜の一歩手前の深い青ってのを撮り直したくて来たのだけど,水面への反射も入って良い感じ.三脚が弱くて歩留まりが悪いのが残念だったりするけれど.とりあえずモンサンミッシェルを右に寄せてトリミングして壁紙にした.

あとは19:17の満潮でどの程度まで水が来るのかを確認するためにモンサンミッシェルまでテクテクと歩きつつ途中で撮ったり.


まあ,結局入口に続く桟橋のすぐ手前まで水が来る程度だったので,やっぱり新月の時にくるのがよろしいと思われる.

ホテルから見える橋まで戻ってきて再び.やっぱり真っ暗より濃い青がバックのほうが好ましいよねとか思いつつ本日の撮影終了.

閑話休題.

TGVが往復で160.20ユーロ,パリのメトロが3.4ユーロ,バス代が往復で24.20ユーロ,ホテルが99.50ユーロ,合計で300ユーロ弱の旅.結構掛かるもんだなぁ.TGVをだいぶ前に買っておけばもっと安いのかね.

閑話休題.

チケットをバスで買えるかなぁとか思って試してみたのだけど,モンサンミッシェル行きのバスのチケットはチケット売り場で買えと言われた.たぶん,帰りのチケットはバスで買うに違いない.

閑話休題.

つーか日本人多すぎ.

うぼあ

共著論文の出来があまりにも悪すぎるので現実逃避にモンサンミッシェルへお出かけしつつ電車とバスの中で周りの目をきにせずセコセコ論文を直す一日.大学がお休みでプリンターが使えないので効率が悪い.もう一人の共著者が忙しすぎてノータッチになるとか想定外だよなぁ.

あー,締め切りまで後2日.

でぃなぁ

教授のお家の夕食会にお呼ばれしてきた.まあフランス語全然わからんな.とりあえず Bon Appétit がボキャブラリーに追加されたけど.

閑話休題.

日本語は会話は分かりやすいが読み書きは無理だよねぇ漢字的に,という話が出た.たしかに漢字の読み書きは日本人でさえ小学校で6年間きっちりとやるわけだし,単語一つ一つに図が対応しているようなもんだから面倒この上ないよね.常用漢字で2千ちょっとあるっぽいし(読みはその倍).……1日に1つで6年なのか.

一日動けない

体が冷えきって筋肉が緊張した状態でくしゃみしたせいか,肩というか首の付根というか背中というかの筋を痛めたっぽい.とりあえず寝返りを打てない.起き上がるのも一苦労.

ということで昼間は動かずじっとしているしかない一日だった.

閑話休題.

サマータイムが終わるので時刻の変化を観測しようと未明に時計を表示しているテレビ番組を見ていたのだけど…… その番組の時計は2:59の次に3:00になってしまった.その1分後には3:01で.確認のために他のチャンネルに変えたら 2:01 だったのに.観測するチャンネルの選択に失敗した.残念.

とりあえず携帯の時計は勝手に2時を繰り返していた.そして腕時計は勝手に直ってはくれない.

天気が良いのでお出かけ

明日から1時間遅くなるし,せっかくなので早朝のエッフェル塔を見ようと朝5時の電車でパリへ出発.

んで,未明のエッフェル塔のどアップ.東京タワーと違って重たい色なので重量感があっていいと思う.

橋を渡ってシャイヨ宮に移動したところで明け方のエッフェル塔.今日はとても良く晴れてて運が良かった.7時過ぎとはいえまだ暗いしすごく寒いのにちらほら人が来て写真を撮っていたのには驚いた.

そして寒すぎて1時間待機してギブアップ.日の出は拝まずルーブル美術館の地下の開館待ち行列に並んだ.

とりあえず今日も安定して賑わうモナリザ.

金ピカになってる誰もいないアポロンギャラリー.前回は失敗したが今回は混む前に行けた.

そして撮ってる間に人がちらほらきてここらでギブアップ.

最後にニケを ISO200 で撮るオペレーション.混んでるところに露光時間が長いから1時間くらい粘った気がする.その間に幽霊が通ったような写真を大量に生成し,幽霊無しは1枚しか撮れなかった.また今度の機会にチャレンジしよう.

閑話休題.

せっかくなのでユーロコインを錬成しようかと20ユーロ札で切符を買ったら1ユーロコインが18枚出て残念な気分.2ユーロが9枚だと思ってたのに……

ひと仕事した

幾つかの大学から近めの研究グループが集まって発表しあうローカルなワークショップにお呼ばれして研究の発表をしてきた.ぶっちゃけ「関係のない○○ですが,突然発表します」みたいなノリで.基本的にみんなフランス語で発表するのだけど,私が参加していたせいで何人かが英語で発表してくれたりしてちょっと申し訳ない気分.でも色々とコメントもらえたりして非常にありがたい機会だった.

閑話休題.

参加者のドイツ人にいててお昼時に話をしたので,ついでに俺のドイツ語をチェックしたいんだけどとか言いつつ「Ich komme aus Japan.」と言ったらちゃんとOKをもらえた.バンザイ.とりあえず Ich の ch の発音がよろしいとコメントを貰ったのだけど,国によってはこの音を全然発音できないそうな.少なくとも日本人にはあまり問題ない気がする.

ま,ぶっちゃけ他には数字を数えるくらいしか覚えとらんのだけど.

閑話休題.

Windows 8 が発売されたのか…… 何かをポチった記憶があるので実家に何かが届いているに違いない.外装丸出しだとちょっと困るな.

ワイドスクリーンはどれくらい普及しているのか?

とりあえずセミナー室のプロジェクターはアスペクト比がワイドなのにスクリーンは4:3という…… そしてプロジェクタを4:3出力した時にちょうどスクリーンいっぱいに映るようにしているのでワイド画面なPCを普通に接続すると両端がはみ出す罠.どうにかして欲しい気分.

なんとなくワイドに対応した横長のスクリーンってまだあまり見たことがない気がする.

閑話休題.

改めて部屋を眺めてみると日本の製品があちこちにあるのね.問題のプロジェクタもパナソニックだし.前に座ってる人が使ってたPCは東芝だし.ホテルのエアコンはダイキンでテレビは東芝だし.こんなもんなのか.

Isabelle で遊ぶ

Isabelle チュートリアルがあったので参加.Coqと違うなぁと思いつつ具体的にどう違うのかわからない程度.ハマったのは from a and b show hoge とか書いて a と b の順番が逆だと証明できないとかいうオチで.and って書いたら普通 commtative だと思いたいのだけどそうではないと.

つーか動きがよくわからん.当たり前だが.

閑話休題.

ディナーが7時半に始まり11時に終わるとか時間かけすぎだと思うのは気のせいだろうか? そして炭水化物が足りない.

閑話休題.

SNFC でストか…… どれくらい続くのかよくわからんのでちょっと遠出しにくいなぁ.満月直後にモンサンミッシェルとか行こうかと思ったが来週もう一度とかやられると困る……

気がつけば朝なので大学へ行く

モジュールがぁとか叫びながら Coq と遊んでいたらいつの間にか朝になっていたのでそのまま大学へ.同じファンクタを同じモジュールに別のモジュール内で適用してやったものが別物として扱われているのか何かの問題で物事がうまくいかない(訳わからんことしとるなぁ).つか,モジュールのシステムをリファレンスとか見ずに直感で使っているからおかしなことになっているのかもしれない.依存関係がめちゃくちゃなのをどうにかしよう.

閑話休題.

さすがに typeclasses のサーチの時間がかかりすぎるようになってきたなぁ.プログラムの自動変換が終わるまで30秒待ってくださいってのはギャグでしかない気がしてきた.

make clean 大事だな、きっと

Proof General で Compile Before Require のオプションを使っているのだけど,たまには rm *.vo *.glob してやったほうが良いのかもしれない.とりあえず意味不明な挙動が解消された気がする.……気がするだけかもしれない.

つか,Proof. typeclasses eauto. Qed. で証明できるのに証明が必要とかわけわからん.いまひとつ typeclass のリゾルバの挙動がつかめん.Implicit arguments の決定とのタイミングとかが問題なのか?

モジュールが第一級オブジェクトでないとやってられん

兎にも角にもめんどくさすぎてやってられん.つーか typeclass でライブラリ全部書き直されないかなぁ.

閑話休題.

モジュールの読み込みとインスタンス宣言のタイミングとの兼ね合いで個々の機能は動くのに合成した機能が働かない.いまひとつモジュールを絡めたスコープの扱いがよくわかってないな.要修行.

そして今日も無限ループと戦う.

リファレンスマニュアルに書いてあるのに……

Typeclass の eauto の深さ指定ができない.Typeclasses eauto := debug bfs 10 とかかくと 10 のところはピリオドだろと怒られる.うーん,書き方が悪いのか廃れたオプションがマニュアルにあるのか実装してないのにマニュアルにあるのか……

とりあえず,よくわからんけど無限ループしまくるのをどうにかして欲しい.デバッグも大変.すんごく微妙にインスタンスの優先度を設定したら無限ループを回避できたけど,もうちょっと頭良く探索してくれないかなぁ.

つか,dfs と bfs の切り替えもできてないような?

サマータイム

という言葉が一瞬通じなかった.Daylight saving time でオッケーだったと.

Wikipedia の Daylight saving time を見たらアメリカ英語的には daylight saving time なのね."summer time" って言い方はイギリス英語であると.まあ,Daylight saving time より summer time の方が単純な単語を使っているから日本だとサマータイムってなるのかね.

閑話休題.

つまり月末の土曜の深夜で終わりなんだな.前回来た時とは逆向きの調整になるのか…… 一日が25時間になるはずだけどどの時間帯が重複するんだろう?

Japanese Restaurant Hikari in Orleans

ディナーに連れて行ってもらったものの予約なしで適当に行こうぜ的なノリだったので当初の目的地には満員で入れず,適当に歩いて見つけた日本食レストランに面白そうだからと入ってみた.「ひかり」というお店で,この前行った Lift とかのある川の近くのレストラン街の一角にあった.12,3年くらいやってるらしい.

感想:全くがっかりしないちゃんとした日本の料理だった.揚げだし豆腐がとても美味しゅうございました.天ぷらも美味しかった(寿司は食べてないので分からない).

んで,日本の料理がフランスの作法に則って前菜から順に出てくるのは斬新だった.味噌汁もスープとして単品で出てきたし,普通のお椀(汁椀)に入ってぽつんと置かれるのでとても違和感があって面白い.何やらご飯とかとまとめて出すとフランスの人たちが困るとかでそうなっているそうな.ここらへんは習慣の違いよね.

今回は試せなかったのだけど,1日前に予約しておくとすき焼きとかもあるらしい.いなり寿司とか太巻きとかもその部類.機会があればここらを試してみたい気分.

ちなみに,女将さんは日本の方で日本語通じた.ウェイトレスさんは日本語ダメらしい.主人はちょっと日本語わかるらしい.

とりあえず,大当たりでしたとさ.久々に日本の料理が食べられて良かった.

あー,証明から値を取り出せないんか

まあ,exists x とか書かれていたとして具体的にどれが出てくるかとか証明上は関係ないのだから何かを取り出そうとしないというのが自然な思考なのだけど,ときどき値が取り出せたらなぁと思わなくない.

とりあえず Prop の扱いにまだ慣れていないらしい.

閑話休題.

証明を対話的にやるのが面倒だから直接プログラム書いてしまえと思うようになってきた.が,まだ tactic と実際のコードとの対応とかが把握しきれていないのでなんとも難しい.

単位体積あたりの熱量が……

パンだと少なすぎる気がする.半分以上空気じゃん.ご飯が恋しい.

閑話休題.

Function で定義した関数は Qed で終わらず Defined で終わっておかないと Eval compute とかで試しに動かした時にとても残念なコトになると学習した.ここらはもう少し中のことを理解しないとダメなんだろうなぁ…… つか,Function って何やってるのよ?

あー、便利なものがあるではないか、ないではないか

assert → apply とかいうコンボを使いまくっていたら,specialize 使えよアホというコメントを貰った.確かにアホだ.

閑話休題.

Leibniz equality ではなく equivalence relation を使って物事を定式化しようとすると証明が色々ととても面倒.rewrite とかが動かないのが非常にストレスなわけで…… Equivalence relation 用の rewrite とかあったりするのか? なければ自前で用意すりゃいいんだろうけどああ面倒.

Weekend パス

土日乗り放題で 3.6ユーロ.通常1回1.4ユーロなので3回乗ったら元が取れる.30回の回数券だと35.2ユーロなので4回乗らないと元が取れんけど.

お出かけ+買い物+大学に行くというのを週末にするにはこっちのほうがお得.

閑話休題.

日曜日とそれ以外の日との時刻表の差が激しすぎる…… 日曜だと始発が2時間半以上遅くなるとか信じられん.

ベルサイユ宮殿(雨)へ行く

早朝3時から天気予報とにらめっこをし,雨のベルサイユ宮殿ってのも面白いかねとか結論づけて朝イチの電車でパリへ出発.オステルリッツ駅に6時ちょっと過ぎに到着.そこからRERのC線(VICK)に乗り換えて終着駅まで40分くらい.とりあえず,終着駅の名前が Versailles Rive-Gauche だと思っていたところに券売機の表示が Versailles Château で戸惑った.切符には Versailles RG って書いてあるんだけど.

んで,駅から歩いて5分くらいでルイ14世がお出迎え.ぶっちゃけ7時過ぎなのでまだ真っ暗.

メインゲートが閉じてて庭園へすら入れないので宮殿の周りを歩きまわる.宮殿南の池から宮殿を望む.7時半を過ぎてそろそろ明るくなってきた.

8時過ぎに戻ってきたらメインゲートが開いていた.とりあえず中へ.

宮殿の建物へ入る第二の門は開かない.

そして飾りが面白い.

チケット売り場もまだ行列なし.

今日は土曜日なので噴水ショーがありますよと.お陰で庭園に入るだけで8.5ユーロとか取られる.

8時半を過ぎた辺りでチケット売り場に列が出来たので並ぶ.晴れてれば日がさしてただろうけど,あいにくと天気予報のとおりにご機嫌ななめな空模様.

色々と中略.9時直前に結構な雨が振ってきたり,チケットを事前に用意していた人たちの列がものすごかったり,チケット購入列の長い列の先には空いている自動券売機が鎮座していたり.色々と絶望した.

んで,目的地である鏡の回廊.まあ,人だらけ.今度来るときにはチケットを事前に用意しておこう(インターネットで購入して印刷しとけばいいんか?)


回廊を過ぎて階段のあたりで面白いものを発見.

階段のランプなのだけど,光が柔らかくなかなか良い感じだった.

そして庭園.広すぎる.広すぎる.全部は回っていられないので下の噴水まで移動.




んで,11時から噴水ショーが始まりましたとさ.



…….昔と同じただ水が出てくるだけの噴水だった.8.5ユーロ返せ,というのが素直な感想.もうちょっとこう電子制御された噴水ショー的なものを期待していたのだけど…… そんなんを期待するほうが悪いといえば悪いのだけど,人魚よりがっかりした.はぁ.

PermutationA め……

なんで欲しい性質が証明されていないんだ…… Sorting にある Permutation の方はいろいろ揃ってるのに.くそぅ.

歩く

終電を逃したので10キロほど歩く.まあ余裕で歩行圏内なのだけど,街灯がない道を歩いたり川を越えるのに手間取ったりして結局2時間かかった.もうちょっとちゃんとグーグルマップで予習しておくべきだったか.

閑話休題.

gcc のパスがおかしいなぁという問題はパスの最初を // にしてあげたら問題なくなった.きっと何処かで最初の一文字が消える仕様なのだろう(4.7.2 でもそうなったからなんか変なオプションの使い方をしているのかもしれんけど).

プログラミング言語をその初心者が使うと

言語処理系の奇妙な動作を結構な確率で掘り当てるという.その言語に慣れている人間であれば何となく回避するような使い方を平気でするのが原因なのだけど.まあ,滅多にないことはとりあえず気にしなくていいや的なのりでないと言語処理系の実装とかやってられないよね.

閑話休題.

gcc をいつものようにヘッダのインストール先を指定して cofigure && make && sudo make install したら,何故かヘッダファイルを探しに行くパスの最初のスラッシュが消えた状態の gcc がインストールされた.automake まわりのバージョンの食い違いとかでなにか変なことが起きたのか? よくわからないのでもう一度.

GCCのベクタライザに言う事をきかせられない

ほんのちょっと外側に単純なループを追加しただけで mulps とかが mulss とかになってしまう.中でやっている変換の仕様を見たほうがはやいかなとか思い始めた.

あとはレジスタ余ってるのに直前に読んだメモリをレジスタに置いとくとかしてくれないのね…… そのオフセットの値はひとつ前のイテレーションで読んでるじゃん,とか文句を言いながらどうしたもんかと1日悩む.結局解決法はわからん.Expression templates で計算式を持ってきているので手動で register と叫ぶことができず,コンパイラに頑張ってもらうしかないのだけど…… ああ,マイナス方向のインデックスへのアクセスを拾ってきて明示的にキャッシュしておいた値を返すように式を変換してしまえばいいのか.問題はそれをやったとしてベクタライザがうまく動いてくれるかだな.

コンパイラに言う事をきかせるのは難しい.

休日だが

関係ないので大学へ行く.今日は夕方に発表があったはずなので.

が,先週のセミナーの最後に「来週発表してね」と言われたはずなのだけどそれを言った主催者が今日は不在らしいというオチで…… 人も少ないしまた来週ってことになった.

next week って「次回」の意味だったのだろうか? 隔週でやるとか言ってた気もしなくもないからそうかもしれない.ま,いいや.

閑話休題.

ものすごく自明に SSE/AVX を使って並列化してもらえそうなのに GCC が頑張ってくれない.ICC でないとダメかなぁ.使える環境で一番新しい ICC の入ってるのってどれだ? つか帰ったら自分でひとつ買うか.

日曜だが

大学で明日の発表の準備.Expression Templates 使ったライブラリの技術的な話を期待さられているらしいのだけど,実装されたものを紹介しても複雑すぎるので簡易版を作って説明しなければならない.

ということで,朝からガリガリとC++のテンプレートなコードを書きつつスライド作成.ひと通り作ってから整理したら何故か2話分のスライドが出来上がっていた.

閑話休題.

休日の防犯巡回か何かの人たちがやってきて何かを語りかけられたのだけど,ぶっちゃけ何言ってるかわからんかった.ジェスチャー的に鍵をちゃんとかけろってことだと思うのだけど,正確なところはわからない.つか,フランス語分かりませんって言うフランス語を喋れるようになるべきだな.英語で言っても通じない.

「日本語食べれません」って言えば大抵の人は引き下がるよ,とかいうことを言っていた留学生を思い出した(「喋れません」すら言えないと認識されて無罪放免になるという論理).

VPS を幾つか試す

さくらのVPS以外も試してみようと思って,L2TP/IPsec な VPN が簡単に作れるかどうか幾つかの安い VPS で試した.つか,VPS と VPN って紛らわしい.

とりあえず月490円のお安い DTI の ServersMan @VPS Enrty を最初に試したが,使えるUbuntu のバージョンが古い(10.10 amd64, 10.04 x86)ってのと,カーネル周りがどうやって弄ったものかわからないのとで使いにくい.カーネルモジュール全然ないし…… モジュールを作りなおすとか嫌すぎるし…… そもそもカーネルいじれるのか? Ubuntu でカーネル変えると起動しませんとか書いてあるドキュメントもあったり…… とかいう感じで即解約.そもそも Ubuntu のインストーラを自分で操作してインストールするタイプでないので色々と面倒.

次に,月840円のカゴヤの VPS タイプA を試すも基本的に ServerMan のと同じでカーネル周りの自由度が…… という感想で即解約.こちらはインスタンスを1日30円で簡単に増やせるのでその点は便利な気がする.

最後に月940円のお名前.com のVPS1GBプラン.これは普通に Ubunru 12.04 を Ubuntu のインストーラを使ってインストールできるのでさくらのVPSと同様に使いやすい(さらには自前のISOをマウントして起動できるのか?).んで,通常のインストーラで入れるのでカーネル周りも普通で L2TP/IPsec な VPN の構築も何の問題もなく終わった.さくらの VPS と比べてコントロールパネルの出来がよろしい(初心者向けな)気がする.

とうことで,結論:お名前.com の VPS は使いやすいっぽい.計算機性能はどうだかしらんけど.

閑話休題.

お名前.com でサービスを使うには電話認証が必要だったりして微妙に躓いた.申請完了通知のメールに書いてあるURLのページに行ってそこにあるボタンを押すと,申請時に書いた電話番号に電話がかかってくるので,そのページにある認証コードを電話で入れてくださいと.……出張中にもかかわらず自宅の電話番号で申し込みをすると電話認証ができず残念なコトに.とりあえず,ユーザ情報の変更で携帯の電話番号に変更した上でもう一つインスタンスを申し込んで認証をするとかいう対処をした.つか,普通に電話番号間違って登録することもあるだろうから何処かに真っ当な対処法が有る気もする.

Typeclass で遊ぶ

Haskell と違って型以外の項もパラメータにとれるので色々と遊べる.自動でプログラムを変換させてみたりとか(基本となる関数の変換方法をインスタンスとして置いといて,それらの基本関数を適当に合成したものの変換結果を計算させるとか).

とりあえず基本的なギミックは理解したので来週はもうちょい応用にチャレンジしよう.

閑話休題.

自明だけど証明が面倒(というか tactic の使い方に慣れてない)なので admit が大活躍してたりする今日この頃.慣れている人が証明してくれることを願いつつリポジトリに投げる.

ハマる

Coq の Module の Inline ディレクティブに関連して理解不能なエラーにハマった.下のコードがハマった部分を抜き出したもの.

Module Type A. End A.
Module Type B  (a : A). 
  Parameter t : Type.
End B.
Module Type Bi (a : A). 
  Parameter Inline(10) t : Type.
End Bi.
Module C  (b : B).  End C.
Module Ci (b : Bi). End Ci.
 
Module CX (b : B) (bi : Bi).
  (* These two work well.*)
  Module Cb := C b.
  Module Cbi := C bi. 
  (* These two work well too, using `!' to ignore the Inline directive. "*)  
  Module Cib := !Ci b.
  Module Cibi := !Ci bi.
  (* This fails with saying "Error: The field t is missing in Top.b."*)  
  Module Cib2 := Ci b.
  (* This fails with saying "Error: The field t is missing in Top.bi."*)  
  Module Cibi2 := Ci bi.
End CX.

ファンクタ B と Bi は Print Module Type で見ても名前以外は同じ.ファンクタ C と Ci はファンクタ B と Bi をとる.んで,この C と Ci に B と Bi の型の b と bi を適用してみると,Inline を付けた定義の Bi を受け取るという定義の Ci に関してよくわからんエラーが出る.b も bi も t というフィールドを持っているのにそれが無いとか言われ…… 

とりあえず ! 付けて Inline を無視させればエラーでないということは学習した.でも Inline の意味はよくわからん.

隠れている部分が違うのか

Coq に「Hoge a b c の項が期待されるのに Hoge a b c の型の項なのでエラー」と言われた.このメッセージだけを見ていても何も悪いことしてないようにしか思えない.

んで,Set Printing All. と叫んでみたら implicit なパラメータ部分で微妙にずれていたという罠で,「@Hoge X a b c の項が期待されるのに @Hoge Y a b c の型の項なのでエラー」という意味のわかるエラーを吐いてくれるようになった.

……見えている型が同じだったら隠れている部分も自動で表示してくれればいいのに.

ちょっと移動

いい場所にキッチン付きのホテル(アパートメントホテル)を見つけたので移動.目の前に大学直通のトラムの駅がある.まぁ,30分強かかるけど.

とりあえずキッチンが使えるのはいいことだ.

使ってきた Linux ディストリビューションの変遷

1998年~1999年 Slackware.最初に Linux をいじった時にはカーネルのバージョンはまだ 2.0.X だった.PJE で Wnn を突っ込んだりとかしていたような気がする.この頃に比べると最近はものすごく便利になったもんだ.

1999年~2000年 Turbo Linux.ここらで Slackware で環境整えるのが面倒になって Turbo Linux に手を出してひよった.研究室のマシンは FreeBSD だったっけな.まだまだ Linux は趣味の世界だった頃?

2000年~2005年 Red Hat&Fedora Core.ひよるのにお金かけるのもあれだからとフリーにもどる.しばらくは Red Hat 系で安定.

2005年~2006年 Gentoo.後輩が使っているのを見て使い始めた気がする.結局,色々と面倒になったのとコンパイルしまくるのは環境によろしくないのとで1年くらいしか使わなかった気がする.

2006年~2008年 Debian.ここらは使うディストリビューションを色々試しつつ Fedora より Debian のほうが使いやすいかなぁとか考えていた気がする.

2008年~2012年 Ubuntu.お仕事用のメインマシンを Linux にして生活しようと決めて,色々と楽な Ubuntu に移ったのが 2008年の頭だったはず.ここから基本的に Ubuntu しか使ってない.

うん,よくわからんが普通な変遷だ.

Home > Archives > 2012年10月

Search
Feeds

Page Top