running remote agda

学生のノートPCだと非力で Agda が動かないなので、

VSCode から remote で server 上の動かせば?

と思ったんだが

　　WindowsのPowerShell -> Bat -> ssh -> apptainer exec

なんだけど、apptainer が

　　 Message from stderr when validating the program:
　　INFO: underlay of /etc/localtime required more than 50 (116) bind mounts

とかいう余計な stderr を出す。これを避ける方法がないので諦めました。

まぁ、singurarity の中の emacs で使っとけ。