Socket.leanを作ってみる（失敗）

Lean 記録

まず、

$ git clone https://github.com/xubaiw/Socket.lean

$ cd Socket.lean

$ cat lean-toolchain
leanprover/lean4:nightly-2022-06-16

去年だと、「ふるっ！」と思う。

$ git branch
* main

$ git rev-parse main
9fc98bc24ccdb4471b2e38e94dccd18f75d2a293

これが確実なパッケージID。

$ elan toolchain list
leanprover-community/lean:3.23.0
leanprover-community/lean:nightly
leanprover-community/lean:stable
leanprover/lean4:nightly (default)
leanprover/lean4:nightly-2022-07-06
leanprover/lean4:nightly-2022-10-09
leanprover/lean4:nightly-2022-10-20
leanprover/lean4:nightly-2022-11-20
leanprover/lean4:nightly-2022-12-02
leanprover/lean4:nightly-2022-12-16
leanprover/lean4:nightly-2022-12-22
leanprover/lean4:nightly-2022-12-24
leanprover/lean4:nightly-2023-01-10
leanprover/lean4:nightly-2023-01-21
leanprover/lean4:stable
leanprover/lean4:v4.0.0-m5

leanprover/lean4:nightly-2022-06-16 はない。ウーム。とりあえず、手で lean-toolcain を書き換えてやってみるか。

$ mv lean-toolchain lean-toolchain.ORIG

$ echo leanprover/lean4:nightly-2022-07-06 > lean-toolchain

$ cat lean-toolchain
leanprover/lean4:nightly-2022-07-06

$ lake --version
Lake version 3.2.1 (Lean version 4.0.0-nightly-2022-07-06)

$ lean --version
Lean (version 4.0.0-nightly-2022-07-06, commit 38e1f6ba824b, Release)

ひと月弱新しいツールチェーンに無理くり置き換えた。

$ lean-build
error: unknown short option '-v'

ナニッ?! 昔のlakeには -v オプショナルがない。

$ alias lean-build-nov='lake build  |& tee $(date +%Y-%m-%d_%H-%M-%S).lake-build.log'

ビルド失敗。エラーログは：

> c:\Users\m-hiyama\.elan\toolchains\leanprover--lean4---nightly-2022-07-06\bin\leanc.exe -shared -o C:\Windows\System32\ws2_32.dll -Wl,--whole-archive C:\Windows\System32\ws2_32.dll -Wl,--no-whole-archive
> gcc -c -o .\build\native\ffi.o .\native\native.c -I c:\Users\m-hiyama\.elan\toolchains\leanprover--lean4---nightly-2022-07-06\include
error: stderr:
ld.lld: error: cannot open output file C:\Windows\System32\ws2_32.dll: Permission denied
clang: error: unable to remove file: Permission denied
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command c:\Users\m-hiyama\.elan\toolchains\leanprover--lean4---nightly-2022-07-06\bin\leanc.exe exited with status 1

起動コマンドを書くと：

  • leanc.exe -shared -o C:\Windows\System32\ws2_32.dll -Wl,--whole-archive C:\Windows\System32\ws2_32.dll -Wl,--no-whole-archive
  • gcc -c -o .\build\native\ffi.o .\native\native.c -I c:\Users\m-hiyama\.elan\toolchains\leanprover--lean4---nightly-2022-07-06\include
  • エラーメッセージは、ld.lld と clang から出ている。

分かること：

  • gccコマンドは起動可能。Clangがgcc互換モードでインストールされている。cc, gcc, clang のどれでも起動できる。
  • ld.lld.exe はClangではなくて、Leanツールチェーン側かも知れない。
  • lean.cexe は gcc と ld.lld を呼んでいるようだ。gccの実体はclang。
  • -o C:\Windows\System32\ws2_32.dll ここは無理がある。管理者モードで実行か。

しかし、C:\Windows\System32\ws2_32.dll は既存システムファイルだな。書き換えるのはこわい。