Macのストレージを空けた

今使っているMacはMacBook Proの256GBフラッシュストレージモデルで、いくらでもファイルを保存できるという感じではない。購入から1年近く経った今、90%以上の領域を使ってしまっている。そこで、使用頻度の低いファイルを外付けHDDに追い出したり、使わなくなった古いバージョンのソフトウエアを積極的に削除していくということが必要になる。

Haskell Platform

~/Library/Haskell 以下にいろいろ入っている。
$ du -h -d 2 Library/Haskell で調べた感じ、古いGHC 7.6.3が1.3GBほど占めているようだった。なので古いGHCを消す。
手順はMac OS X – HaskellWikiをみた限りでは uninstall-hs コマンドを使えばいいらしい。

$ du -h -d 2 Library/Haskell
144K	Library/Haskell/bin
 26M	Library/Haskell/doc
1.3G	Library/Haskell/ghc-7.6.3/lib
1.3G	Library/Haskell/ghc-7.6.3
3.2G	Library/Haskell/ghc-7.8.3/lib
3.2G	Library/Haskell/ghc-7.8.3
188K	Library/Haskell/logs
203M	Library/Haskell/repo-cache/hackage.haskell.org
156M	Library/Haskell/repo-cache/hdiff.luite.com
359M	Library/Haskell/repo-cache
4.9G	Library/Haskell
$ uninstall-hs -v
-- Versions found on this system

7.6.3
    /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64
    /Library/Haskell/ghc-7.6.3
    /Users/*/.ghc/x86_64-darwin-7.6.3
    /Users/*/Library/Haskell/ghc-7.6.3

7.8.3
    /Library/Frameworks/GHC.framework/Versions/7.8.3-x86_64
    /Library/Haskell/ghc-7.8.3
    /Library/Haskell/ghc-7.8.3-x86_64
    /Users/*/.ghc/x86_64-darwin-7.8.3
    /Users/*/Library/Haskell/ghc-7.8.3

-- To remove a version and all earlier: uninstall-hs thru VERSION
-- To remove only a single version:     uninstall-hs only VERSION

$ uninstall-hs only 7.6.3
-- Would remove just version 7.6.3
/Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64
/Library/Haskell/ghc-7.6.3
/Users/*/.ghc/x86_64-darwin-7.6.3
/Users/*/Library/Haskell/ghc-7.6.3
/Users/*/Library/Haskell/bin/cpphs@ -> ../ghc-7.6.3/lib/cpphs-1.18.4/bin/cpphs
/usr/bin/ghc-7.6.3@ -> /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/bin/ghc-7.6.3
/usr/bin/ghc-pkg-7.6.3@ -> /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/bin/ghc-pkg-7.6.3
/usr/bin/ghci-7.6.3@ -> /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/bin/ghci-7.6.3
/usr/bin/haddock-ghc-7.6.3@ -> /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/bin/haddock-ghc-7.6.3
/usr/bin/runghc-7.6.3@ -> /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/bin/runghc-7.6.3
-- To actually remove these files, sudo run the command again with --remove
-- To generate a script to remove these files, run the command again with --script

$ sudo uninstall-hs only --remove 7.6.3
Password:
-- Removing just version 7.6.3

そもそも今インストールされているGHC 7.8.3も最新版じゃないという気がするが。

TeX Live (MacTeX)

古いTeX Live 2013が入っていたので消す。確かMacTeXで入れたような気がするので、このへんを読んでおく。普通に /usr/local/texlive/2013 を消せばいいみたい。

$ du -d 1 -h /usr/local/texlive
4.4G	/usr/local/texlive/2013
4.5G	/usr/local/texlive/2014
4.0K	/usr/local/texlive/texmf-local
8.9G	/usr/local/texlive
$ sudo rm -rf /usr/local/texlive/2013

その他

Homebrewで入っている古いソフトウエアを消したりMacPortsで入っている古いソフトウエアを消したり、Dropboxで同期しているでかくて使用頻度の低いファイルを同期しないようにしたりいろいろ

コマンドラインでJPEGファイルのEXIF情報を取り除く

Webに写真を載せる時とかにEXIF情報は削除しておきたい。

以前はImageMagickのconvertコマンドで convert -strip とやっていたがどうやらこれは画像の再圧縮がかかるようだ(strip後の方がファイルサイズが大きくなったりする)。

ググったらそれっぽいStack Overflowの質問が出てきたのでメモしておく。

何種類か回答が寄せられているが、自分の環境にはexiv2を入れた覚えがあったのでexiv2の方法をやってみた。コマンドは

$ exiv2 rm (JPEGファイル)

となる。JPEGファイルは上書きされるので注意。

MacPortsを使っていればexiv2は $ sudo port install exiv2 で入るはず。

Idrisの有界な自然数で遊んでみる(1) — 証明をつける

前回:Idrisの有界な自然数で遊んでみる(0)

前回はIdrisで「有界な自然数の冪乗を計算する」finPower2 : Fin n -> Fin (power 2 n) という関数を実装したが、いくつか後回しにした証明があった。今回はIdrisの証明支援機能を使ってこれを埋める。

続きを読む

Idrisの有界な自然数で遊んでみる(0)

プログラミング言語Idris自体についての詳しい話はここではしない。このブログの昔の記事で軽く紹介したかもしれないが他人の参考になるかは分からない。

この記事を読むにあたっては、

  • ペアノ算術

は知ってないと厳しいと思われる。あとHaskell風の言語にも慣れていた方がいいか。

この記事で使うIdrisのバージョンは0.9.16である(執筆時点の最新版)。これと異なるバージョンだとコードの修正が必要かもしれない。

続きを読む

Union Typesは直和型ではない

【2017年12月18日 追記】この記事は古いTypeScript (2.0以前) を念頭に置いている。もちろん、現在のTypeScriptにも当てはまる記事はあるだろうし、TypeScript以外の言語における合併型 (union types) についてもある程度読み替えられるかもしれない。ただしElmとは “Union Types” の用法が完全に相入れないのでElmユーザーの方はお帰りください。


TypeScript 1.4について、 TypeScript 1.4.1 変更点 – Qiita という記事が目に留まった。で、その中の
直和型(Union Types)
という項目に引っかかりを感じた。:

なぜ引っかかりを感じたかというと、TypeScriptに今回導入されたUnion Typesと、巷に言う直和型というのは、異なる概念であるからだ。

注意:以下の話は型理論の専門家でもないフツーの学生が適当に書いた程度の信憑性しかありません。

続きを読む

TypeScript 1.4がいい感じ

TypeScript 1.4がリリースされた。目玉機能としては Union Types とか ECMAScript 6 出力モードの搭載とかになるのだろうが、他にもいろいろ地味だが嬉しい機能追加などがあるようだった。

前にTypeScriptで組み込みオブジェクトを拡張できないというようなことを書いたが、そのとき感じた問題点が直っている。具体的には以下。

  • 各種組み込みオブジェクトのコンストラクタの型が interface ほにゃららConstructor というものに変更されている。よって、各種組み込みオブジェクトのコンストラクタに勝手なプロパティーを追加できる。
  • ECMAScript 6 で追加される関数の型定義が追加されている。つまり、自前で組み込みオブジェクトの型定義をいじらなくていい。(ECMAScript 6 出力モードで使えるようになるようだ)

あと地味に便利だと思ったのはコンパイラ tsc に追加された --noEmitOnError というオプションである。今まではソースコードが解釈さえできれば型チェックが通らなくても ECMAScript の出力が生成(!)されていて、Makefile で TypeScript のコードをコンパイルする時に不便だった。だが、このオプションがあれば型チェックが通ったコードしか出力されないので、Makefile との相性が上がる。

Rustから直接C++を叩いてみる

プログラミング言語Rustのα版が出たので遊んでみようかなという。(と言ってやってることはRustである必要性が全然ないけど)

ここで使っている環境はOS X 10.9.5 (アーキテクチャはx86_64)で、C++コンパイラはClangである。ここでやっているのは激しく環境依存なのだが、まあでもコンパイラがGCCかClangなら多くの環境で上手くいくんじゃないかと思う(知らん)。

続きを読む

TeX処理系の気に食わない点(0) — エラー時の挙動

明治維新で新政府がTeXを旧来の陋習として弾圧したとき、TeX使いたちはわざとTeXの使い勝手を悪くすることで難を逃れたと伝えられています。 — TeXしぐさ

↑「適当にでっち上げた嘘です」と注記しようと思ったが元ネタも適当にでっち上げた嘘だった

TeXの気に食わない点…はきっと皆さんいろいろあると思うが、ここではTeX処理系の挙動に絞った話をする。ここに書いた挙動に関しては、TeXpdfTeXXeTeXも大差はないようである。

続きを読む

一次分数変換と球面の回転の話(0)

\(\require{AMScd}\def\Real{\mathbf{R}}\def\Complex{\mathbf{C}}\newcommand{\abs}[1]{\left\lvert #1\right\rvert}\)次の形をした複素関数 \(f\) を一次分数変換という:\[
f(z)=\frac{az+b}{cz+d},\quad \text{ただし \(ad-bc\ne0\).}
\]分母が0になるとき(\(z=-d/c\) のとき)は \(f(z)\) の値は複素数としては定まらない、のだが、値が複素数であることにこだわらなければここは \(\infty\) としておくのが都合がいい。逆に、\(z=\infty\) のときは、(\(z\to\infty\) の極限を考えれば分かるように)\(f(z)\) の値は \(a/c\) として定義できそうである。何がいいたいかと言うと、一次分数変換は、複素平面の関数というよりは、複素平面に「無限遠点」を加えたもの \(\Complex\cup\{\infty\}\) の関数をみるのが自然である。

複素平面に無限遠点を加えたもの \(\Complex\cup\{\infty\}\) は、球面と同一視できる(こうやって同一視したものをリーマン球面という)。球面上の点 \(P\) に複素平面の点 \(z\) をどう対応させるかというと、球の北極 \((0,0,1)\) から \(P\) に直線を引いて、その直線が複素平面と交わる点 \(z\) を対応させる。逆に、複素平面の点 \(z\) に対しては、\(z\) と北極 \((0,0,1)\) を結ぶ直線を引いて、それが球面と交わる(北極じゃない方の)点 \(P\) を対応させる。北極に対応する点は複素平面上にはないので、北極には無限遠点 \(\infty\) を対応させる。この対応を立体射影(stereographic projection)という。
projection-fig
続きを読む

SO(2) と SO(3) が弧状連結であることの簡便な(?)証明

\(\def\Real{\mathbf{R}}\def\Complex{\mathbf{C}}\newcommand{\ip}[2]{\left\langle #1,#2\right\rangle}\newcommand{\vect}[1]{#1}\def\Ker{\operatorname{Ker}}\newcommand{\restrict}[2]{\left.#1\right\rvert_{#2}}\newcommand{\transpose}[1]{{#1}^T}\newcommand{\abs}[1]{\left\lvert #1\right\rvert}\)特殊直交群 \(SO(n)\) が(弧状)連結であることを示すのはこの記事に書いたやり方がおそらく正攻法なのだろうが、次元が低い時はもっと短い議論でできるんじゃないかなあと思った。

命題. \(SO(2)\) の元 \(A\) は次の形に書ける。\[
A=\begin{pmatrix}
\cos\theta&-\sin\theta \\
\sin\theta&\cos\theta
\end{pmatrix}
\]
証明. \(A\) を成分表示して \(SO(2)\) の条件の式に代入してガリガリ計算すればわかる。
定理. \(SO(2)\) は弧状連結である。
証明. さっきの命題を使えば簡単。

続きを読む