誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「WindowsへのCoqのインストール」： 事情があって、AgdaかCoqを触ってみようか、と。 事情というのは、個々の命題の証明（確認）は割と簡単そうだが、命題がイッパイあるのでウンザリな状況のことです。家計簿の計算が筆算だと面倒だから電卓を使いたい、という状況と同様です。 それでCoqのインストールは済んだのですが、処理系の使い方が分からない。個々の操作は覚えていけばいいのでしょうが、そもそもCoq処理系が何をするものなのか？ が理解できないのです。Web上にCoqの解説は幾つもあるのですが、「いやいや、そうじゃなくて、それ以前のことがサッパリわからんのですけど」という感じ。スタートラインに立てない。 それで、「Coqの解説」じゃなくて「Coqの仕様」を読んだほうがいいのかも、と https://coq.inria.fr/distrib/current/refman/ （リファレンス
なぜHTTPSはHTTPより速いのか
先週、httpvshttps.com というウェブサイトが公開されました。このウェブサイトでは、HTTP と HTTPS を用いてアクセスした場合のウェブページのダウンロード完了までにかかる時間の比較ができるのですが、多くの環境で HTTPS の方が HTTP よりも高速なことに驚きの声が上がっていました。 HTTP が TCP 上で平文を送受信するのに対し、HTTPS は TCP 上で TLS (SSL) という暗号化技術を用いて通信を行います。ならば、TLS のオーバーヘッドのぶん HTTPS のほうが遅いはずだ、という予測に反する結果になったのですから、驚くのも無理はありません。 実は、この結果にはからくりがありました。 Google Chrome、Mozilla Firefox、最近のSafari注1は、Google が開発した通信プロトコル「SPDY」に対応しており、HTTPS
Ruby でラインメモリプロファイラ - Qiita
プロファイラ好きなモニタの前の皆さんこんにちは。@sonots です。この記事では、Ruby コードのどの行がどのぐらいメモリを消費しているか調べる方法を紹介します。 オブジェクトの数を数える Ruby には ObjectSpace というオブジェクトの情報を集めたり操作したりする module があります。 このモジュールの each_object メソッドを使用すると、RubyVM 上の全てのオブジェクトを取り出すことができます。 このメソッドを使って、以下のようなコードを書くと、実行した地点で、RubyVM 中にどのクラスのオブジェクトが何個存在しているのかカウントできたりするわけです。興味深いですね! ObjectSpace.each_object.inject(Hash.new 0) {|h,o| h[o.class]+=1; h } #=> {Class=>241, Strin
ノートPCをサーバーにして大惨事になった話 | vps比較メモ
ボクには黒歴史がある。 WEBエンジニアとして働き始めた頃の話だ。 当時は、社内のお荷物的なキャラだった。 外注で客先に行ってはクレームが入り、社内に出戻りするような日々を送っていた。 社内の居心地も悪く、何とか這い上がろうと必死に勉強していた時期でもある。 ただなかなか勉強した成果が出ない。 そんなとき「自宅サーバを立ててWEBサイトを公開すると実践的な勉強ができる」と聞いた。 早速試してみた。 しかしこの安易な考えが、ボクの黒歴史を作ることになってしまう・・。 ノートPCが起こした大惨事 朝、会社への通勤途中にアパートの大家さんから電話がかかってきた。 大家「キミの部屋燃えてるから！」 自分「え！？」 大家「キミの部屋が燃えてるから早く帰ってきて！」 自分「え！？」 大家「いいから早く戻ってこい！」 自分「え！？あっは、はい！」 ボクは、上司に事情を話し会社に行けないことを伝えると、す
iPhoneを使うなら覚えておきたい！ iTunesでできる5つの便利技まとめ
どうもハンサムクロジです。 iPhoneを使っているうえで切っても切り離せないのが、PCにインストールして利用する「iTunes」。 使用しているiPhoneのデータをバックアップ・復元したり、端末の管理や音楽の同期など様々なことができます。 今回は、この「iTunes」を使ううえで覚えておきたい5つの便利技をまとめてご紹介したいと思います！ 1.Apple IDで認証したコンピュータをリセット Apple IDに紐付けられる端末は10台（うちPC5台）までとなっています。認証している端末がいっぱいになってしまった場合や、売却済みの端末が認証されたままになっている場合は、それら認証した端末のリセットを行いましょう。 iTunesを起動して右上にあるボタンをクリック。表示されるメニューからアカウント情報を選択します。 Apple IDとパスワードを入力してサインインしたら、ページをスクロール
RubyとRailsにおけるTime, Date, DateTime, TimeWithZoneの違い - Qiita
RubyとRailsにおけるTime, Date, DateTime, TimeWithZoneの違いRubyRails 2021.2.11追記：DateTimeクラスは非推奨なクラスになりました DateTimeクラスは非推奨なクラスとなり、DateTimeクラスではなくTimeクラスを使うよう、公式にアナウンスされました。 参考1 But we consider use of DateTime should be discouraged. - matz (Yukihiro Matsumoto) https://bugs.ruby-lang.org/issues/15712#note-4 参考2 DateTime は deprecated とされているため、 Timeを使うことを推奨します。 https://docs.ruby-lang.org/ja/latest/class/DateT
47NEWS（よんななニュース）
北陸新幹線の敦賀延伸だけじゃない、２０２４年の鉄道の注目イベントは？ 新型車両や新観光列車が続々、東海道新幹線は開業６０年「鉄道なにコレ！？」【第５５回】
服装がダサい人の特徴と、唯一の改善策
「服なんて何着ても一緒、結局顔だろ顔」 高い服着たブサイクと、安い服着たイケメンの画像が2ちゃんねるにあったけど、この手のことを言う人はほぼ間違いなくダサい人だと思います。 そう見えるのは、服を見る目がボヤけてるからです。 ド近眼の人がちょっと離れて人を見ると、白いシャツを着ているなとか、青いジーンズを履いているなとか、服を漠然としか認識できないのとまるっきり一緒で、ダサい人はそれがバンドオブアウトサイダーズの３万円する白のオックスフォードシャツであろうと、2000円のユニクロの同じシャツであろうと、値札を見るまで違いがわかりません。同じ白いシャツと思ってるのです。 だからか、ダサい人はメニューの多い安っぽいファミレスみたいに、いろんな服に手を出しがちです。一杯のおいしいコーヒーを飲むよりも、ドリンクバーで不味いいろんなジュースを飲む方が嬉しいんでしょう。 例えば変な形のシャツだとか、変わ
Rubyによるクローラー開発技法 巡回・解析機能の実装と21の運用例 読んだ - hitode909の日記
Rubyでインターネットを巡回する本． いちばん簡単なのだと，Wgetで再帰的にダウンロードしてみましょうとか，Anemoneっていうクローラ作るためのライブラリとか，ThreadやEventMachineで並列に動かすとか． あとは，Rubyだからgemの便利グッズが紹介されていて，一番よかったのは，koalaっていうfacebookにアクセスするためのライブラリで，キラキラネームでまぶしい． 気になったのは，けっこうHTMLをXPathとかで取り出してスクレイピングしていることで，こういう方法だとしばらくすれば壊れそう．壊れたときに気付けるように結果もバリデーションしましょう，とか書いてあったけど，メンテナンスできるのか．それか，意外とマークアップ変わらなくて壊れないもの? スクレイピングというと2007年くらいにPerlの人たちがCPANでYoutubeをダウンロードとかいって喜んで
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
https://qiita.com/kenokabe/items/618692858044a89adbc0
Loading...