msys2 上で ocaml をビルドしようとして失敗した記録

■真新しいmsys2上でomakeを使いたくなったが、周知の通り現在はWindows用のバイナリが配布されていない。
msys2上のocamlでomakeをビルドしようとしたが上手く行かない。そこで、msys2上でocamlをビルドしてみればいいのではないかというアホなことを考えて失敗した記録。

■準備。本当に必要かどうかはわからない。

$ pacman -S gamin #fam みたいなもの
$ pacman -S bison #yacc みたいなもの
$ pacman -S gcc git patch

■ocamlをビルドする

#ocaml を msys2 上でビルドする。
$ git clone https://github.com/ocaml/ocaml
$ cd ocaml
$ ./configure -host x86_64-w64-windows -cc "gcc -Wno-error=implicit-function-declaration -Wno-error=int-conversion -Wl,--stack,16777216"
$ make clean
$ make world
$ make install

ln: シンボリックリンク 'ocamlyacc' の作成に失敗しました: No such file or directory
make: *** [Makefile:606: install] エラー 1

■msys2でsymlinkを使う方法:msys2_shell.cmd をテキストエディタで編集し

rem To activate windows native symlinks uncomment next line
rem set MSYS=winsymlinks:nativestrict

となっているところを

rem To activate windows native symlinks uncomment next line
set MSYS=winsymlinks:nativestrict

に変更して保存する。そして、msys2_shell.cmd を右クリックして「管理者として実行」してmsys2のシェルを立ち上げる。

■手持ちの別のマシンでやったところ ocamlyacc のエラーは出なかったが omake のビルドで

$ ocaml configure.ml
Cannot load required shared library dllcamlstr.
Reason: dllcamlstr.so: dynamic loading not supported on this platform.
Cannot load required shared library dllunix.
Reason: dllunix.so: dynamic loading not supported on this platform.
File "./configure.ml", line 1:
Error: Reference to undefined global `Str'

となって止まってしまった。

広告

(超適当な自作小説のあらすじ)

ミステリが好きな人はそっとじ推奨

講談社から述語論理を駆使する探偵が活躍する(らしい)小説が出るとのことで、大変めでたいと思います。
このニュースに刺激を受けて超適当な自作小説のアイデアを書き出してみたのですが、書きだしただけで満足してこれ以上書く気がなくなったのでブログの記事にして晒しておきます。

季節:真冬
舞台:開発されたスキーリゾート地に隣接する古い村のはずれにある古びた洋館

■第一の殺人

宿泊客の一人が食堂で変死する。死者の背には一連の閉論理式が刺青されていた。居合わせた刑事はこれを「ダイニングメッセージ」と受け取る。背中の刺青は、容疑者を特定するためのヒントとして被害者が自ら施したという推理を披露し、他の宿泊客を呆れさせる。

「つまり刑事さん、あなたは被害者が自分の背中に刺青を、死ぬ前の僅かな時間にやってのけたと言うのですか?」
「人間その気になればなんでもできるものです」

■第一の探偵

スキーコースからはずれて遭難してきた男は論理学者だった。論理学者は論理式の構造と解釈、コンパクト性定理について解説し、刺青理論がモデルを持つならばそれこそが犯人に違いないという推理を展開する。論理学者は残された宿泊客を一人ずつチェックするが、だれも刺青理論のモデルではないことが判明する。論理学者はそれでも納得せず「犯人はこの中にいるはずだッ」と一喝、驚きのあまり隠れ潜んでいた犯人(刺青理論のモデル)が天井を突き破って落下し、刑事に捕縛される。

■第二、第三の殺人

翌朝、論理学者が死体で発見される。確保された犯人もまた惨殺されていた。「犯人は一人ではなかったのでは?」怯える宿泊客たち。やはりスキーコースからはずれて遭難してきた男は大論理学者だった。男は(殺された)論理学者の推理には漏れがある可能性を指摘する。大論理学者はレーヴェンハイム-スコーレムの定理と非標準モデルについて説明し、刺青理論が犯人を指し示すならば、無限に多くの非標準犯人が存在する可能性を指摘する。翌朝、大論理学者が惨殺死体で発見される。

■死神の登場

宿泊客が起きると、ホールには何処から来たのか死神が立っていた。宿泊客が気圧される中、死神の口から発せられたのは驚愕の託宣だった:「ゲーデルの不完全性定理により今までのお前たちの推理は全て間違っている」。
混乱を尻目に、死神は忽然と姿を消す。

■第三の探偵

スキーコースからはずれて遭難してきた男は神聖論理学者だった。神聖論理学者は超積による超準モデルの構成と初等埋め込みについて解説する。神聖論理学者は事件を解決する意思など全くなさそうである。翌朝、神聖論理学者が惨殺死体で発見される。

■聖者の登場

宿泊客が起きると、食堂で待ち受けていたのは何処からか迷い込んだ乞食(聖者)だった。聖者は Edward Nelson の Internal Set Theory について解説し、「超準世界と標準世界に截然とした境界などない、それが本当の姿かもしれません」と言い放つ。例として聖者は「全ての無限集合は超準元を持つ」ことを示し、「無限者の似姿として創造された我々人間にもこれは言えるはずです」と言う。宿泊客の目が次第に開かれてゆき、今までの死者たちの超準部分はまだ生きていることに気づく。もはや死者はおらず、殺人は起こっておらず、従って殺人事件は存在しなかった。死者(だと思われていた宿泊客)たちは立ち上がり、他の宿泊客と歓談を交わす。

背中に刺青を施された宿泊客が「結局犯人は誰だったのでしょうか?」と聖者に質問する。聖者は微笑んで「舌を見せなさい」と言う。宿泊客の舌には「0=1」と刺青が施されていた。「これが見落とされていた公理です。殺人は起こらなかったのだから犯人が存在することは矛盾です、そうですね」

刑事が不審そうに「では背中の刺青は結局誰が何のために残したのですか?」

聖者は口を開こうとするが途中でやめ、ただ微笑んでいた。
唐突に物語は打ち切られ、空白だけが続く。