search

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
62 stars 18 forks source link

chore: bump toolchain to nightly-2024-10-07 #217

Closed alexkeizer closed 3 weeks ago

alexkeizer commented 1 month ago

Description:

Bumps the toolchain to the latest nightly. Mostly in the (unlikely) hope that some of our instantiateMVars performance woes might disappear.

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine? Yes

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

alexkeizer commented 1 month ago

@bollu the traces for the CSE tests changed. I've accepted the new trace somewhat blindly; could you confirm the difference is benign?

bollu commented 1 month ago

Yep, LGTM!

shigoel commented 1 month ago

FYI: https://github.com/draperlaboratory/ELFSage/pull/15 where the toolchain is leanprover/lean4:nightly-2024-10-07

While that's upstreamed, we can use my fork of ELFSage.

shigoel commented 1 month ago

FYI: https://github.com/draperlaboratory/ELFSage/pull/15 got merged. No need to use my fork.