No Such Blog or Diary

«Prev || 1 | 2 | 3 |...| 800 | 801 | 802 |...| 1325 | 1326 | 1327 || Next»

coq2scala が……

Coq 8.4 用のはバグってる? 生成される関数の本体であるラムダ式が型引数を通常の引数と同様に受け取ろうとしているような気が…… 関数の型が合わないという文句を言われる.どうやら Haskell を吐いても Ocaml を吐いてもおかしいらしい.

とりあえず 8.3p12 用で我慢するか…… 別の部分が 8.4 の機能を使っている気がしなくもないのだけど大丈夫かな?

つか,1日に2回も coq をコンパイルすることになるとは.

こっくりこっくり

Coq を入れて proof general 入れてごにょごにょ.結構メンドイなぁ.証明の仕方がわかっても具体的に Coq をそのとおりに動かすのが慣れてないので手間かかる.うーん.

おーう,フランス語全然わからん(当たり前だが)

無事にお仕事その一は終了したが,お昼とかに周りの連中の会話を聞いていたのだけど全くフランス語がわからない.赤ん坊とかどうやって言語獲得してんだ? とりあえず第二外国語はドイツ語だったし,フランス語とか基本の単語もわからない.出口が Sortie だとか駅が Gare だとか確定が Valider だとか程度の名詞がいくつか分かる程度の能力.

うーん,悲しいのでちょいとフランス語をお勉強しよう.

閑話休題.

時差ボケがまだ……

移動

オルレアンへ移動した.RERのBが改装中につきシャルル・ド・ゴール国際空港から5駅ぐらいが使えないという罠にハマった以外は平和だった(バスで B のもう一方の端まで輸送中).

さて,明日は仕事だ.寝るか.

うーん……

ホテルの予約1日分間違ってたので面倒という罠.ま,いいか.

明日は早いので空港近くに移動.

プロシーディングスが重い……

荷物をぎりぎりの重さに仕上げてきているのでちょっと投げ捨てたい気分.適当に買った吊りばかりが意外と便利(超過料金払うギリギリの線を狙うのに).

閑話休題.

ようやく scala のインタプリタの動作の感覚がつかめてきた.コンパイルできてもインタプリタでロードできないファイルが有るとかやめて欲しいんだけど.とりあえずデモるにはインタプリタのほうが楽なのでソースをゴニョゴニョ修正.インタプリタで読み込むと,頭から順に処理してくれるのでファイルの後ろのほうで定義しているものを頭のほうで使うと文句を言われるっぽい.本当にそうなのか知らんがとりあえず定義の順を直したら通った.

閑話休題.

来週の月曜って日本だと休日なのか…… 月曜に海外でお仕事した場合って休日出勤扱いなのか? よくわからん.

«Prev || 1 | 2 | 3 |...| 800 | 801 | 802 |...| 1325 | 1326 | 1327 || Next»
Search
Feeds

Page Top