speedcenter on nightly-testing

Stream: mathlib4

[Joachim Breitner]

I just tried to run !bench on a nightly testing commit, but it failed:
http://speed.lean-fro.org/mathlib4/run-detail/41e5d68f-95ec-432b-8f47-9e2d46edcddb

############
## Stderr ##
############
copying path '/nix/store/aixa5dj9k9hjvqkfcxzk8g737a7c62n0-source' from 'https://cache.nixos.org'...
these 10 paths will be fetched (7.59 MiB download, 35.16 MiB unpacked):
  /nix/store/j9rc786ylq8cid4zgcn6idknilkbd4ax-bash-5.1-p16
  /nix/store/d2bpliayddadf6lx6l1i04w265gqw8n6-glibc-2.34-210
  /nix/store/8q06kxhkl4dq3vjd3ai2j8n9kr26c271-gnumake-4.3
  /nix/store/b8g2i5l196pdywljm3df4zlsk45jpzcy-gnumake-4.3-man
  /nix/store/01ymyhl5ckhav09f7p6vk7w227bicglv-jq-1.6-bin
  /nix/store/wrlj7h8kixc5y8qkjaar24012nw9mr1m-jq-1.6-lib
  /nix/store/89m35h04cfx0w1wgwr6kd9abvganncm2-jq-1.6-man
  /nix/store/finq3bf8qy4nwkc447q7msg4g8nliyii-libidn2-2.3.2
  /nix/store/7k3alvjrd0017ddk87rdnmdvlgh7yq9d-libunistring-1.0
  /nix/store/is67c0b7knhd8i930xxfpmrh0dskwymp-onig-6.9.8
copying path '/nix/store/b8g2i5l196pdywljm3df4zlsk45jpzcy-gnumake-4.3-man' from 'https://cache.nixos.org'...
copying path '/nix/store/89m35h04cfx0w1wgwr6kd9abvganncm2-jq-1.6-man' from 'https://cache.nixos.org'...
copying path '/nix/store/7k3alvjrd0017ddk87rdnmdvlgh7yq9d-libunistring-1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/finq3bf8qy4nwkc447q7msg4g8nliyii-libidn2-2.3.2' from 'https://cache.nixos.org'...
copying path '/nix/store/d2bpliayddadf6lx6l1i04w265gqw8n6-glibc-2.34-210' from 'https://cache.nixos.org'...
copying path '/nix/store/j9rc786ylq8cid4zgcn6idknilkbd4ax-bash-5.1-p16' from 'https://cache.nixos.org'...
copying path '/nix/store/8q06kxhkl4dq3vjd3ai2j8n9kr26c271-gnumake-4.3' from 'https://cache.nixos.org'...
copying path '/nix/store/is67c0b7knhd8i930xxfpmrh0dskwymp-onig-6.9.8' from 'https://cache.nixos.org'...
copying path '/nix/store/wrlj7h8kixc5y8qkjaar24012nw9mr1m-jq-1.6-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/01ymyhl5ckhav09f7p6vk7w227bicglv-jq-1.6-bin' from 'https://cache.nixos.org'...
+ temci exec --config ./scripts/bench/temci-config.yml
[2023-12-01 14:24:49,641] Program block no. 2 failed: Unexpected return code 1, expected 0
[2023-12-01 14:24:49,641] output

Mathlib.lean:1:0: error: unknown package 'Mathlib'
You might need to open '/home/velcom/mathlib4/task_repo' as a workspace in your editor

[2023-12-01 14:24:49,641] error

error: unknown command 'print-paths'

Is this on someone’s radar?

[Sebastian Ullrich]

I guess it would have to be on my radar but it wasn't so far

[Sebastian Ullrich]

Oh, I see a lake print-paths invocation, that needs updating

[Sebastian Ullrich]

Pushed a tentative fix onto nightly-testing, I hope that was the correct thing to do /cc @Scott Morrison . But the build is broken anyway.

[Scott Morrison]

@Sebastian Ullrich, which Lean version requires that fix?

Ideally changes that will be required long term get made as PRs to bump/v4.5.0, and then can be merged into nightly-testing while undergoing review.

[Scott Morrison]

Right now nightly-testing is broken until we get Mathlib onto v4.4.0-rc1, hopefully in the next few hours.

[Scott Morrison]

I think your fix wasn't right, in any case:

lake setup-file --no-build Mathlib Mathlib

doesn't produce any json on nightly-testing.
(but lake setup-file Mathlib does)

[Sebastian Ullrich]

@Scott Morrison works fine in #8808