lean4
lean4 copied to clipboard
chore: nix flake update
In order to fix nix-shell failure due to CCache 4.8.1 test script. Closes #3048.
- ❗ 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. Trygit 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.
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.
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?
We should check the docs after merging, other than that CI is what it's for :)
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)
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.
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 :-)
We might want to consider not using shell.nix for these configurations if it makes our lives harder rather than easier :)
If it works it probably makes it easier, e.g. when we have to debug it outside CI, doesn't it?
Right, I suppose it would still be my own workflow for building a sanitized build - not much other choice on NixOS
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?
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.
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.
Hi, the CI passed, I wonder if I should rebase again and try to merge this PR?