neovimでcoq環境
neovim上にcoqの環境を整えます
基本的にはこちらの記事を見るとよくわかると思います.
僕の場合のハマったところを詳細に記述していこうと思います.
coquilleを導入する
dein.toml
[[plugins]] repo = "let-def/vimbufsync" on_ft = "coq" [[plugins]] repo = "the-lambda-church/coquille" on_ft = "coq" depends = ["vimbufsync"] hook_source = """ let CoqIDE_coqtop = '/usr/local/bin/coqtop' nmap <silent> J :CoqNext<CR> nmap <silent> K :CoqUndo<CR> nmap <silent> L :CoqToCursor<CR> """
あとはneovimを開いて :call dein#update() します
python2導入する
python3 をneovimで使っている人は多いと思いますが，
現在(2018/10/31), coquilleは python3 対応がまだ完了していないようです*1
これに気づかずハマっていました.
neovim上で
:echo has('python')
で 1 が返ってきたらneovim上でpython2が使えます.
0 の場合は
pip2 install neovim
してやりましょう
必要に応じて
let g:python_host_prog='/usr/local/bin/python2'
を init.vim を書き込む必要があるかもしれないです.
完
neovim上で
:CoqIDELaunch
:CoqIDENext してみて動けば完了です.
何もフィードバックがない場合はpython2が入ってない，認識されてないかもしれません. 頑張ってください.
*1:issueに上がっていました: https://github.com/the-lambda-church/coquille/issues/59
fishの文法を書くのがめんどくさい人のためのTips
fish shellを使って2年がたちました
今では結構使っている人も多いのではないでしょうか
fishはとても使いやすい良いshellです. ただbashやzshと文法が大きくことなります.
特に苦労する機会が多いのは環境変数の文法や &&, || が使えないことだと思います.
僕の2年悩んだ苦渋にまみれた解決策があるのですが、 余り同じようなことをしている人をみないので共有します.
苦渋にまみれているので、デメリットもあることを念頭に置いておいてください.
fishの環境変数
export HOGE=hensu-dayo
と書くと思います.
fishでは
set -x HOGE hensu-dayo
こうですね.
全然違うので web上に乗っているscriptを毎回書き直すの 面倒です.
苦渋にまみれた解決策
.bash_profile
export HOGE=hensu-dayo exec fish
これであら不思議, 環境変数がbashのままfishを使えます 😇
デメリットとして, bashを起動しようとしてもfishが開きます 😇
&& ||が使えない
bashでは
echo hoge && echo foo
というように記述しますが,
fishでは
echo hoge; and echo foo
といった風になります.
書き直すのめんどくさいですね
苦渋にまみれた解決策
- bash -c オプションを使う
bash -c 'echo hoge && echo foo'
これでそのままコピペできますね😇
それでもやっぱりめんどくさい😇
fishの関数を作って少しでも楽をします.
以下のようなfishスクリプトを~/.config/fish/functions/bash_c.fishとして保存します.
~/.config/fish/functions/bash_c.fish
function bash_c read --prompt="echo 'write bash script: '" bash_script bash -c $bash_script end
これでfishでbash_cをうち、bashスクリプトを入力するとbashを実行できます.
ただしあくまでbashのプロセスが立ち上がり実行されるので、ここで環境変数の設定とかはできません😇
だれか良い方法を教えてください😇
DockerでGo × mysqlの最低限な開発環境を用意する
今更ながらDockerの勉強をしています。 色々わからないところが多く、詰まったりしたところが多かったので自分はこのようにしたというのをまとめて見ます。output大事かなって思ったので
他にやり方があるよとかあれば、教えていただけると嬉しいです。
一応Dockerとか関係なく、 ローカルでさえ設定ができませえんって人が読めるくらいのレベルで書きたいです。
コードは全てgithubにおいておきます。 記事では関係ないところは飛ばしていたりします。 疑問があればご確認ください. この記事のコード
この記事の目標
コマンドを一つ叩くと、 (データがなければ)初期化されたmysqlコンテナ、goのwebコンテナが立ち上がり、 今回はmysqlに入ったデータを取得し、jsonで返すくらいにしておきます。
この際、もちろんですが、データは永続化されていて、 ついでにmysqlのログがローカルで見れるようにします。
docker-composeが動く環境にだけしておいてください。
下準備:mysqlコンテナ
mysqlコンテナの下準備をします。 具体的には,
- 文字コードの変更
- logをローカルで見れるようにする
- 初期データを作る
文字コードの変更
公式のmysql imageを使いますが、 そのままだと日本語を入れると文字化けしてしまいます.
解決策は調べてみた感じで複数あるようです。
mysqlの設定ファイルをVOLUMEを使って書き換える
僕はこれを使いました。 query logを見たくなった時とかにどうせ書き換える必要があるし
という訳で設定ファイルを用意します. mysql系の設定ファイルはmysqlというでディレクトリを作ってそこに入れることにします。
./mysql/my.cnf
... [client] ... default-character-set=utf8 ... [mysqld] ... character-set-server=utf8
文字コードをutf8に変更しておきましょう。 寿司ビール問題とかはとりあえず無視でします。
mysqlの公式のコマンドを使う(試してない)
見にくくなるのこちらに書きました.
logをローカルで見れるようにする
ここでは、とりあえずerr-logをローカルで見れるようにします。
そもそもエラーログを出力させるために my.cnfを編集しましょう.
./mysql/my.cnf
[mysqld] ... log-error = /var/log/mysql/error.log
次にローカルにログを出力するためのディレクトリを作っておきます。
mkdir mysql/log
ログの下準備は以上です。
初期データを作る
やり方は色々あるでしょうが、 ここでは、mysqlの公式コンテナでは, コンテナ内の/docker-entrypoint-initdb.dというディレクトリにある .sqlファイルと.shファイルをコンテナ作成時に読み込んでくれるというものを利用します。
ローカルに初期データ用のディレクトリを作っておき, 以下のようなsqlファイルを作っておきます.
./mysql/init/0_init.sql
CREATE DATABASE test_db; CREATE TABLE test_db.test_table(id int, name varchar(256)); INSERT INTO test_db.test_table VALUES(1, "ひょーが");
/docker-entrypoint-initdb.d以下のファイルはアルファベット順に読み込まれるようなので、 0_hoge.sql, 1_foo.shのようにしておくと楽かもしれません。
mysql下準備まとめ
ここでは以下の三つのことをするための下準備をしました。
- 文字コードの変更
- logをローカルで見れるようにする
- 初期データを作る
ここまでの操作は全てローカルで行われています。 ディレクトリ構成は以下のようになりました。 詳しくはgithubで確認して見てください. この記事のコード
. |--mysql |--init | |--0_init.sql |--log |--my.cnf
下準備:Golangコンテナ
特になんてことはしません. ここでは以下のことをします.
- jsonを返すだけのコードをかく
- vendoringする
jsonを返すだけのコードをかく
./src/cmd/main.go
package main import ( "database/sql" "fmt" "github.com/gin-gonic/gin" _ "github.com/go-sql-driver/mysql" ) type User struct { ID int Name string } func main() { r := gin.Default() r.GET("/ping", func(c *gin.Context) { db, err := sql.Open("mysql", "root:password@tcp(db-server:3306)/test_db") defer db.Close() if err != nil { fmt.Println(err.Error()) } rows, err := db.Query("SELECT * FROM test_table") defer rows.Close() if err != nil { fmt.Println(err) } user := User{} for rows.Next() { err = rows.Scan(&user.ID, &user.Name) if err != nil { fmt.Println(err) } fmt.Println(user) } c.JSON(200, gin.H{ "hello": user.Name, }) }) r.Run() }
コードが汚い？ハードコーディング？ なんの事やら
vendoringする
これもやり方は複数あると思います。 何がベストプラクティスかわかりません、教えていただけると幸いです。
ここでは、depというものを使いました。
cd src
dep init
とするとsrc以下にvendorディレクトリが作成され、 依存パッケージが入ってくれます。 詳しい使い方は調べて見てください。
余談
このvendoringはgolangで用いている 依存パッケージをコンテナ内で使うために行なっています。
ここでは、依存パッケージをVOLUMEでコンテナ内に追加する事で解決しています。 ですが、コンテナを立ち上げ時に依存パッケージを全部ダウンロードということもできます。 他にも方法はあるでしょう。
何が良いのかぶっちゃけわからないので、教えてください。
Golang下準備まとめ
ここでは、以下のことをしました。
- jsonを返すだけのコードをかく
- vendoringする
ここまでのディレクトリ構成は以下のようになっています。
. |--src | |--Gopkg.lock | |--Gopkg.toml | |--cmd | | |--main.go | |--vendor | |--github.com | |--gin-contrib | |--..... | |--..... | |--..... | |--mysql |--init | |--0_init.sql |--log |--my.cnf
docker-compose.ymlをかく
ここからが本番です。 実際にmysqlのコンテナとgoのコンテナを立ち上げ、 動かします。
先にdocker-compose.ymlが結局こうなったというのを示します。
./docker-compose.yml
version: '3.3' services: db-server: image: mysql ports: - "3306:3306" volumes: - "data:/var/lib/mysql" - "data:/var/log/mysql" - "./mysql:/etc/mysql/conf.d" - "./mysql/init:/docker-entrypoint-initdb.d" - "./mysql/log:/var/log/mysql" environment: mysql_root_password: password app: image: golang:1.8-onbuild ports: - "8080:8080" volumes: - ".src/vendor:/go/src/github.com" - "./src:/go/src/app" depends_on: - db-server command: go run cmd/main.go volumes: data:
data volume
Dockerではコンテナを起動し、停止すると基本的にコンテナ内のデータは消えます。 永続的なデータを扱いたい時はData用のVOLUMEを用意します。
volumes: data:
これだけで用意してくれるようです.
今回はmysqlのデータを永続化したいです。
services: db-server: volumes: - "data:/var/lib/mysql" - "data:/var/log/mysql"
このようにdb-serverのvolumesにmysqlのデータ保存先を追加します. 今回はlogも永続化しておきます。
mysqlの下準備を適用する
前半に書いたmysqlの下準備を適用していきます。 dockerのVolumeを用いて、コンテナ内の設定ファイルをローカルのものと置き換えます。
services: db-server: volumes: - "./mysql:/etc/mysql/conf.d" #設定ファイルを置き換える - "./mysql/init:/docker-entrypoint-initdb.d" #ローカルのinitとコンテナのdocker-entrypoint-initdb.dを繋げる - "./mysql/log:/var/log/mysql" #ローカルの./mysql/logとコンテナと/var/log/mysqlを繋げる
ローカルのパス:コンテナ内のパス
という風に書きます。
設定ファイルを置き換えたり、ローカルのディレクトリとコンテナのディレクトリをつなげたりできます。 これによってmy.cnfは置き換えられ、mysqlで出力されたlogはローカルの./mysql/logでも確認できるようになります。
あとは3306portを使用するので、あけておきます
goの下準備を適用する
mysqlと同じです。 volumeを使ってコードと依存パッケージをコンテナ内と共有します。
services: app: image: golang:1.8-onbuild volumes: - ".src/vendor:/go/src/github.com" - "./src:/go/src/app"
気をつけることはそんなにないですが、 goの公式imageでは GOPATHが/goになっているくらいでしょうか
特に意味はないですが、
docker-compose exec app bash
とかで、直接コンテナ内でビルドできたりするのでbuild済みのものを使いました. (一回もしませんでしたが)
あとはこちらも8080ポートを開けておきます
コンテナ同士の接続
今回は, GoコンテナからMySQLコンテナに接続する必要があります。 link(非推奨)というものを使うか、networkというものを使う方法があります. docker-composeのversion3を使うと、 services以下に定義したコンテナ同士はデフォルトで、 同じnetworkによしなに属してくれます。
名前は,
services: app: #ここ .... db-server: #ここ ....
のものが使われます。
なので、片方のコンテナから(例えば、今だとappのコンテナから)
ping db-server
するとちゃんとpingが通ります.
動かす
一思いに,
docker-compose up
します。
docker-compose.ymlにdepends_onと書いていると思うのですが、 起動する順番が決まるだけで、mysqlが起動するまで待ってくれないようです。
少し待ってから, http://localhost:8080/pingにアクセスすれば、 mysqlから取得したデータが入ったjsonが返ってきているはずです.
リガチャー(合字)が使えるエディターを適当に見てみた
リガチャ使っていますか？
これ
が
こうなります。
カッコ良いね、コード書きたくなるね
リガチャ
複数の文字を一つの文字として、 表示してくれます。
最近話題になっている気がしますが、 以外と使えるエディターが少ない？気がしたので調べてみました。
美しい環境はやる気に繫がると思いますので、 ぜひ使ってみてください。
今回は都合で(めんどくさくて)macでよく使われている気がする エディタ(IDEも見ます)を調べてみました。
いろいろなリガチャーがありますが、 今回はFira Codeの
=> -> >= <= == := ~= ~> <!-- -->
だけ見ていくことにします。
atom
さすがatomですね〜
綺麗に使えます！
注意
v1.0.0から正式に使えるようです。 updateしてなかったらupdateしてね
IntelliJ
使えますね。 エディタというよりIDEですが、 気にしません
versionはver2016.3.4です
こちらの記事 見るととてもわかりやすいです。
Eclipse Neon.2
使えますね〜 versionは4.6.2
iterm2
こんな感じ。
ちょっと変ですね、
というのも、
まだNightly Buildsでしか使えません。
まあそれでも使いたいvimmerなら使いましょう 僕はvimmerなので使います。
使えなかったもの
- sublime くらい
最後に
結局 4つくらいしか見てません。
というのも、 Fira Codeのgithubページ を見ると 対応しているものがだいたい書いてます。（書いてる途中に思い出した）
ですが、eclipseは使えないと書いてあったりするのと、 リガチャーの啓蒙のために投稿します。 (せっかく書いたし)
対応しているのが少ない気がしていたけれど、 なんだかんだで結構対応してましたね。
SICP
SICP勉強会してるので、 気が向いたら知見書いていけたらなぁと
exe2.63
(define (tree->list-1 tree) (if (null? tree) '() (append (tree->list-1 (left-branch tree)) (cons (entry tree) (tree->list-1 (right-branch tree)))))) (define (tree->list-2 tree) (define (copy-to-list tree result-list) (if (null? tree) result-list (copy-to-list (left-branch tree) (cons (entry tree) (copy-to-list (right-branch tree) result-list))))) (copy-to-list tree '()))
問題はtree->list1とtree->list2が同じリストを生成するのか、 オーダーはどうかである。 生成されるリストは順序ありリストという縛りがある。
前者は、生成されるリストは 一意に決定されるので、一つに定まる。
後者は、 tree->list1は
こんな感じの順番で評価される
tree->list2は
はこんな感じ.
これだけの違いしかなく、 それぞれ要素数nの場合 tree->list1はn回、 tree->list2(copy-to-list)もn回呼ばれる。
ここでtree->list1はappendを用いてlistの結合をしているので、 さらにO(n)かかる。 tree->list2はconsで済んでいる。
結果的にtree->list1は O(n2)、 tree->list2は O(n)
ハフマン木が面白かったから、 そこまで書こうと思ったけど疲れたから終わり
fishでVundle使うときの罠
shellをfishに変えて意気揚々とvimのプラグインを追加して:BundleInstallすると次のようなエラーがでる
Error detected while processing function vundle#installer#new[24]..<SNR>59_process[11]..vundle#installer#run[8]..vundle#installer#install[12]..<SNR>59_sync[6]..<SNR>59_make_sync_command[4]..<SNR>59_get_current_origin_url[3]..<SNR>59_system:
まあ正直エラーメッセージでググれば解決できるのだけれど、英語ばっかりだったし、メモ。
zshやbashを使っていると出ないエラーみたいなので、fishの関数が何やら悪さをしているっぽい？
ともあれ、
.vimrcの最初の方に
set shell=/bin/bash
と書いておけばおk
shellをvimrc読み込むときだけ、切り替えている
