Coq 8.6のインストールほか
Coq 8.6をインストールしたときのあれこれ
Coqのインストール
これの通りにやるだけ
aptのパッケージは古いからだめってあったので言われたとおりにopamでいれた
それと~/.opam/4.04.0/binにパスを通すのもやった.
どうもopamはバージョンごとにbinディレクトリを分けてるみたいなのでバージョン上げるときは注意(面倒だからやめてほしい).
ssreflectを入れた場合は
From mathcomp Require Import ssreflect.
が通るかを確認.
ProofGenral
基本は上の通り.
Input methodをAgdaにした(unicode symbolsをカジュアルに使うため, TeXでもいいけど最高に使いづらかったのでAgdaにした).
当然のことながらagda-modeが入ってるのが前提
;; proof general (when (file-directory-p "~/.emacs.d/lisp/PG") (load "~/.emacs.d/lisp/PG/generic/proof-site") (require 'agda-input) (add-hook 'proof-mode-hook (lambda () (set-input-method "Agda"))))
以上.
とっても簡単.
minecraft 1.11 MOD開発メモ
1.11準拠のMOD開発に関するメモ
詳しいことは自力で調べてね的なスタンス
概要
- proxyを用意して、common proxy側にMOD本体の処理、client proxyに描画関係の処理をかくようにする
- ゲーム内のオブジェクトの管理はすべてﾅﾝﾄｶregistryがやってくれてる だいたいのものは
GameRegistry.registerで登録できるし、新しいレシピはGameRegistry.addRecipeで登録できる - あとforgeが色々イベントフック用の関数を用意してくれているらしいので、バニラのクラスを継承して頑張るよりイベントフックした方が早い場合もあるかも
block
- ブロックとはワールド内に3Dの形で描画されるブロックのこと
- 内部にTileEntityを持てるので、ブロックに対する操作とか特殊なデータを持ちたいとかはTEでやろう
- インベントリに表示されるアイテムはitemblockというまた別のオブジェクトなので、itemblockも併せて登録しないとインベントリには表示されない
- ブロックの見た目に関する設定はblockstate jsonで記述する
- blockstate jsonからはblock model jsonを参照することができて、こちらではより細かい設定ができる 例えば面ごとに違うテクスチャを貼るとか、ブロック自体の高さを変えるとか
- blockはpropertyを持つことができて、それをblockのmeta indexを通してデータをやり取りできるので、例えばユーザーの入力に応じて90度ずつ回転するみたいなことはpropertyでできる
TE
- TileEntityはブロックにもたせてあれこれの処理をさせるためのクラス
- 上で書いたpropertyでは物足りない人のために複雑な情報を処理したりデータを保存したりできる
- データの保存はNBTを使う
TESR
- TileEntitySpecialRenderer
- ブロックの3Dデータを完全に特殊な方法で実装するための仕組み
- mobとかこれでやってる 要は3Dモデルを自分で作りたい時とかに
- MrCrayfish’s Model Creatorとか使うとよいかもしれない
GUI
- GUIはTEから呼ぶ感じになる
- ボタンをつけたりテキストを貼ったりアイテムを表示したりする
- アイテムの出し入れをするインターフェイスはSlotと呼ばれ、Slotを配置しておくことでインベントリを実装したり取り出し専用のスロットを実装できる
参考
自作PC組んだよ2017
構成は次の通り
自分で使うPCを自作したのは初めてだったので色々調べながらパーツを選んだ。
一応個人的な選定基準とかを書いておく。
用途は、主に開発・たまにコンパイルとか動画編集・たまーーーにゲーム とか色々。
パーツ選び
CPU
Core i7-7700、今買う人でそれなりに予算があって普通に使いたいだけならこれ一択な気がする。(Kでもいいっちゃいいけど)
i6-6500あたりとちょっと迷ってたけど、メモリ32GBを諦めて浮いたお金でグレードアップしといた。
長く使うものでもあるし。
メモリ
16GBと32GBで迷って、まぁ足りなかったら増設すればいいだけだし、という理由でひとまず16GBにした。
32GB=1人権という単位(誰が言い出したんだこれ)があるらしいけど、まぁ普通に使うだけなら16で枯渇することは多分ないしいいかってなった。
一応スロットまだ空いてるしそのうちもっと欲しくなったら買うかって気持ち。
マザーボード
ググったらH170がいいよって話があったのでそうするかってなって、Intelラピッドなんとかという技術でSSDとか早くなるらしいって聞いたのでH270のこれにした。
したけど後述の理由によりこのIntelラピッドなんとかは完全に無駄になったのでLinux使う人でH270買う人はお気をつけて。
あと、ネットではまことしやかにATXが主流ですみたいなこと言ってる人が多いけど、
自作PCに多くを求めない人ならMiniATXで十分だと思う。(今更)
ATXだと本体もでかくなるし。
グラボ
コスパでGTX1060。そんなにゲームとかする感じじゃなければ悪くないと思います。
それかめっちゃ値が下がってるGTX960とかも割と買いかもしれないと思ってた。
まぁ先を見据えるなら、これくらい出しておいてもいいかもぐらい。
そんなゲームしない自分にはむしろオーバースペックぐらい。そもそもLinuxって時点で(最近Steamのおかげで対応ソフト増えてるけど)ゲームする気あんまりないし。
思ったよりでかかったので、マザーボードのPCIスロット1つ塞いでしまってる。
これはどうなんだ。
SSD
M2がめっちゃ早いらしいと聞いたのでそうしました。
実際めっちゃ早いけど、前のPCはHDDだったのでM2じゃないSSDとの比較とかはよくわからない。
256GBなのでLinuxシステムに40GBぐらい、あとはゲームとかアプリケーションとかのファイルを置いてる。
あとSSD大容量だとめっちゃ高いし早く2TBが数千円ぐらいで買える時代になってほしい。
HDD
まぁなんでもいいよ(投げやり)
最初は1TBでいいやってなったけど1TBも2TBもそんな変わんないので2TBにしました。(って思ったけど実は2TBも3TBもそんな変わらないという話もある)
ケース
ピカピカ光って中が透明で見えるやつです。
割となんでもよかったんだけど思ったより派手派手になった。あと思ったより大きい。(サイズあんまりちゃんと見てなかった)
結構場所を取るのでそういう意味でもMiniATXで良かった感。
電源
必要な電力の倍ぐらいがいいよって言ってる人がいたので550Wにした。600Wでもよかったけど。
組み立て
ケースのネジがやたら硬くて大変だったことと、
ケースに「ATXはこの穴にとめてね！」って書いてあるやつよりマザーボードが何故か一回りくらい小さくて端がちゃんと固定できませんでした。
おかげでメモリ挿すときボードがたわんで怖かった。
それ以外は普通にすんなりいけた。
BIOS画面がめっちゃ派手で笑った。あとBIOS画面マウスで操作できるのかすげぇって思った。
OSインストール
最初はWindows Server 2016(学生だと無料なので)を入れようとしたら、インストールを開始した瞬間に「ドライバが見つかりません」みたいなエラーに。
グラボのドライバかチップセットのドライバあたりがないのかと思って色々探しまわったけど、そもそもwin serverについての情報がネットに全然なくて(そりゃそうだ)
色々それっぽいのを入れたけどダメでした。
結局あきらめてUbuntu MATEを(前のPCに引き続き)使うことに。またお世話になりますUbuntuさん…。
それと、Ubuntuを入れる際にIntelラピッドなんとかを切ってAHCIモードにしないとSSDを認識してくれなかったのでH270にした意味はありませんでした。(悲しい)
うーむ、Win ServerとHyper-VでLinux環境作ってウハウハする未来を想像してたけど無理だったかという気持ち。
ちなみにKVMでWin Serverは普通に動いた。そういえばGUIはvirt-managerから動かすよりもRDPでwinにつなぐ方が早いらしいよ。
パーティション
次のようにしました
/varとか細かい単位でHDDにしたほうがいいとかそういう話も聞くけど
ちゃんとTRIMの最適化とかしたら別にSSDでも問題ないって話と
HDDに/homeだけ振っとくとある時突然SSDが死んでも必要なものはちゃんと残るから安心だしPC移行するのも楽だよってコメントを見て
こういう感じにしました。
まぁ色々言いましたが普通に使えてるしスペックは十分だしすごい。
じゅうさんまんえんのちからってすげー！(雑なまとめ)
