herokuがgit push heroku masterしても一向に動いてくれなかった件

heroku

githubのフィードをtwitterに投げ続けるだけのbotをherokuで作った

Procfileは↓というだけの簡単なもので、構成もGemfileとProcfileとbot.rbだけのシンプルなもの

cat Procfile
worker: bundle exec ruby bot.rb

herokuにログイン

https://dashboard.heroku.com/apps からサクッとアプリをひとつ作って、herokuコマンドでリポジトリを追加。

heroku git:remote -a xxxxxbot

あとは

git push heroku master

で動くはずだった。

が！一向に動かない

logを仕込んでみたりheroku runでコマンド実行してみたりしてもうあくいかないし、プロセスを確認すると動いている様子はない

なんでー

と思ってダッシュボード見なおしてみると、dynoの割り当てが０！

なるほど！そりゃ動かんわ！

というわけで、ダッシュボードからdynoの割り当てを１にしたら無事動いた

vagrantで立ち上げたvmがどこにあったかわからなくなっちゃう

vagrant

Macというのはダメな奴なので、ubuntuとかが欲しくなる。

というわけでとりあえず作業用にVMを立ち上げたりよくするんだけど、適当にVagrantfileを作って起動するものだから、しばらくするとどこで立ち上げたやつだかわからなくなる。 Vagrantfileどこだっけ・・みたいな

ちゃんと管理しとけな話なんだけどそういうことがちょいちょいあるので、全部VM見れるようなのはないんだろうか。

と思ったらあった

fgrehm/vagrant-global-status · GitHub

と思ったらもうDEPRECATEDだ

Centralized machine index by mitchellh · Pull Request #3225 · mitchellh/vagrant · GitHub

と思ったらもうvagrant本家に取り込まれてるじゃん

vagrant global-status - Command-Line Interface - Vagrant Documentation

vagrant global-status　でいいのね。いいじゃん。

--prune でゾンビを消すこともできるんだ。便利

Coq入門 - 4.1

coq

https://coq.inria.fr/を見ていたら、Documentationのところにこんなものがあった。

https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf

ここにSearchのことが少し書いてあって、SearchRewriteで望むものが出てこない理由がわかった。

The command SearchRewrite is similar, but it only looks for rewriting theorems, that is, theorems where the proved predicate is an equality.

なるほど、rewriteっていうのは確かにそういうことか。

applyとは別ね。

applyしか使ってなくてよく分かっていなかった。

このドキュメントを読む感じだとSearchやSearchPatternを使うべきっぽいが、emacsのcoq mode(かproof-general?)のコマンドにはそれらはない。

あるのは

  • SearchRewrite
  • SearchAbout
  • SearchConstant
  • Searchregexp
  • SearchIsos

のようだ。

RewriteとAboutは解説があるが、他は・・・？

特にemacsコマンドにドキュメントは書かれていないようだ

ただ、SearchIsosがC-c C-a C-oにProofGeneralでバインドされていて、使う頻度が高そう。

使ってみるとエコーエリア？に

SearchPattern (parenthesis mandatory), ex: (?X1 + _ = _ + ?X1) (default nil):

なんかSearchPatternと書いてあるし、クエリの例も求めているものっぽい。

使ってみると望み通りっぽい結果が出てきている。

これを使って進めてみよう。というメモ

Coq入門 - 4

coq

進捗あまりない。

update · 702639b · totem3/coq-prac · GitHub

全然わからんのでもうImportしたのを使って証明せずに進めているｗ

できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。

こうなってくると、今後まともにやっていくうえで大事なのはSearchを使いこなすことのような気がしてくるんだけど、不等号系が全然SearchRewriteとか使っても出てこない

このあたりがよくわからない。次使いこなすべきはSearchかなと思った

n <= m -> ~ m < nとかFalseの証明がでてきたけど、これがやっぱりわからない。

Searchを使いこなせるようになるのと、矛盾を示せるようになりたい

Coq入門 - 3

coq

Coq入門 - 2.1 - エンジニアですよ！ に追記したが、Lemma le_n_0_eqが証明できた

あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。

False_indやFalseの証明の仕方が少しわかった。

しかし、その後も証明ははかどらない。

ムリ

Coqの使い方とかtacticがどうこう、というより単に証明するだけの頭脳が私にないような気がしてきた

もしくは自然数の証明は難しいのではないのか？

そんなことはないか

ペアノの公理は数学ガールで読んだことがあるというくらいの知識はあるんだがｗ

高校でも大学受験でも証明はすごい苦手だったなぁ

さて戻って、証明の続きをしてる。

全然証明進まないし、答え（標準ライブラリのコード）を見ても全然わからないんで飛ばす。

ArithとかImportしてるんで証明は進む。intuitionだけで進むｗ

intuitionだけで進まなくなったle_elim_relを証明してみようと思って取り組んでみる

さっぱりわからーん。

inductionとdestructしか使えるものがないので全然進まない

2日ほど悩んでライブラリを読んでみると、なんだろうね

auto with arithとかやってるので自動で証明できるくらい些細な事なんだろうな。

わからんけどね。

でもelimっていうのもあるので、使ってみたら証明できた。

autoを使っていないところ以外はまるっきりライブラリ通り。

introsで名前を渡すところとか、できる気がしない・・・

introsで名前を特に渡さずにやると、進まなくなる。

具体的には、この部分。

Lemma le_elim_rel :
 forall P:nat -> nat -> Prop,
   (forall p, P 0 p) ->
   (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) ->
   forall n m, n <= m -> P n m.
  intros P H0 HS.
  induction n; trivial.
  intros m Le.
  elim Le.
  apply HS.
  intuition.
 
2 subgoals, subgoal 1 (ID 97)
  
  P : nat -> nat -> Prop
  H0 : forall p : nat, P 0 p
  HS : forall p q : nat, p <= q -> P p q -> P (S p) (S q)
  n : nat
  IHn : forall m : nat, n <= m -> P n m
  m : nat
  Le : S n <= m
  ============================
   P n n

ここで、名前を付けずに進めていると、 IHn : forall m : nat, n <= m -> P n mこの部分がforall m : natが付いてないものになってしまい、P n nにapplyできなくて進まない。

証明ができない！ こんなときにもgeneralizeしないと進まないことあるよ、みたいに書いてあるからやってみたけどそれでも進まん。

まぁとりあえずintrosするときには名前を付けると何が違うのかと、elimについて学ぼうと思う

Coq タクティクリファレンス: 帰納法と場合分け

ここがとても詳しいので、ここを読む。