Singularityにてrakudoのビルドを行う
研究室の同僚に Singularity 教えてって言われた
が、面白そうだしそんなに難しくないかなと思ったので、 そのまま必要としてる環境を作ってみて def ファイル渡すことにした。 (実際、その方が Singularity 使ってる感があったのでそうした)
こちらが rakudo をビルドする def ファイルになります
rakudo-star のイメージを使うのではなく、rakudo のビルドがしたいとのことだった。
というわけでコイツを Singularity build して使えばいい。
BootStrap: docker
From: alpine
%post
apk add --update --no-cache perl git make alpine-sdk
git clone https://github.com/rakudo/rakudo.git
cd rakudo
perl Configure.pl --gen-moar --gen-nqp --backends=moar
make install
image には alpine を使って少しでも軽量にした。(意味があるのかは把握してない) Singularity で環境作るのはかなり簡単で、RTA でもしていたのかって思うくらいには速攻で終わった。 でも実は何度か再走している。
- 最初に
apk addで--no-cacheオプションをつけてなかったので遅かった(1敗) - make している時に build-essential が無いと怒られた(2敗)
makeだけだと prel6 の REPL を実行できなかった(3敗)
Singularity は優秀なんだけど sif をビルドするときにキャッシュに取らないのが玉に瑕…(そのために multi-stage-build 使うのもなぁ…とは思ってる)
おわりに
Singularity は簡単に環境を作れて、さらに今回のようにその環境をまるごと人にパッと渡せる便利なものなので、みんなも使おう！ (ただ、就職したら Singularity 使う場面あるのかなぁ…)
参考文献
Manjaro on WSL で Agda を書こうとしたら特殊文字の文字化けに苦しめられた件
TL ; DR
- 使う理由があり WSL で Manjaroを入れた
- Manjaro on WSL で Agda を書こうとしたら特殊文字で文字化けが発生した
- 最終的にここの日本語フォントを読み込むのとロケールを日本語にするので解決
Windows の環境は全部WSLで何とかしたい
大学に入ってからはずっと macOS や Linux を使っていたので、Windowsのシステムと相容れなくなってしまった。
素のWindowsでプログラミングはあまりしたくないお気持ちが強く、ずっとWSLで完結するようにしていた。
(Windowsだけでプログラミングして、Gitにまで上げてる人は普段何食べてるんだろう…僕の不足した技術力では想像すらつかない…)
唐突にWSLgで研究環境を構築したい欲が！
おととし(2021年)くらいからWSLでもGUIアプリケーションを使えることは小耳に挟んでいた。が、素の Manjaro Linux で今のところ全部やっちゃってるし、今のところはいいかな…と思っていた。
そんな矢先、修論の締め切りが近づくとさすがに「家でも研究のコーディングや執筆とかすすめられたらな…」と思うことが多くなった。(筆者の愛用している Manjaro Linux が入ってる PC は研究室にあり、研究室には昼から朝までいる事ことがよくある。そして研究できる環境は研究室にしかないぞ！)
最初は Windows ラップトップにUSBを付けて、そこに Manjaro をインストールして使っていた。が、Windows OS と行き来するのが煩雑という問題を抱えた。
じゃあWSLでやればいいじゃん！(ということで環境構築していく)
この問題を解決するために、今はWSLgがあるんだし WSL で manjaro を動かして、開発環境(Agda on Spacemacs)を整えようと思った。(Agdaには後述もするが、特殊文字を多用する性質上GUIでやった方が楽)
まずはWSLにManjaroを入れるところから
とても簡単。以下のリポジトリのREADME通りにやればよいだけ github.com (こんなに簡単なら最初からやっておけばよかったな…と思ったのは内緒)
無事にManjaroが入ったなら次はAgdaのインストールだ
Manjaro だと普通に pacman で Agda 各種はインストールできる。
(pacman-mirrors -c Japanとかで早い順でミラーリポジトリをソートしたり、このタイミングで /etc/pacman.conf でパッケージのダウンロードを並列化すると幸せになれる)
sudo pacman -S agda agda-stdlib emacs
そのあとはspacemacsをインストールする
一応emacsを立ち上げてみると、GUIでspacemacsが立ち上がると思う。(この際、初期設定とインストールが挟まる。)
その後、emacsにemacs-agda-modeを入れるためにagda-mode setupを実行する。一瞬emacsが立ち上がったと思ったら消えたらだいたい成功してる。
そしたら以下のコマンドを入れてStanderd libraryの設定を完了する。(standard-library.agda-libの場所はmacとかだと違うので要注意)
mkdir -p ~/.agda echo /usr/share/agda/lib/standard-library.agda-lib >>~/.agda/libraries echo standard-library >>~/.agda/defaults
ちゃんと入ってるかの確認は test.agda を spacemacs で新規作成して以下を書いて C-c l するとわかる。 (C-c lの指の動きはコントロールキーを押しながらcキーを押す。その後押しているキーは離してlキーを押す)
module test where open import Data.Nat
文字化けの解消(問題はここからだった…)
書いていたagdaファイルを開いたところ、日本語が文字化けしていた。
あーじゃあ sudo pacman -S otf-ipafont の実行で直るのでは？->結果、日本語は表示されるようになったが、Agda 上で使用している特殊文字は文字化けしたままだった。
四角の中に数字が入っている僕が見たことない文字の化け方をしていて、色々試してみた結果、Win11のWSL2 (WSLg)を日本語化 & Mozcで日本語入力 | AsTechLogに
Windows側にインストールされているフォントをWSL2側でも参照する...
とあり、これとその下にあるロケールの日本語化で特殊文字も正常に表示されるようになった。 こんな方法わかるなんて元記事の人は天才かもしれないな…
いかがでしたか？
これでWindowsのWSL環境で立ち上げたManjaroでWSLgを使ってspacemacsにてAgdaを書くことができるようになったぞ！
それでは良きAgdaライフを！
余談
最近なぜかvimモードでもhybridモードでもemacs-agda-modeが動かない…(しかたなくemacsモードにしている)
参考文献
(下の方で万事解決～と慢心していたら案の定特殊文字が文字化けして足元を掬われた)
(特殊文字なんか使わないよ、という方には下の解決法で事足りるかもしれない…)
バックアップを取っていたから軽傷で済んだ話
昨日、突然デスクトップPCがネットワークに繋がらなくなった
いろいろ疑ったりしながら調査した結果、どうやら以前設定したネットワークブリッジがDHCPから割り当てられるipをぶんどっているようだった。
よしじゃあこのブリッジを消してしまえばいいじゃん！と思ったところ、消してもネットワークに再接続しようとするたびに謎に復活してきた。(おかげで永久にネットワークに繋がらない…)
systemctlにそれっぽいもの(ブリッジを復活させてそうなservice)があったのでそれを消してみるもだめ、そこから再起動してもだめだった。
すぐに出る最終手段
修論書かないといけないのにこれ以上こんなことに時間を取られるのもな…ということで、多少強引ではあるがそのブリッジの設定をしていた時期よりも前の日まで環境を巻き戻すことにした。
基本的に書いたコードやらなんやらはgitとかのvcsに置いてあったので何も考えずに戻せた。(本当に戻したらダメなものがあるのか考慮する力があったのかは謎)
バックアップはtimeshiftで自動的に取るようにしていたが、リストアするのもポチポチで簡単だった。
で、戻したら消したがっていたブリッジの設定も存在せず、無事にネットワークにも接続することができた。わーい
今回初めてリストアをしてみた知見
timeshiftはバックアップ取る周期の設定も楽だし、こんなにもリストア簡単だったのかと思った。
あとはHDDにバックアップを取ってもリストアが思っていたより高速だった。m.2が貰い物で128GByteしかないのも原因にあるかもしれないが、それでも10倍くらいは待てそうな感じだった。
ということで
なんとなくで取っていたバックアップに助けられた話と、書いたものはgitとかに送っておくとリストアもしやすくて良いという話でした。
