Agda のモジュール読み込みのエラー

Agda のモジュール読み込みのエラー

Agda 2.5.2 で import my-module-file as M のようにしてファイルを開こうとすると 、

Module cannot be imported since it has open interaction points
when scope checking the declaration
  import my-module-file as M

というエラーが出ますが、これは元ファイル (my-module-file.agda) に示すべき Goal が残っているのが 原因のようです。 Hole を埋めてあげて、*All Done* の状態にしてあげればモジュールとして読み込めました。

bash の補完機能は inputrc で

bash の補完機能で大文字と小文字の区別をなくす

bash でファイル名をタブで補完するとき、Windows の Git Bash みたいに大文字小文字 の補完を自動でやってくれるようにしました。

set completion-ignore-case on

というのを ~/.inputrc というところに書いて読み込ませればOK。 inputrc って便利なんですね…!

Bibtex 備忘録

文章を書いた TeX ファイルに何を加えれば参考文献を表示できるか、忘れないようにメモしておきます。

前提

Makefile を利用しています。

手順

1. TeX ファイルに参考文献を付け加える

メインの .tex ファイルの \begin{document}\end{document} で挟まれてる部分に、

\bibliographystyle{jplain}
\bibliography{paper} % paper.bib というファイル名なら paper とかく

を加える。jplain は日本語論文でABC順で文献を並べるという意味。 詳しくは http://ideas.paunix.org/latex/latex_6_bib.htm#bibstyle をみるべし。

2. Makefile を編集

Makefile をこんな感じにする。

.SUFFIXES: .tex .pdf

all :
    @echo usage: make filename.pdf / make clean

.tex.pdf :
    platex $<
    pbibtex $*
    platex $<
    platex $<
    dvipdfmx $*

clean :
    rm -f *.ps *.bak *.dvi *.aux *.log *.toc *.bbl *.blg *.out *.ptb

3. Bib ファイルを作る

英語論文の引用の場合、タイトルの中でアルファベットを大文字にしたいところを {} で囲ってあげればよい。

@InProceedings{文献名,
  title={{T}itle {O}f {T}he {P}ublication},
  author={著者},
  journal={ジャーナル},
  pages={227--238},
  year={2000}
}
  • このフォーマットを自分で書くのは時間の無駄なので、Google ScholarChrome 拡張が非常に便利。 chrome.google.com

  • @InProceedings, @article, @book, @phdthesis などはよく使う。

  • pages, author などは PAGES, AUTHOR と大文字で書いても問題ない。
  • 自分の過去の論文を引用したいが、これから収録される場合は note={to appear, 11 pages} などとすればいいらしい。

4. 引用する

.tex ファイル中で \cite{文献名} とする。引用が一つもないと、次のように「一つも引用してませんよ!」 とエラーを出してくれるので、とりあえずダミーの引用でも入れておけばよい。

This is pBibTeX, Version 0.99d-j0.33 (utf8.euc) (TeX Live 2017)
The top-level auxiliary file: ppl19.aux
The style file: jplain.bst
I found no \citation commands---while reading file ppl19.aux
Database file #1: paper.bib
(There was 1 error message)

stack build でエラーが出る

Haskell のパッケージ管理システム便利版の stack というものをいじっていてビルドしようとした際に出たエラーの対処法です。

cabal の他に新しくできた stack というものは、パッケージ依存性の問題(cabal hell)を解決するようにできているそうです。便利。

haskell.e-bigmoon.com

(↑stack の使い方、なぜstackを使うべきかなどが詳細に書かれていますので、 stack の説明は上記のページにお任せすることにします)

stack build できない

stack では、YAML形式の設定ファイルを読み込んでビルドしていくのですが、それを行おうとすると構文解析に失敗します。

Could not parse '(略)/stack.yaml':
Aeson exception:
Error in $['extra-deps'][0]: failed to parse field 'extra-deps': expected PackageIdentifier, encountered Object
See http://docs.haskellstack.org/en/stable/yaml_configuration/

エラーによれば、extra-deps の一つ目で詰まったようです。私のファイルでは

extra-deps:
  - git: [リポジトリのURL]
    commit: [特定のコミット]

という部分の - git: と書いているところが怒られていて、ここにはパッケージの名前が入るべきだと言われていますが、ネットで調べた限りはこれは一応書き方としては間違っていないようですね…

stack のバージョンをあげる

原因は stack のバージョンがあまりにも古いことにあったようです。調べたところ私の stack はなんと version 1.3.2 (2016年12月) でした。 version 1.5.1 よりも古いと上記のエラーが出てしまうみたいです。

$ stack upgrade
Current Stack version: 1.3.2, available download version: 1.9.1
Newer version detected, downloading
Querying for archive location for platform: osx-x86_64-static
Querying for archive location for platform: osx-x86_64
Downloading from: https://github.com/commercialhaskell/stack/releases/download/v1.9.1/stack-1.9.1-osx-x86_64.tar.gz
Download complete, testing executable
Version 1.9.1, Git revision f9d0042c141660e1d38f797e1d426be4a99b2a3c (6168 commits) x86_64 hpack-0.31.0
New stack executable available at (ホームディレクトリ)/.local/bin/stack

新しい stack がダウンロードできたので、/usr/local/bin の stack のリンクを貼り替えます。 リンク先のパスを知るには readlink コマンドが使えます。

$ readlink stack
/Library/Haskell/ghc-8.0.2-x86_64/bin/stack

正しくリンクを貼り替えられたようです。この後、stack build もうまくいきました。

$ stack --version
Version 1.9.1, Git revision f9d0042c141660e1d38f797e1d426be4a99b2a3c (6168 commits) x86_64 hpack-0.31.0

tlmgr: Remote repository is newer than local に対処する

TeX のバージョンアップを要求される

TeX のパッケージマネージャーである tlmgr のバージョンが 2017 から 2018 に上がったために古いものはサポートされていないようです。

$ sudo tlmgr update --self
tlmgr: Remote repository is newer than local (2017 < 2018)
Cross release updates are only supported with
  update-tlmgr-latest(.sh/.exe) --update
Please see https://tug.org/texlive/upgrade.html for details.

そこで、以下のいずれかの選択肢があるのですが…

  • tlmgr そのものを 2017 から 2018 にアップグレードする
  • 2017 のまま使い続ける

セットアップがめんどくさいという非常に後ろ向きな理由ですが 2017 のリポジトリに固定して使い続けてみます。

リポジトリを固定する解決策

以下の方法にしたがってリポジトリを固定し、 TeX Live 2017 のまま使い続けることに。

tex.stackexchange.com

$ sudo tlmgr option repository ftp://tug.org/historic/systems/texlive/2017/tlnet-final
Password:
tlmgr: setting default package repository to ftp://tug.org/historic/systems/texlive/2017/tlnet-final
$ tlmgr --version
tlmgr revision 46207 (2018-01-04 19:34:36 +0100)
tlmgr using installation: /usr/local/texlive/2017basic
TeX Live (http://tug.org/texlive) version 2017

init.el で cask のエラーがでるので旧バージョンに戻す

Emacs の設定ファイルである init.el の読み込みに失敗するようになってしまいました。

Warning (initialization): An error occurred while loading ‘(略)/.emacs.d/init.el’:

error: Given parent class package-recipe is not a class

To ensure normal operation, you should investigate and remove the
cause of the error in your initialization file.  Start Emacs with
the ‘--debug-init’ option to view a complete error backtrace.

原因は cask のアップデートらしい

init.el の中で原因を探したところ、cask という Emacs のパッケージマネージャーのアップデートによるものだったようです。

Cask — Cask 0.8.4 (cask の公式ドキュメント)

cask の設定ファイルは /usr/local/share/emacs/site-lisp/cask/cask.el にあり、その中の defclass の使い方に関連するところでエラーが出ているようです。 …というところまではわかったので(そして Emacs Lisp に詳しくないので…)、とりあえず急場しのぎ的ですが homebrew で cask のバージョンを1つ前に戻します。

homebrew で cask のバージョンを戻す

ローカルにある旧バージョンを消してしまったので()、homebrew の Formula で Git を1つ巻き戻してインストールし直します。 再びここを参照していろいろやってみます。

確かに、つい最近アップデートがあったようです。cask の ログを辿りたいので Formula の中の cask.rb を見てみます。

$ pwd
/usr/local/Homebrew/Library/Taps/homebrew/homebrew-core/Formula
$ git log cask.rb
commit 9e8d64eb8fa735973ba58469072d72ad52bead1e
Author: Sam Brightman <sambrightman@users.noreply.github.com>
Date:   Fri May 11 03:10:45 2018 +0100

    cask 0.8.4 (#27715)

commit 1a9b379d15865c23176862e25d1d9b954656b76d
Author: ilovezfs <ilovezfs@icloud.com>
Date:   Wed Feb 21 00:02:46 2018 -0800

    cask 0.8.3 (#24378)

巻き戻します。

$ git checkout 1a9b379d15865c23176862e25d1d9b954656b76d cask.rb
$ brew unlink cask
Unlinking /usr/local/Cellar/cask/0.8.4... 2 symlinks removed
$ HOMEBREW_NO_AUTO_UPDATE=1 brew install cask
==> Downloading https://github.com/cask/cask/archive/v0.8.3.tar.gz
==> Downloading from https://codeload.github.com/cask/cask/tar.gz/v0.8.3
######################################################################## 100.0%
==> Caveats
Emacs Lisp files have been installed to:
  /usr/local/share/emacs/site-lisp/cask
==> Summary
🍺  /usr/local/Cellar/cask/0.8.3: 14 files, 167.0KB, built in 4 seconds
$ cask --version
0.8.3
$ git reset --hard
HEAD is now at bddf42a93 wrk-trello: update url

とりあえずはこれでバージョンも1つ前に戻り、うまく動くようになりました。

Coq のバージョンアップに対応する

Coq のバージョンが上がってしまい (Homebrew で 何も考えずに upgrade をかけてしまった) 、いざ Coq を書こうとしてRequire Import [ライブラリの名前] という行を読み込もうとしたら、

Error:
File /Users/(略).vo has bad
magic number 8700 (expected 8800). It is corrupted or was compiled with
another version of Coq.

というエラーが出てしまったのでどうにかしましょうね、という話です。

環境

  • macOS HighSierra 10.13.4
  • Emacs + Proof General
  • Coq version 8.7.2 → 8.8.0 (Homebrew)

proofgeneral.github.io

解決策① Coq を旧バージョンに戻す

Homebrew で Coq を入れているので、バージョンを戻せばなんとかなります。新しいバージョンを入れたばかりなら旧バージョンもローカルに残っていると思うので、とりあえず確認してみます。

$ brew info coq
coq: stable 8.8.0 (bottled), HEAD
Proof assistant for higher-order logic
https://coq.inria.fr/
/usr/local/Cellar/coq/8.7.2 (4,312 files, 217.9MB)
  Poured from bottle on 2018-02-19 at 13:33:15
/usr/local/Cellar/coq/8.8.0 (4,398 files, 220.6MB) *
  Poured from bottle on 2018-05-03 at 10:34:53
From: https://github.com/Homebrew/homebrew-core/blob/master/Formula/coq.rb
(…以下略)

8.7.2 と 8.8.0 の2バージョンあるのがわかります。また、現在使われているバージョンである 8.8.0 の方に*印が付いています。

すでに 8.8.0 にしてしまったものを 8.7.2 に戻すには、次のようにします。

$ brew switch coq 8.7.2
Cleaning /usr/local/Cellar/coq/8.8.0
Cleaning /usr/local/Cellar/coq/8.7.2
27 links created for /usr/local/Cellar/coq/8.7.2


下のサイトを参考にさせていただきました: qiita.com

解決策② 新バージョンでライブラリを make し直す

新バージョンで使っていくためには、(ライブラリがうまく対応していればという条件付きですが) 再度コンパイルし直せば大丈夫のようです。

ライブラリのあるディレクトリ(= Makefile が置いてあるディレクトリ) に移動して、

$ make clean

とすれば今までコンパイルされていたもの (主に拡張子が .vo のファイル) が削除されます。そして、新しいバージョンの Coq (今回なら 8.8.0) で

$ make

とします。これで新しいバージョンでのコンパイルがうまくいくはずです。

参考にさせていただきました: http://coq-club.inria.narkive.com/aFqstVbp/ynot