lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

chore: nix flake update

Open crvdgc opened this issue 1 year ago • 15 comments

In order to fix nix-shell failure due to CCache 4.8.1 test script. Closes #3048.

crvdgc avatar Dec 11 '23 12:12 crvdgc

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-11 12:35:07)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bb0695b0175bad81f8c13e5db5c6f54e11ca6db0 --onto 88fbe2e5313bb418abdb035c48cae2680ea9bcea. (2024-02-26 23:58:53)

Thanks for this PR!

The nix CI is failing. It seems somewhere a rust package vendor hash needs updating. @crvdgc, let us know if you can find and fix that or need advise.

nomeata avatar Dec 11 '23 12:12 nomeata

Hi, @nomeata. The problem is the lean-mdbook's cargoDeps.outputHash. I'm not sure what's the dependency requirement for that directory, so I just bumped the hash as well as the flake.lock file together. Let me know if this creates any futher problem and I'll dive deeper.

crvdgc avatar Dec 11 '23 14:12 crvdgc

Thanks, CI passes, so that should be sufficient.

@Kha, are there things in the nix setup that aren't covered by CI that we should check manually before merging?

nomeata avatar Dec 11 '23 16:12 nomeata

We should check the docs after merging, other than that CI is what it's for :)

Kha avatar Dec 11 '23 16:12 Kha

With full-ci, the sanitize job failed, probably because of newer LLVM or something?

[    ] Linking /home/runner/work/lean4/lean4/build/stage1/bin/lake
/nix/store/1fn92b0783crypjcxvdv6ycmvi27by0j-binutils-2.40/bin/ld: /nix/store/07haalw3zm3yl0rbphvrg59fl8ain36k-clang-wrapper-15.0.7/resource-root/lib/linux/libclang_rt.asan_cxx-x86_64.a(ubsan_type_hash_itanium.cpp.o): undefined reference to symbol '_ZTIN10__cxxabiv121__vmi_class_type_infoE@@CXXABI_1.3'
/nix/store/1fn92b0783crypjcxvdv6ycmvi27by0j-binutils-2.40/bin/ld: /nix/store/myw67gkgayf3s2mniij7zwd79lxy8v0k-gcc-12.3.0-lib/lib/libstdc++.so.6: error adding symbols: DSO missing from command line
clang-15: error: linker command failed with exit code 1 (use -v to see invocation)

nomeata avatar Dec 11 '23 18:12 nomeata

Hi, looking at the full-ci failure, I added one fix for a warning for CMP0148 because CMake is bumped to 3.27.

As for the actual error, my hypothesis is that to use -fsanitize=address, compiler-rt needs to be enabled. Although previously g++ picked that up by itself. See the compiler-rt page and the AddressSanitizer page.

I should note that I'm not familiar with LLVM/clang. Feel free to edit or invite more experts for reviewing.

crvdgc avatar Dec 12 '23 00:12 crvdgc

I should note that I'm not familiar with LLVM/clang. Feel free to edit or invite more experts for reviewing.

Me neither, so I'm secretly hoping you'll be able to figure it out so that I don't have to, and will be grateful for that :-)

nomeata avatar Dec 12 '23 07:12 nomeata

We might want to consider not using shell.nix for these configurations if it makes our lives harder rather than easier :)

Kha avatar Dec 12 '23 08:12 Kha

If it works it probably makes it easier, e.g. when we have to debug it outside CI, doesn't it?

nomeata avatar Dec 12 '23 09:12 nomeata

Right, I suppose it would still be my own workflow for building a sanitized build - not much other choice on NixOS

Kha avatar Dec 12 '23 09:12 Kha

What about pinning nixpkgs to the revision where CCache is bumped to 4.8.2? That should be generate the minimum breakage but also solves #3048. If that doesn't work as well, then maybe we should wait for upstream change.

I can put the above revision in place of nixpkgs-unstable in the root flake.nix, or just updating the lock files. Pinning in the flake may be ugly and may have some cache implications, but it makes the intent clear. What do you think, @nomeata?

crvdgc avatar Dec 12 '23 12:12 crvdgc

If you just want to scratch that itch, and aren't motivated to track down the other issue (which is fair), then that's a plausible approach. It's still from nixpkg master, so the cache should work.

I'd pin it in the flake with a comment that explains why that commit.

You could also see if nixpkg-23.11 happens to work; using stable if we can would be good.

nomeata avatar Dec 12 '23 12:12 nomeata

Thank you for the suggestions @nomeata. I tried nixpkgs 23.11 and it can compile Lean 4 but fails to build the doc. nixpkgs 23.05 worked for me locally (on aarch64-darwin), so I'll try one more time :)

Sorry for the auto format change in the doc/flake.nix, I'll amend it.

crvdgc avatar Dec 12 '23 17:12 crvdgc

Hi, the CI passed, I wonder if I should rebase again and try to merge this PR?

crvdgc avatar Dec 15 '23 11:12 crvdgc