IQ1 Advent Calendar 2019、七日目の記事です。
今(書いてる時間)は2019年12月7日 -680時です。
12月7日じゃない?IQ1なのでよくわかりません。
おしまい。
2019年11月08日
IQ1 Advent Calendar 2019 七日目 -680時
posted by chiguri at 16:01| Comment(0)
| 雑多
2017年07月06日
AWStatsのインターフェースをいじろう(というのはお薦めできない)
結果として面倒だったので、「表示を変えた箇所を調べておけばバージョン変わってもなんとかなるかな?」くらいに考えている人は参考にならないとだけ言っておく。
AWStatsはログ解析ツールとしては結構有名どころらしく、普通にパッケージ管理ソフトで入るため、単に使いたいと言う場合にはあまり苦労することもなく導入できる。
また、使い方も調べればそれなりにでてくるため、さほど問題は起こらない。(少なくともここに来るような人にはすぐ見つけられるはず)
しかし、インターフェースは微妙なところもあり、変更したいと思ったりもする。
もっとも、やってみた感想は「やめた方がいい」なのだけど。
変更内容は、一年前の情報も同時に表示すること。
自分の所属が大学であるため、webサーバーの負荷などは大体月と曜日に依存している。
そのため、何か変化や異常があると、昨年と比較できれば割と簡単に見えるのである。
しかし、AWStatsのインターフェースはなぜかその年の情報しか出さないので、比較が難しい。
(また、その年しか出さないので、1-3月あたりでは表示される情報がなさすぎて使いづらい)
じゃあ並べるようにすればいいんじゃないかといじり始めたが、どうにもこうにも・・・
起こった問題(怒った問題)を挙げていこうと思う。
1)月ごとの情報を表示する箇所は割と簡単に見つけられて、HTMLMainMonthlyという関数になっている。
この中に前の年のデータを表示するルーチンを無理矢理書き込めばいいはずなのだが、全く部品化されていないので、今見ている年の処理をコピペするしかない。やれやれ。
2)よく見るとところどころにコメントアウトされたあからさまに不要とおぼしきコードが見える。バージョン管理してるだろうが。消せ。
3)無理矢理表示を追加してるうちに、月ごとの関数から移って日ごとの情報を表示する関数が目に入るが、インデントが少し壊れてる。直せ。(もっとも、自分が見たバージョンは現在のバージョンよりさらにひどかったので、少しずつ直しているのだろうか。全部直せよとは思うが。)
4)表示させるように変更したので、一年分の情報は読んでいるが全てのログを見ているわけではないということにすぐ気づく。サーバーによってはログがすごい量なのだから当たり前ではあるが、どこで読んでるのか分かりづらい。表示に使っているデータの変更箇所を追うと、どうやら3330行くらいからのRead_History_With_TmpUpdateという関数で読んでるらしい。呼び出し箇所を見ると月ごとに読むようにしている。ただし、選択した月とそれ以外で月以外にもう一つ引数が異なっている。意味はさっぱりわからず。中を見れば分かるかと関数の範囲を見ると3800行ある。読めるかこんなもの。
5)とりあえず選択していない月と同じように読ませればなんとかなるかとやってみたところ、前の年の表示に成功。一安心かと思ったら明らかに「時間毎の通信量」が増加している。何が起こってるのかと調べると昨年の同月分を単純に足している様子(1年後を表示させて気づいた)。変数から当たりを付けてRead_History云々を見ると「選択した月の情報なら計算対象にして、他の月だったら無視する」という状態になっている。月だけ??年のチェックは???
6)努力の甲斐あって表示に成功。ただ日本語表示になっているのにところどころ「日 月」の順になっていてもやもやする。かと思ったら一箇所だけ「〜年〜月〜」(日付はあるが「日」がない)になっていたりする。さらに気持ち悪い。何かと思って表示部を見たら順番がハードコーディングされている。一箇所だけ別ファイルからフォーマットを読んで出力している(ただし微妙に不足している)。だからその中途半端なのをやめろというのに。というか多言語対応やってるんならハードコーディングするなよ。
とまあこんな感じである。
全部手で直したので、当然のことながらバージョンアップしたらおじゃん。
全体的に思うのは、
1)全体のメンテナンスに気を遣っているか若干怪しい。
2)細かい引数指定があるのに、普通に出てくるはずの組み合わせを想定していない。
3)大域変数だらけで関数毎に想定している状態がさっぱりわからない。
4)関数がでかすぎる。
全体のテスト以外してないよねこれ、という感じである。
AWStatsはログ解析ツールとしては結構有名どころらしく、普通にパッケージ管理ソフトで入るため、単に使いたいと言う場合にはあまり苦労することもなく導入できる。
また、使い方も調べればそれなりにでてくるため、さほど問題は起こらない。(少なくともここに来るような人にはすぐ見つけられるはず)
しかし、インターフェースは微妙なところもあり、変更したいと思ったりもする。
もっとも、やってみた感想は「やめた方がいい」なのだけど。
変更内容は、一年前の情報も同時に表示すること。
自分の所属が大学であるため、webサーバーの負荷などは大体月と曜日に依存している。
そのため、何か変化や異常があると、昨年と比較できれば割と簡単に見えるのである。
しかし、AWStatsのインターフェースはなぜかその年の情報しか出さないので、比較が難しい。
(また、その年しか出さないので、1-3月あたりでは表示される情報がなさすぎて使いづらい)
じゃあ並べるようにすればいいんじゃないかといじり始めたが、どうにもこうにも・・・
起こった問題(怒った問題)を挙げていこうと思う。
1)月ごとの情報を表示する箇所は割と簡単に見つけられて、HTMLMainMonthlyという関数になっている。
この中に前の年のデータを表示するルーチンを無理矢理書き込めばいいはずなのだが、全く部品化されていないので、今見ている年の処理をコピペするしかない。やれやれ。
2)よく見るとところどころにコメントアウトされたあからさまに不要とおぼしきコードが見える。バージョン管理してるだろうが。消せ。
3)無理矢理表示を追加してるうちに、月ごとの関数から移って日ごとの情報を表示する関数が目に入るが、インデントが少し壊れてる。直せ。(もっとも、自分が見たバージョンは現在のバージョンよりさらにひどかったので、少しずつ直しているのだろうか。全部直せよとは思うが。)
4)表示させるように変更したので、一年分の情報は読んでいるが全てのログを見ているわけではないということにすぐ気づく。サーバーによってはログがすごい量なのだから当たり前ではあるが、どこで読んでるのか分かりづらい。表示に使っているデータの変更箇所を追うと、どうやら3330行くらいからのRead_History_With_TmpUpdateという関数で読んでるらしい。呼び出し箇所を見ると月ごとに読むようにしている。ただし、選択した月とそれ以外で月以外にもう一つ引数が異なっている。意味はさっぱりわからず。中を見れば分かるかと関数の範囲を見ると3800行ある。読めるかこんなもの。
5)とりあえず選択していない月と同じように読ませればなんとかなるかとやってみたところ、前の年の表示に成功。一安心かと思ったら明らかに「時間毎の通信量」が増加している。何が起こってるのかと調べると昨年の同月分を単純に足している様子(1年後を表示させて気づいた)。変数から当たりを付けてRead_History云々を見ると「選択した月の情報なら計算対象にして、他の月だったら無視する」という状態になっている。月だけ??年のチェックは???
6)努力の甲斐あって表示に成功。ただ日本語表示になっているのにところどころ「日 月」の順になっていてもやもやする。かと思ったら一箇所だけ「〜年〜月〜」(日付はあるが「日」がない)になっていたりする。さらに気持ち悪い。何かと思って表示部を見たら順番がハードコーディングされている。一箇所だけ別ファイルからフォーマットを読んで出力している(ただし微妙に不足している)。だからその中途半端なのをやめろというのに。というか多言語対応やってるんならハードコーディングするなよ。
とまあこんな感じである。
全部手で直したので、当然のことながらバージョンアップしたらおじゃん。
全体的に思うのは、
1)全体のメンテナンスに気を遣っているか若干怪しい。
2)細かい引数指定があるのに、普通に出てくるはずの組み合わせを想定していない。
3)大域変数だらけで関数毎に想定している状態がさっぱりわからない。
4)関数がでかすぎる。
全体のテスト以外してないよねこれ、という感じである。
posted by chiguri at 01:30| Comment(0)
| 雑多
2016年05月23日
WerckerのBoxの使い方(変更に巻き込まれた話2)
前回はカスタムしたBoxの作り方がずいぶん変わってしまったという話をしたのだが、実は使い方も変わっていたという話。
経緯はほぼ同じ。新しく作ったらBoxの設定ができなかった。
あまりにわからなかったので、サポートにメッセージ投げたら
「Wercker classicのサポートそのうちやめるよ。できれば早く移行してね。一応今は、やりたかったらstep作ってからprivateにし直したらできるよ。」
またstep作るんかい!!
step作るときは、対象のリポジトリがpublic repositoryしかダメなので注意。
リポジトリがprivateだったら、こっそりpublicにして、werckerのstep作って、deploy target消して、stepの設定でprivacyのところをprivateにして、リポジトリへのアクセス方法をdeploy keyに変更して、リポジトリの設定をprivateに直して、さあtrigger。またはgit push。
リポジトリがpublicだったら、werckerのstep作って、deploy target消して、stepの設定でprivacyのところをprivateにして、trigger。
いい加減classicから離れる方法を調べないとなあ。
経緯はほぼ同じ。新しく作ったらBoxの設定ができなかった。
あまりにわからなかったので、サポートにメッセージ投げたら
「Wercker classicのサポートそのうちやめるよ。できれば早く移行してね。一応今は、やりたかったらstep作ってからprivateにし直したらできるよ。」
またstep作るんかい!!
step作るときは、対象のリポジトリがpublic repositoryしかダメなので注意。
リポジトリがprivateだったら、こっそりpublicにして、werckerのstep作って、deploy target消して、stepの設定でprivacyのところをprivateにして、リポジトリへのアクセス方法をdeploy keyに変更して、リポジトリの設定をprivateに直して、さあtrigger。またはgit push。
リポジトリがpublicだったら、werckerのstep作って、deploy target消して、stepの設定でprivacyのところをprivateにして、trigger。
いい加減classicから離れる方法を調べないとなあ。
posted by chiguri at 22:32| Comment(0)
| 雑多
2016年02月20日
ZenPad 7を買った
Nexus7(2013)の画面を割ってしまった(2年振り?3回目)
修理に12k円もかかるのを三回もやったらさすがにちょっとやっていられないので、新しいのを購入することにした。
ZenPad 7といっても、2015年12月に出たARMのLTE使える方のやつである。
(7と言うと大分前にIntel入ってるのが出ているが、そっちはLTE不可)
とりあえず使った感想なのだが、まずNexus7のときに比べて、白飛びする。
解像度が低いのはわかっているし、さして気にもしないのでいいのだが、どうにも明るめの画像を見ると白になってる部分が。
Nexus7のときは気にならなかったし、他の画面と見比べてもZenPadのときだけ思うので、多分白飛びだと思うんだけどなあ・・・
次に、Androidデフォルトのアプリとほぼ同じような別のASUS製アプリが大漁に入っている。
いらぬ。無効にしかできないのが歯痒い。
UIはNexus7のときと似ているようで違う。ちょこちょこ引っかかるなあ。
カメラ、試してない。オートフォーカスがあるらしいのだが・・・(カメラアプリどこいったかな・・・)
後は現状さほど気にしていない。まあこんなものだろう。
ただ、久々に新しめのSDカードが入るAndroid端末を使って思うのだが、内蔵ドライブを特別扱い「しすぎて」いて、内蔵が小さいとやっていられない。
アプリ(のデータの一部)をSDに移す機能が使えることもあるが、やたら領域を食うのは大体が「後でダウンロードしたデータ」であって、「最初に入っているデータ」ではない。
SDに移せるのは「最初に入っているデータ(の一部)」なので、何の役にも立たず。
Kindleとかそこそこ買っているので、5GBを越えて内部を圧迫。つらい。
専用にフォーマットとかでもいいから、SDカードをもう少しまともに扱わせてくれないだろうか。
(Rootを取ればなんとかする方法もあるようだが、もしかしてRoot取りっぱなしじゃないとダメじゃないのこれ?と首を傾げているので今のところ試す気なし。symbolic linkを作るのかな?ならシェルからいける気がするけど)
うーむむむ・・・
追記:Rootはまだ取れなさそうだ。
ext3にフォーマットするとSDカード挿入ではマウントしてくれないし、仕方なくext3のパーティションを15GBほど作ったが、マウントできないのでやっぱり無用・・・
Root取れるようになったら試したいところではあるが・・・
修理に12k円もかかるのを三回もやったらさすがにちょっとやっていられないので、新しいのを購入することにした。
ZenPad 7といっても、2015年12月に出たARMのLTE使える方のやつである。
(7と言うと大分前にIntel入ってるのが出ているが、そっちはLTE不可)
とりあえず使った感想なのだが、まずNexus7のときに比べて、白飛びする。
解像度が低いのはわかっているし、さして気にもしないのでいいのだが、どうにも明るめの画像を見ると白になってる部分が。
Nexus7のときは気にならなかったし、他の画面と見比べてもZenPadのときだけ思うので、多分白飛びだと思うんだけどなあ・・・
次に、Androidデフォルトのアプリとほぼ同じような別のASUS製アプリが大漁に入っている。
いらぬ。無効にしかできないのが歯痒い。
UIはNexus7のときと似ているようで違う。ちょこちょこ引っかかるなあ。
カメラ、試してない。オートフォーカスがあるらしいのだが・・・(カメラアプリどこいったかな・・・)
後は現状さほど気にしていない。まあこんなものだろう。
ただ、久々に新しめのSDカードが入るAndroid端末を使って思うのだが、内蔵ドライブを特別扱い「しすぎて」いて、内蔵が小さいとやっていられない。
アプリ(のデータの一部)をSDに移す機能が使えることもあるが、やたら領域を食うのは大体が「後でダウンロードしたデータ」であって、「最初に入っているデータ」ではない。
SDに移せるのは「最初に入っているデータ(の一部)」なので、何の役にも立たず。
Kindleとかそこそこ買っているので、5GBを越えて内部を圧迫。つらい。
専用にフォーマットとかでもいいから、SDカードをもう少しまともに扱わせてくれないだろうか。
(Rootを取ればなんとかする方法もあるようだが、もしかしてRoot取りっぱなしじゃないとダメじゃないのこれ?と首を傾げているので今のところ試す気なし。symbolic linkを作るのかな?ならシェルからいける気がするけど)
うーむむむ・・・
追記:Rootはまだ取れなさそうだ。
ext3にフォーマットするとSDカード挿入ではマウントしてくれないし、仕方なくext3のパーティションを15GBほど作ったが、マウントできないのでやっぱり無用・・・
Root取れるようになったら試したいところではあるが・・・
posted by chiguri at 16:12| Comment(0)
| 雑多
2014年12月06日
Theorem Prover Advent Calendar 6日目:Coqでの前向き証明を始めるまで
タイトルの通り、これはTheorem Prover Advent Calendarの6日目のための記事である。
MizarやIsarをご存じだろうか?
Mizarは数学的な体系について性質を証明し、その証明が正しいことを機械で確認する、というのが目的である。
そのため、比較的証明を自然言語(英語)で書いたものに似せている。
実際の証明は、「こういう仮定がある。これを変形するとこうである。この補題からこういうことが言える。これはゴールと等価であるため、成立することが言える。」のように、仮定から前向きに証明を行うことがよく行われる。
この前向き証明だが、比較的読みやすいのが特徴である。
Isarは、このMizarの書き方をIsabelle上で使えるようにしたシステムである。
どうやら、証明が終わった後に前向き証明に書き換えるということを行われることも多いらしい。
さて、Isabelleに実装されていることをCoqで実装されていないと言うことがあろうか。
いやたくさんあるけど。
しかもかなりほしいものばっかりだけど。
スレッジハンマーとか。
ただし、今回紹介するこの機能に関しては、普通に論文も出て、さらに現在のCoqに実装されている。
マニュアルの11章を見よう。
ここからはそれを見ながらの話になる。
以上、前置き終わり。
ところで、前向きと書いたが、この機能自体は宣言的(declarative)という方が一般的だ。
すまないがタイトル変えるの面倒なので流して欲しい。
そして、マニュアルを書いている人はどうやら数学的証明と呼びたいようだ。
もう何でもいいや。
とりあえずここで書いている「数学的証明言語」とは、本来の証明の記述よりも弱いものらしい(11.1.3)。
記述時に使う自動証明がうまくいかなかった場合に、不完全な(普段で言うadmitで飛ばしたような)証明が書けてしまう。
この方向での証明で、なぜ不完全なものを書けるようにしたのか首を傾げるのだが、著者としては初学者が容易に学べるようにしたい、等の意図があったらしい。
エラーと切り替えられるようにした方が良いと思うのだが(admitにそういう機能が欲しい)。
ちなみに、不完全な証明を書くと、コマンドを打つ度に何度も何度も「これが証明できないよ」と言ってくる。
この機能の、標準的(legacy)Coqとの違いは大体以下の通り(上も含めている)。
想定環境も書いてあるが、普通にCoqを使う範囲ならば問題なさそうだ。
coqtopやcoqide、Proof-Generalもある。
他にもあるが、今回はちょっと放っておこう。
例えばPCoqが使えないと書いてあるけれど、そもそも今まともに使えるのかわからない(バージョン1.4が2003年2月に出ている。2013年ではない。私が大学に入る直前だ。)。
内容に入ろう。
文法が11.2に載っている。
全体としては証明構造を記述するのが主で、ほとんど対応するのは基本的なtacticだ。
命題などをより具体的に書かせている点が違う。
基本的に命題を具体的に書くが、ゴールだけは何度も書かなくて良いように特殊な名前としてthesisが使えるらしい。
"thesis"はみんなだいすき学位論文・・・という意味もあるが、ここでは主張する命題のこと(辞書を見よう)。
文法は読み慣れていないと分かりづらいので、とりあえず動かすのが定石。
11.3で機能を説明しているので、見ていこう。
まず「証明の始め方と終わり方」が書いてある。
そしていきなりAnormalyを出す。しかも"Please report"が出るヤツだ。(実装のバグの可能性が高いから報告してくれ、と言うメッセージ。実装をいじったりすると出る)
え??
続いて「proofコマンドは残りが一つじゃないと使えないんだ」といって3つのサブゴールがある例を使う。
ここでもAnormalyを出す。
おい。
エラーメッセージ作れよ。
なんでこんなのがマニュアルに載るんだろう。
そんな愚痴を言っても始まらないので、実行してみる。
うん。マニュアル通りの動き・・・え??
証明が終わってない。
たしかQedの直後は「証明に使ったスクリプトを出す」はず。
ちなみに証明項はできていて、Show Proofで見られる。
うん、まあ若干不思議なことをやってるけど、別に問題なさそうだ(おそらく特徴の一つの、自動生成された変数の使い切りのために関数抽象になっているのだと思う)。
だがエラーだ。
エラー対策しろよ。マジメに。
考えてみると、この機能で書いた証明、今までの記述と同じ分けがない。
それで証明の出力関数が死んでるわけだ。
そう考えると、Qedの直後の出力を抑制できれば大丈夫なはずだが、マニュアルを見てもそんなコマンドは見つからない。
そして、この機能の説明がある章、よく見ると「どの例もQedまで行ってない」のだ。
ふざけんな。
調べてみたが、唯一見つかったのが、出力をほぼ完全に抑制するSet Silentコマンド。
あとでUnsetすれば大丈夫だろう、と高をくくって実行。こんな感じになった。
ようやく始められる状態まで来たが、さすがに今回これ以上書こうという気力が湧かない(日をまたぎかねないというのもある)。
なので、この話はここまでと言うことにしておく。
次回をやる気力が湧けば書くかもしれないが、とりあえずこの問題を回避できれば後は書かれている例題を元に少し試してみるだけなので、それぞれで試すこともできるだろう。
まだ紹介するような機能じゃなかった。
腐ってやがる!早すぎたんだ!
なんてね。
MizarやIsarをご存じだろうか?
Mizarは数学的な体系について性質を証明し、その証明が正しいことを機械で確認する、というのが目的である。
そのため、比較的証明を自然言語(英語)で書いたものに似せている。
実際の証明は、「こういう仮定がある。これを変形するとこうである。この補題からこういうことが言える。これはゴールと等価であるため、成立することが言える。」のように、仮定から前向きに証明を行うことがよく行われる。
この前向き証明だが、比較的読みやすいのが特徴である。
Isarは、このMizarの書き方をIsabelle上で使えるようにしたシステムである。
どうやら、証明が終わった後に前向き証明に書き換えるということを行われることも多いらしい。
さて、Isabelleに実装されていることをCoqで実装されていないと言うことがあろうか。
いやたくさんあるけど。
しかもかなりほしいものばっかりだけど。
スレッジハンマーとか。
ただし、今回紹介するこの機能に関しては、普通に論文も出て、さらに現在のCoqに実装されている。
マニュアルの11章を見よう。
ここからはそれを見ながらの話になる。
以上、前置き終わり。
ところで、前向きと書いたが、この機能自体は宣言的(declarative)という方が一般的だ。
すまないがタイトル変えるの面倒なので流して欲しい。
そして、マニュアルを書いている人はどうやら数学的証明と呼びたいようだ。
もう何でもいいや。
とりあえずここで書いている「数学的証明言語」とは、本来の証明の記述よりも弱いものらしい(11.1.3)。
記述時に使う自動証明がうまくいかなかった場合に、不完全な(普段で言うadmitで飛ばしたような)証明が書けてしまう。
この方向での証明で、なぜ不完全なものを書けるようにしたのか首を傾げるのだが、著者としては初学者が容易に学べるようにしたい、等の意図があったらしい。
エラーと切り替えられるようにした方が良いと思うのだが(admitにそういう機能が欲しい)。
ちなみに、不完全な証明を書くと、コマンドを打つ度に何度も何度も「これが証明できないよ」と言ってくる。
この機能の、標準的(legacy)Coqとの違いは大体以下の通り(上も含めている)。
- focusという機能で「今から証明するものを一つに絞る」機能がある。表示範囲が圧迫されない意味では悪くなさそうな機能だ。
- 証明できないようなものを書いても「後で埋められるようにwarning出すだけにしている」。(上に書いた)
- 通常のtacticはコマンドの特定の位置に書くか、escapeコマンドで一旦通常モードに戻して使わせる。特定の場所とは、例えばそのときに成り立つ命題を作る際のusingの直後。ちなみに、by 変数かusing tacticで進めるのが主だが、何も書かないとfirst-orderで解くらしい(11.3.14)。これで解けないと「不完全な証明」となる。
- 変数名などの自動生成は可能だが、必ず_から始まり、次のコマンドの終了後消える(11.2.1)。これは変数名の衝突を避けることと、名前つけるのが面倒なことのバランス取れてるかもしれない。必要なら名前をつけろ、というのも理解できる。
想定環境も書いてあるが、普通にCoqを使う範囲ならば問題なさそうだ。
coqtopやcoqide、Proof-Generalもある。
他にもあるが、今回はちょっと放っておこう。
例えばPCoqが使えないと書いてあるけれど、そもそも今まともに使えるのかわからない(バージョン1.4が2003年2月に出ている。2013年ではない。私が大学に入る直前だ。)。
内容に入ろう。
文法が11.2に載っている。
全体としては証明構造を記述するのが主で、ほとんど対応するのは基本的なtacticだ。
命題などをより具体的に書かせている点が違う。
基本的に命題を具体的に書くが、ゴールだけは何度も書かなくて良いように特殊な名前としてthesisが使えるらしい。
"thesis"はみんなだいすき学位論文・・・という意味もあるが、ここでは主張する命題のこと(辞書を見よう)。
文法は読み慣れていないと分かりづらいので、とりあえず動かすのが定石。
11.3で機能を説明しているので、見ていこう。
まず「証明の始め方と終わり方」が書いてある。
そしていきなりAnormalyを出す。しかも"Please report"が出るヤツだ。(実装のバグの可能性が高いから報告してくれ、と言うメッセージ。実装をいじったりすると出る)
え??
続いて「proofコマンドは残りが一つじゃないと使えないんだ」といって3つのサブゴールがある例を使う。
ここでもAnormalyを出す。
おい。
エラーメッセージ作れよ。
なんでこんなのがマニュアルに載るんだろう。
そんな愚痴を言っても始まらないので、実行してみる。
Welcome to Coq 8.4pl4 (June 2014)
Coq < Goal True.
1 subgoal
============================
True
Unnamed_thm < proof.
1 focused subgoal (unfocused: 0)
============================
True
Unnamed_thm < thus thesis. (* first-orderで解いている *)
No more subgoals.
Unnamed_thm < end proof.
No more subgoals.
Unnamed_thm < Qed.
Anomaly: Cannot print a raw proof_instr. Please report.
Unnamed_thm <
うん。マニュアル通りの動き・・・え??
Unnamed_thm <
証明が終わってない。
たしかQedの直後は「証明に使ったスクリプトを出す」はず。
ちなみに証明項はできていて、Show Proofで見られる。
Unnamed_thm < Show Proof.
((fun _fact : True => _fact) I)
うん、まあ若干不思議なことをやってるけど、別に問題なさそうだ(おそらく特徴の一つの、自動生成された変数の使い切りのために関数抽象になっているのだと思う)。
だがエラーだ。
エラー対策しろよ。マジメに。
考えてみると、この機能で書いた証明、今までの記述と同じ分けがない。
それで証明の出力関数が死んでるわけだ。
そう考えると、Qedの直後の出力を抑制できれば大丈夫なはずだが、マニュアルを見てもそんなコマンドは見つからない。
そして、この機能の説明がある章、よく見ると「どの例もQedまで行ってない」のだ。
ふざけんな。
調べてみたが、唯一見つかったのが、出力をほぼ完全に抑制するSet Silentコマンド。
あとでUnsetすれば大丈夫だろう、と高をくくって実行。こんな感じになった。
Unnamed_thm < Qed.
Anomaly: Cannot print a raw proof_instr. Please report.
Unnamed_thm < Set Silent.
Unnamed_thm < Qed.
Coq < Unset Silent. (* 左側が変わってるのでうまくいったっぽい *)
Coq < Print All.
>>>>>>> Library Top
Unnamed_thm : True
Coq < (* Goalだから勝手につけられた名前だができている *)
ようやく始められる状態まで来たが、さすがに今回これ以上書こうという気力が湧かない(日をまたぎかねないというのもある)。
なので、この話はここまでと言うことにしておく。
次回をやる気力が湧けば書くかもしれないが、とりあえずこの問題を回避できれば後は書かれている例題を元に少し試してみるだけなので、それぞれで試すこともできるだろう。
まだ紹介するような機能じゃなかった。
腐ってやがる!早すぎたんだ!
なんてね。
posted by chiguri at 22:06| Comment(1)
| 雑多