git pull時にエラー "error: failed to run repack"

久方ぶりにgitのリポジトリにトラブル発生。前回はこちら→「error: object file .git/objects/～ is empty」の対処法 - 発声練習

現象

以下のようなエラーがでる。

% git pull
Enter passphrase for key 'hogehoge': 
Auto packing the repository in background for optimum performance.
See "git help gc" for manual housekeeping.
error: The last gc run reported the following. Please correct the root cause
and remove .git/gc.log.
Automatic cleanup will not be performed until the file is removed.

error: bad packed object CRC for 8b06f3e6621e49ae6feefc517bd808fdf90d926b
error: failed to read object 8b06f3e6621e49ae6feefc517bd808fdf90d926b at offset 64243959 from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack
fatal: packed object 8b06f3e6621e49ae6feefc517bd808fdf90d926b (stored in .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack) is corrupt
error: failed to run repack

応急処置

「error: object file .git/objects/～ is empty」の対処法 - 発声練習の教訓をいかし、ワーキングディレクトリ（今回 WorkDirとする）の.gitをバックアップしておく。

% cd ~/WorkDir
% cp -pr .git .git-old

原因調査

言われたとおりgit gcを実行してみる。

% git gc
Counting objects: 89254, done.
Delta compression using up to 2 threads.
error: bad packed object CRC for 8b06f3e6621e49ae6feefc517bd808fdf90d926b
error: failed to read object 8b06f3e6621e49ae6feefc517bd808fdf90d926b at offset 64243959 from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack
fatal: packed object 8b06f3e6621e49ae6feefc517bd808fdf90d926b (stored in .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack) is corrupt
error: failed to run repack

どうも、8b06f3e6621e49ae6feefc517bd808fdf90d926bのハッシュキーを割り当てられたオブジェクトに問題が有る様子。つづいて、fsckを実行する。

% git fsck --full
Checking object directories: 100% (256/256), done.
error: .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack SHA1 checksum mismatch
error: index CRC mismatch for object 8b06f3e6621e49ae6feefc517bd808fdf90d926b from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack at offset 64243959
error: inflate: data stream error (invalid stored block lengths)
error: cannot unpack 8b06f3e6621e49ae6feefc517bd808fdf90d926b from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack at offset 64243959
error: inflate: data stream error (invalid stored block lengths)
error: failed to read delta base object 8b06f3e6621e49ae6feefc517bd808fdf90d926b at offset 64243959 from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack
error: cannot unpack 19b3bbceea4399c0c2d878701a846e9a4211f45e from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack at offset 69361275
Checking objects: 100% (82765/82765), done.
dangling blob 2b0c54951732d2539ade8535b636914d73548348
dangling blob 54df0cd16c54da83fcb2a522dd0a99f25c88f48d
dangling blob 6249d9d9fd0fd67733856654294207a4ebc43e90
dangling blob e4050a4ec65de33fc37f6fddaeb0e180f3a764ff
dangling blob 62372a20ebee044bd2be00298bf34b833bd6ea86
dangling blob 537b364ad9df32d9e0a21a94e3bf480721a1640a
missing blob 8b06f3e6621e49ae6feefc517bd808fdf90d926b

つづいて、git fsck。fullオプションよりも情報が多いのは何故？

% git fsck
Checking object directories: 100% (256/256), done.
error: .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack SHA1 checksum mismatch
error: index CRC mismatch for object 8b06f3e6621e49ae6feefc517bd808fdf90d926b from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack at offset 64243959
error: inflate: data stream error (invalid stored block lengths)
error: cannot unpack 8b06f3e6621e49ae6feefc517bd808fdf90d926b from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack at offset 64243959
error: inflate: data stream error (invalid stored block lengths)
error: failed to read delta base object 8b06f3e6621e49ae6feefc517bd808fdf90d926b at offset 64243959 from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack
error: cannot unpack 19b3bbceea4399c0c2d878701a846e9a4211f45e from .git/objects/pack/pack-55bbe2351e8cd70def9bc91271a9d66be731ec66.pack at offset 69361275
Checking objects: 100% (82765/82765), done.
broken link from    tree dc683ff3ebe0988a90073e5f2c29e15e98107b5f
              to    blob 8b06f3e6621e49ae6feefc517bd808fdf90d926b
Checking connectivity: 89252, done.
dangling blob 2b0c54951732d2539ade8535b636914d73548348
dangling blob 54df0cd16c54da83fcb2a522dd0a99f25c88f48d
dangling blob 6249d9d9fd0fd67733856654294207a4ebc43e90
dangling blob e4050a4ec65de33fc37f6fddaeb0e180f3a764ff
dangling blob 62372a20ebee044bd2be00298bf34b833bd6ea86
dangling blob 537b364ad9df32d9e0a21a94e3bf480721a1640a
missing blob 8b06f3e6621e49ae6feefc517bd808fdf90d926b

上の結果によると　dc683ff3ebe0988a90073e5f2c29e15e98107b5f　のツリーにおいて失敗しているとのこと。これの内訳を見てみる。

% git ls-tree dc683ff3ebe0988a90073e5f2c29e15e98107b5f
100644 blob 19b3bbceea4399c0c2d878701a846e9a4211f45e	"ファイル名１"
100644 blob 8b06f3e6621e49ae6feefc517bd808fdf90d926b	"ファイル名2"
100644 blob 16cde91af56ebf546f2278e395c1ede663f17c13	"ファイル名3"
100644 blob 6e3345ffacb05a5360aed34491887c25ad0313d9	ファイル名4
100644 blob 2f9d5e581f28d24cdf88fed69cbfcc1e82f5813f	"ファイル名5"

これらの５つのファイルを追加したときのコミットっぽい。これらのファイルが存在するかどうかを調べる。Git の object がおかしいというエラーが出た場合は object を表すファイルを消せば良さそう - ひだまりソケットは壊れないによるとblob（保存されているファイルそのもの）は、.git/objects/ハッシュの最初の２桁/ハッシュの残り　という名前で保存されているとのこと。調べてみると以下のとおり該当ファイルが存在しない。このため、エラーがでている様子。

% ls .git/objects/19/b3*
zsh: no matches found: .git/objects/19/b3*

% ls .git/objects/8b/06*
zsh: no matches found: .git/objects/8b/06*

% ls .git/objects/16/cd*
zsh: no matches found: .git/objects/16/cd*

% ls .git/objects/6e/33*
zsh: no matches found: .git/objects/6e/33*

% ls .git/objects/2f/9d5e*
zsh: no matches found: .git/objects/2f/9d5e*

小中学校の教室の温度を測るプロジェクトをだれかやってくれないかなぁ

はじめに

自分でやるとなると現状手が回らない。ソーシャルファンディングが始まったら寄付するので誰かやってくれないかなぁという他力本願エントリー

状況

いたましい事故が起きた。
www3.nhk.or.jp

17日午前、愛知県豊田市で小学校の校外学習に参加した１年生の男子児童が学校に戻ったあと意識を失い、熱中症で死亡しました。豊田市は、午前中から気温が30度を超え、気象台は、愛知県に高温注意情報を出していました。

愛知県の豊田市教育委員会によりますと、死亡したのは豊田市立梅坪小学校の１年生の男子児童です。

児童は、17日午前、学校から１キロ離れた公園で行われた校外学習に参加し、学校に戻ったあと意識を失って心肺停止になり、その後、死亡が確認されました。

熱中症と診断されたということです。

校外学習は、午前10時すぎから、１年生およそ110人が参加して行われ、30分ほど虫取りや遊具などで遊んだあと、11時半ごろに学校に戻ったということです。

児童は、公園に行く際、前を歩いていた児童から遅れ、「疲れた」と訴えたため、担任の教師が手を引いて歩いたということで、帰りも「疲れた」と話していたということです。


小中学校の教室の温度を測るプロジェクト

小学校や中学校の教室にエアコンを配備するというのは予算や教育方針などの影響で全国的に差がある。

こういうときには、まず、現状を測る必要がある。で、最近はIoTデバイスが普及してきているので、そいつを使って小中学校の教室の温度・湿度をリアルタイムで測定し、測定したデータを使って可視化することも比較的安価にできる環境になっている。

こんなのとか。
www.kyocera.co.jp
こんなの。
naltec.jp

こういうデバイスを１つの小中学校の教室5つぐらいに1個ずつ配置して（教室の真ん中の机の前側に貼り付けておく）、あとはドコモとか京セラがやっているLPWA網を利用すれば、1校当たり初期コスト15万円（デバイス1個1万円ぐらい？人件費10万円ぐらい？）、年間コスト数万円で計測可能だと思う。
www.nttdocomo.co.jp
www.kccs.co.jp

温度と湿度がわかれば環境庁が公開している暑さ指数を計算できるので教室の暑さ指数をきっちりと把握できる

ソラコムさんみたいなプラットフォーマーと情報系の大学生が組んでソーシャルファンディングでプロジェクトとかやってくれないかなぁ。
soracom.jp

学校へのエアコン設置話

news.yahoo.co.jp

www.asahi.com

www3.nhk.or.jp

メモ：小中高での情報モラル教育

時間が短く、かつ、基本的に安全側に行動方針を向けて欲しいとなると、「脅す」のが効率よくなっちゃうよね。

blog.jnito.com

edutmrrw.jp

d.hatena.ne.jp

以前、TBSラジオの東京ポッド許可局でサンキュータツオさんが「体罰」についてうまく説明していたので転載。

■ビンタは時短のための強制終了ボタン―――

今度はビンタの効果についても掘り下げ。10年以上、小学生にバスケットボールの指導をしていたタツオ局員が、体罰的なもののある種の「便利さ」について、指導者の立場から話しています。

  • タツオ：単純に時間の問題かな？って思ってたの。ビンタってもう強制終了。時間の節約。っていうのはさ、僕は小学生にずっと、12年ぐらいバスケットボールを教えていたわけ。で、やっぱり小5、小6ぐらいになると、もう言うことを聞かなくなるわけ。
  • マキタ：特に女子とかね。
  • タツオ：女子はもう本当に言うことを聞かなくなる。で、そういう時にどうすれば問題が早く解決するか？っていうと、恐怖政治ですよね。で、大声を出して言うことを聞かせる。あとはキャプテンのせいにするとか。規律を守るために、まずロジックを説明して。「みんなの責任はこの人の責任になります」っていう。
  • マキタ：血祭りにあげるところをちゃんと決めておくわけね。
  • タツオ：それをしてビンタするって最短の解決の仕方というか。自分が行きたい状態まですぐに行ける麻薬みたいな。一本そこは張っておいて、すぐに理想の静かな状態に持っていくような強制終了ボタン。だけど、その強制終了ボタンがなかった場合、割と言葉を尽くして話を聞いてもらって。しかも相手がわかるように変換しなきゃいけないっていう、結構な手間と時間を要するんですよ。それは、とても難しいことですよ。
  • マキタ：そうだね。
  • タツオ：「今、この場ですぐになんとかしなきゃいけない」っていう時にそれ、どうしたらいいのかな？っていうね。でも、そうしたことが求められている時代になっているんだよね。

（TBSラジオ：東京ポッド許可局 時代遅れの「ビンタ」より）

恐怖に限らず「心を動かす」ことは時間節約のために使われやすい（短時間で場当たり的な効果がでやすい）。対処療法的には、情報モラルについて適切な講師を呼ぶことが重要だけど、本質的には時間をかけることを許す環境を整備しないといけないのだと思う。学校へのニセ科学の浸透と根は一緒かなぁと。

貨幣の有用さがわかる事例：Coinhive

高木さんのエントリーで初めてCoinhiveという名称をしった。

で、Coinehiveとはなんぞや

Coinhiveは、サイトの運営者が、閲覧者に仮想通貨を採掘させ、その収益を受け取るサービスだ。専用のJavaScriptコードをサイトに埋め込むと、そのサイトを閲覧した人のPCのCPUパワーを使い、仮想通貨「Monero」を採掘。採掘益の7割が、サイト運営者に配分される（残りの3割は手数料として運営元・Coinhive Teamが受け取る）。

（話題の「Coinhive」とは？ 仮想通貨の新たな可能性か、迷惑なマルウェアか - ITmedia NEWS）

この仕組みを聞いて思い出したのが2000年代中盤あたりにキーワードになっていたグリッドコンピューティング。

グリッド・コンピューティングは、インターネットなどの広域のネットワーク上にある計算資源（CPUなどの計算能力や、ハードディスクなどの情報格納領域）を結びつけ、ひとつの複合したコンピュータシステムとしてサービスを提供する仕組みである。

グリッド・コンピューティング - Wikipedia

グリッドコンピューティングの一つの側面に使っていない計算資源をネット上からかき集めて、大きな計算資源が必要なプロジェクトを実施するというのがあった。それの典型例として当時紹介されていたのがSETI@homeのプロジェクト。

SETI@homeの本来の目的は次の2点だった。

  • 地球外知的生命体の証拠を検出するため、観測データの分析をサポートすることで、有益な科学的作業を行う。
  • 「ボランティア・コンピューティング」という概念の実現性と実用性を証明する。

後者の目的は一般に完全に成功したと見なされている。SETI@home の開発から発展した現在のBOINC環境では、様々な分野の計算量の多いプロジェクトにサポートを提供している。

前者の目的は今のところ達成されていない。SETI@homeによってETI（地球外知的生命体）信号の証拠が見つかったという例はない。

SETI@home では、アレシボ天文台の観測データを使い、その中に地球外知的生命体からの無線信号の証拠と見られるものがないか探索する。データは他の科学的プログラムに従って電波望遠鏡を使用しているときに便乗する形で採取されている。データはデジタイズされて記録され、SETI@home の施設に郵送される。そこでデータを時間と周波数で分割して小さな塊にし、それらを世界中のコンピュータに分配し、ノイズとは見なせない情報を含む可能性のある信号を探す。SETI@homeの要点は、データを小さく切り分け、それらを数百万台のパーソナルコンピュータで分析させ、分析結果を返してもらうという点にある。そうすることで、通常なら最新のスーパーコンピュータを必要とするような分析をインターネット上のコミュニティの援助によって達成できるようにした。

（SETI@home - Wikipedia）

プロジェクトに参加する人は、アプリケーションを自分が使っているPCにインストールしてPCの有休時間（あまりCPUやメモリを使っていない時間）に計算資源を提供するということを行っていた。基本的に計算資源はプロジェクト遂行のためのタスクに直接的に使われていた。

で、この発展として何かのサービスを提供する対価として計算資源を支払い、利用者からみると「無料」のエコシステムを回そうという発想がいろいろとでていたと記憶している。ただ、あまり流行らなかった。ネット環境やPCのスペックの問題もあったと思うが、サービスの対価に計算資源を「直接」払うというモデルがうまくなかったと思う（計算資源が欲しいプロジェクトと計算重を支払ってサービスを使いたい利用者とのマッチングが難しい）。Google先生に尋ねてみたらNTTがcell computingというグリッドコンピューティングプラットフォームを展開していたみたい。これはポイントという形で物々交換を抽象化している。

NTTデータは（2002年）12月13日、都内で記者発表会を行い、グリッドコンピューティングへの取り組みについての現状を紹介した。同社は、一般的なパソコンを多数つなぐことで、眠るコンピュータリソースを活用していくPCグリッドを推進しており、これを「cell computing」プロジェクトとして、ライフサイエンス分野などよりも市場規模が大きい一般企業に展開していく。

（エンタープライズ：NTTデータのPCグリッド、「参加者にお小遣いをアゲタイ」）

cell computing(セル・コンピューティング)は過去に行われていた分散コンピューティングの1つ。NTTデータが提供していたサービスであるが、収益の見通しが立たなかったため2008年3月31日に終了した。

BOINCプラットフォームが使われていた。 一般PC所有者に登録してもらい、分散コンピューティング技術を用いて、PCの遊休計算能力を利用する。当初はユーザが稼働させたコンピュータ資源に対し与えられるポイントを、商品等へ交換できるようにする計画があったが、実現はしなかった。また、そのPCの利用者に対する広告メディアとしての意味合いもあった。

（cell computing - Wikipedia）

今回のCoinhiveは、計算資源を仮想通貨に変換し、その仮想通貨で現実世界の任意のサービスを購入できる点が以前の計算資源とサービスの物々交換モデルや計算資源とポイントの交換モデルと異なっている。エネルギーの効率などを考えれば物々交換モデルがもっとも合理的なのだけど、利用者からすると任意のタイミングで、任意のサービスを購入できる貨幣の方が利便性が高く、参加する動機も高くなる。なんで、貨幣が普及したのかを実感させられる事例だと思った。

Ubuntu 16.04上にCoq, SSReflect, MathCompのインストール

Coq/SSReflect/MathCompによる定理証明 フリーソフトではじめる数学の形式化 | 森北出版株式会社を買ったので、とりあえず環境だけ整える。

インストール環境

% uname -a
Linux pi 4.4.0-122-generic #146-Ubuntu SMP Mon Apr 23 15:34:04 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux

% more /etc/lsb-release 
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=16.04
DISTRIB_CODENAME=xenial
DISTRIB_DESCRIPTION="Ubuntu 16.04.4 LTS"

Ubuntu 16.04のパッケージシステムに従うとcoqのヴァージョンが古いのでCoq/SSReflect/MathCompの設定を参考にコンパイルする。

Ocamlのインストール

% sudo aptitude install ocaml
% ocamlc -v
The OCaml compiler, version 4.02.3
Standard library directory: /usr/lib/ocaml

関連ライブラリーのインストール

% sudo aptitude install camlp5

CoqIde用のライブラリーは以下のとおり。なお、Ubuntu 16.04だとlablgtkが古いと言われる（2.18推奨のところ、2.16）。

% sudo aptitude install liblablgtk2-ocaml-dev
% sudo aptitude install liblablgtksourceview2-ocaml-dev

Coqのインストール

Releases · coq/coq · GitHubよりダウンロード。本では8.7.0をインストールしているが、8.8.0をインストールしてみる。

上述の本のバージョンよりかなり古い。

% tar xvfz coq-8.8.0.tar.gz
% cd coq-8.8.0
% ./configure |& tee configure.log
% make -j |& tee make.log
% sudo make install |& tee make_install.log
% coqc -v
The Coq Proof Assistant, version 8.8.0 (May 2018)
compiled on May 8 2018 20:32:08 with OCaml 4.02.3

MathCompとSSReflectのインストール

Releases · math-comp/math-comp · GitHubから1.7.0をダウンロードする。

% tar xvfz math-comp-mathcomp-1.7.0.tar.gz
% cd math-comp-mathcomp-1.7.0/mathcomp
% export COQBIN=/usr/local/bin/  （bashやzshの場合）
% setenv COQBIN /usr/local/bin/  （cshやtcshの場合）
% make -j 3 |& tee make.log
% sudo make install |& tee make_install.log

動作確認

起動する。

% coqide &

開いたウィンドウの左側に以下を入力する。

From mathcomp Require Import ssreflect.

Section ModusPonens.

Variables X Y : Prop.

Hypothesis XtoY_is_true: X -> Y.
Hypothesis X_is_true: X.

Theorem MP : Y.

Proof.
move: X_is_true.
by [].
Qed.

End ModusPonens.

実行してみる。