2014年11月22日

SWI-Prolog-Editor

今いる研究室では、Prologが使われている。
当たり前だけれども、それが問題なわけではない。
ただ、それでもTeraPadで書くというのは、さすがにどうなのよ?と思うわけである。
しかもそれ、Perlモードだから。(拡張子が.plのため)

というわけで、軽くエディタを調べてみることにした。
真っ先に出てきたのはEmacsだったが、TeraPadを使っているのでちょっと、と思ってしまった。
次に出てきたのがこれ、SWI-Prolog-Editor
名前の通り、SWI-Prologを前提とした開発環境。
エディタの説明は上のリンクから公式サイトに行ってもらうとして、入れる際の注意と入れたあとの注意を。
・32bitのSWI-Prologしか対応してない。別に64bit OSでも32bitのPrologが動くのでそっちを入れれば良いけれど、なんかもやっとすると言うか・・・
・言語設定ファイルが読めるので、日本語翻訳したものを突っ込むとインストールからエディタの起動まで全部日本語でできる。ただし一部の記述のフォントが違うせいで、その部分で文字化けする。
・設定(Configuration)は一度エディタを再起動しないと反映されない。フリーカーソルモードは使わない人も多いだろう。あと括弧の対応表示はほしいところ。設定して、再起動。XPCEのマニュアルがないと保存時に(ドイツ語で)文句を言ってくるけれど、別に普通に動くので問題ない。
・フォントの設定はメニューの設定の真上か、エディタ画面で右クリック。なんで設定の中じゃないんだろう。
・構文要素を斜体(italic)にすると、こいつが斜体にしたときの幅を再計算しないために文字がめり込む。Pとか。できれば全部斜体は解除することをオススメ。

あと思いついたらいくつかここに書く。
言語設定ファイル(一部翻訳不完全・適宜更新)はここに置いておくので必要な人は持っていってほしい。
文字化け対策で、その部分だけ英語にしようかなと考え中。
posted by chiguri at 23:50| Comment(0) | PC

2014年10月27日

透過SOCKS-SSHプロキシ

前回の多段プロキシの試行はHTTPSの前にあえなく撃沈。
問題点は、プロトコルに対するプロキシでは暗号化に対して微妙なんじゃないか?ということ。
透過でなければ(ようはプロトコルをうまく中継してくれれば)問題ないのだけれども。

そこでRedsocksというHTTPSをうまくやってくれるらしいと書いてあるプロキシを試

ちょっとまて、それじゃ本当にHTTPSしかできない。
できれば、いろんなプロトコルを通したい。俺は使っていないけれどLINEとかLINEとかSteamとか。
学生が互いの連絡に使うのだよ、LINE。俺は使ってないけれど。
結局それでは微妙に終わるのだ。

SOCKSプロキシを前回確かめたのは、SOCKSさえあれば一通りのことができるからだ。
そういえばSSHは通るんだったか・・・
ポートフォワード・・・
ふと、SOCKSのまねごとできないの?という疑問が湧いた。

調べたら、-DでほぼSOCKSプロキシとして動作するという。
これに透過プロキシを組み合わせれば解決?といろいろ試行。
結果、できた。構成はこんな感じ。
クライアント--(ゲートウェイ扱い)-->サーバー--(iptablesによるredirect)-->redsocks--(redsocksによる透過プロキシ)-->ssh--(ポートフォワード)-->外部サーバー-->(外部)
結論としては、危険きわまりないので、事情分からない人は絶対に真似をしないこと。

以下、実現の際に詰まった部分のメモ書き。

詰まった点その1:大体の情報源において、ssh -Dはlocalhostでやっている(安全性考えれば当たり前か)。
localhostならいいのだが、他のマシンから送るには、ポートフォワードのために-gを付けなければならない。(そうでないとconnection refused)
結果として、ssh -Nf -g -D 1080というコマンドに。オプションだらけだ。
まあよしとしよう。

詰まった点その2:大体の情報源において、redsocksはlocalhostでやっている(以下略)。
今回は外部に置いているわけだが、そうなると当然透過プロキシにするためのiptablesの設定が微妙に変わる。
もっともきつかったのは、なぜかINPUTチェインのポリシーをACCEPTにしないと通らなかったことだ。
怖いよこの設定!!

改めて見ると、外部でやるような内容じゃない。
セキュリティのずさんさが目に余る・・・
真面目にいろいろ向上させたいところだが、原因がわからないからなあ。
なんにせよ、とりあえず目標の達成をかくにん。
よかった♡(時代に乗り遅れた)

なお、この記事の真似をしてハッキング被害に遭ったとしても私は「ばーか」としか言いませんのであしからず。
危険だともセキュリティずさんだと言っているし。
posted by chiguri at 20:55| Comment(0) | 雑多

2014年10月24日

Squid、透過多段プロキシの試行

今いる研究室は、大学のネットワークポリシーの関係上、直接ではなく大学のプロキシを通してしかインターネットにアクセスできない。
ああ面倒くさい、家のネットワークと大学のネットワークで切り替えなければならんのか、と思いながら過ごして半年、嫌になってプロキシの自動検出(WPAD、DNSの方)を導入した。
これで良いか、楽になったな、などと思っていたら、なぜかFirefoxが「ネットワークが切り替わったとき」に自動判別をしないという非常にアホな仕様だったので、やはり不便が微妙に解消されない。
本気でChromeとかIEにしてやろうか、などと思ったりもした(これらはネットワークが切り替わると自動で判別しにいく)。
え、FirefoxからIEの情報を見に行け?使ってみれば分かるが、自動検出はプロキシの設定をしないのと同じ扱いになる。無用の長物もここに極まれり。

とりあえずブラウザの切り替えは悩むとして、他にないのかと考えることにした。
幸い、研究室のインフラ自体はそれなりに自由に動かして問題ないので(だからWPADを導入した)、ルーター付近で何かできないか、と思ったりした。
いろいろ調べると、透過プロキシというのがあるという。
なるほど、来たリクエストをプロキシとして通す。これなら自分でプロキシの設定がなどといわなくて良い。ゲートウェイがうまくやってくれるわけだ。

ふと気づくと、透過プロキシは直接そのサーバーがアクセスを行うものだった。調べども調べどもその用例ばかり。
これはどうだろうと考えたが、昔そういえば多段串とか聞いた。透過プロキシが多段プロキシとして動作するならどうだろうか?

というわけで、仮想サーバーとしてUbuntu、その上にSquidをインストールし、試してみることにした。
Squidの設定は普通に調べれば出る。
透過プロキシの設定は、待ち受けポートにtransparentを付けるだけ。あとはiptablesで80番ポート行きのパケットをむりやりその待ち受けポートへ投げる。
多段プロキシの設定は、親のプロキシの設定及びアクセス方法を親のプロキシ経由のみに限定。
やってみたところ・・・ビンゴ!
透過多段プロキシによって、プロキシを設定しなくてもHTTPアクセスができるようになった。

・・・80番ポート?あれ、HTTPSは?

調べたら、Squidでの透過プロキシはHTTPSに対応できない、とのこと。
夢、絶たれる・・・

redsocksという(透過)SOCKSプロキシに、なにかHTTPSプロキシがどうの、と書かれているのを見つけたので、機会を見つけてそちらもチャレンジしてみよう。
あ、ちなみに大学のプロキシはSOCKSプロキシではないので、いろんなSOCKSプロキシ通すもの(widecapとかいろいろあるらしいが)は全て使えない。
redsocksも当然SOCKSプロキシとしては使えないわけだが・・・HTTPS使えればだいぶ違うし・・・


おまけ:SOCKSプロキシかどうかはcurl -x socks5://hogehoge という感じでcurlを使ったproxy設定をすることで確かめた。便利だ。覚えておこう。
posted by chiguri at 00:03| Comment(0) | PC

2013年12月25日

進捗アドベントカレンダーを開いた感想

進捗アドベントカレンダー、昨日で全ての記事がそろいました。
参加してくださった皆様、ありがとうございます。
でもやっぱりこんなのに参加するなんて奇特な方々だなあ、と思います。

さて、振り返ってみると、一番手(私)がいきなり出したは良いけどconnpassのページを更新してなかったり、なんだか記事の最初で「なんでこんな企画考えたんでしょうあの人」なんていってきた方がお二方ほどいたり・・・
なんかばたばたしてますね。
しかも皆さんなんだかんだで進捗ありありでしたね。
お一人くらい、「進捗ダメです」画像を五つくらい並べてくるかと思ってたんですが。
・・・ああそうか、始めた人間がくそまじめっぽそうなのを書いてしまったからですね。
空気読んでないのは私でした。申し訳ないです。

まあしかし、日付が変わる前から担当者のTwitterのページを開いて、そこからブログがあればそこも開いておいて、日付が変わってすぐとか、ちょこちょこチェックして、ということをやるのはなかなか楽しかったです。
本人が申告する前にconnpassの更新始めたりとか。

そういえば、申告方法を事前に決めていなかったのにあとで気づいたのが一番の失敗でしたね。
最終的には皆さんが私にtweetすることで私が載せる、という形にしてしまいましたが。

アドベントカレンダーを次にやるとしたら、次の二点を気をつけたいですね。
・担当日をどうするか。参加時点で希望を出した方が楽。Qiitaさんのアドベントカレンダーは参加する日付も指定出来るみたいなのでそっちの方が良かったかな。
・申告、更新方法をどうするか。これまたQiitaさんだと自分で更新できましたね。やっぱそっちの(ry

以上、ちょっとした反省とか所感でした。
これから一週間という短い間の年末、なんとか少しでも進捗を出したいものですね。
posted by chiguri at 00:56| Comment(0) | 雑多

2013年12月14日

Coq/Agdaのどちらを使う?

この記事はTheorem Prover Advent Calendar 14日目の記事です。

さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら

Σ(●△●)<Isabelleの人が一人で大半埋めてるじゃねえか!?

というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。

え、CoqとAgdaのことはnotogawaさんが書いてただろって?
細けえこたぁいいんだよ!

・CoqとAgda、どちらを使うべき?


好きな方を選べば良いと思うのですが、個人的な考えを挙げます。

1:性質+証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関してはAgdaもたくさん使われていますので、それこそ好みでいいでしょう(個人的にはCoqがいいと思いますが)。
2:プログラム記述+検証についてはCoqの方がいいです。こちらは型や関数の記述自体は割と単純であることを想定しています。tacticもいいですし、SSReflectも便利(らしい)です。
3:型を複雑にして、いろいろな性質を型に持たせたプログラミングをしたいならAgdaの方がいいです。Coqだとプログラムを証明と一緒に(tacticで)書く勇気が必要になります(そうじゃないとやっていられません)。慣れればそれなりにできますが、いちいちイライラします。
4:型の階層を意識したいなら断然Agdaです。なにせCoqはSet/Prop/Typeの区別しかしませんし(内部でTypeのヒエラルキーは計算していますが、表に見えづらいです)。

1は比較的どちらでも良いですし、4は迷いようがありません。
したがって、おそらく悩むことが多いのは2/3の問題でしょう。
選択の一助になれば幸いです。

ちなみに、OCamlとHaskellの一方を使っているから、はほとんど理由になりません。
どうせ大した差ではありません。
スタートアップで一日差がつくかつかないかくらいです。

・inversion大好き


inversion tacticは便利です。(すでに何回主張したか忘れた)
簡単に説明すると、inversion tacticは「この帰納的述語が成り立つためにはどういうことが成り立っている必要がある?」というのを定義から見つけてくる優れものです。
このとき、成り立たないパターン(帰納的述語のコンストラクタのパラメータに一致しない)があるときは勝手にそれらに関して矛盾を作って証明してくれます。
(よって「起こりうるパターンが一つもない」、つまり矛盾していれば証明完了するわけですが、それはあくまで結果論)
inversionなかったらCoqの証明を勧めるとかありえませんね。
(ただしinversionの生成する項ははっきり言って読めない)
Agdaで同じこと?・・・reflection使えば、できたりするのかな・・・?

・で、証明しないの?


最近AgdaでD-Case書きまくってるので勘弁してください。
次があったら例題使って、最初の4分類が何を言いたいのか書いてもいいのですが・・・
タグ:Coq Agda
posted by chiguri at 00:14| Comment(0) | Coq