From be652f4fe10c3da633f27bc841781aeaa3b7c77e Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Mon, 18 Aug 2025 15:56:22 +0000 Subject: [PATCH 1/5] Upgrade to nightly-2025-08-15 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 39e0a8da5d6..4af101963fb 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-08-14" +channel = "nightly-2025-08-15" components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt", "clippy"] From 44df30b64f6e0487e9f4cf361dc73e2b08cf80f1 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Mon, 18 Aug 2025 16:05:24 +0000 Subject: [PATCH 2/5] Upgrade to nightly-2025-08-16 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 4af101963fb..3bcd5c679a2 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-08-15" +channel = "nightly-2025-08-16" components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt", "clippy"] From 72bb39bc59f418df15c2217dd47ed1f8576fb839 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Mon, 18 Aug 2025 11:44:14 -0700 Subject: [PATCH 3/5] Fix resolution of prelude import --- crates/flux-desugar/src/resolver.rs | 45 ++++++++++++++++++++++------- 1 file changed, 34 insertions(+), 11 deletions(-) diff --git a/crates/flux-desugar/src/resolver.rs b/crates/flux-desugar/src/resolver.rs index 903f5c238c3..13b22af8b5e 100644 --- a/crates/flux-desugar/src/resolver.rs +++ b/crates/flux-desugar/src/resolver.rs @@ -121,8 +121,8 @@ impl<'genv, 'tcx> CrateResolver<'genv, 'tcx> { let mut definitions = DefinitionMap::default(); for (parent, items) in &self.specs.flux_items_by_parent { for item in items { - // NOTE: This is putting all items in the same namespace. We could have qualifiers - // in a different namespace. + // NOTE: This is putting all items in the same namespace. In principle, we could have + // qualifiers in a different namespace. definitions .define(item.name()) .emit(&self.genv) @@ -191,8 +191,8 @@ impl<'genv, 'tcx> CrateResolver<'genv, 'tcx> { hir::UseKind::Glob => { let is_prelude = is_prelude_import(self.genv.tcx(), item); for mod_child in self.glob_imports(path) { - if let Some(ns @ (TypeNS | ValueNS)) = mod_child.res.ns() - && let Ok(res) = fhir::Res::try_from(mod_child.res) + if let Ok(res) = fhir::Res::try_from(mod_child.res) + && let Some(ns @ (TypeNS | ValueNS)) = res.ns() { let name = mod_child.ident.name; if is_prelude { @@ -495,14 +495,23 @@ impl<'genv, 'tcx> CrateResolver<'genv, 'tcx> { } fn glob_imports( - &self, + &mut self, path: &hir::UsePath, ) -> impl Iterator + use<'tcx> { - let res = path.segments.last().unwrap().res; - + // The path for the prelude import is not resolved anymore after , + // so we resolve all paths here. If this ever causes problems, we could use the resolution in the `UsePath` for + // non-prelude glob imports. let tcx = self.genv.tcx(); let curr_mod = self.current_module.to_def_id(); - if let hir::def::Res::Def(DefKind::Mod, module_id) = res { Some(module_id) } else { None } + self.resolve_path_with_ribs(path.segments, TypeNS) + .and_then(|partial_res| partial_res.full_res()) + .and_then(|res| { + if let fhir::Res::Def(DefKind::Mod, module_id) = res { + Some(module_id) + } else { + None + } + }) .into_iter() .flat_map(move |module_id| visible_module_children(tcx, module_id, curr_mod)) } @@ -517,8 +526,11 @@ impl<'genv, 'tcx> CrateResolver<'genv, 'tcx> { match module.kind { ModuleKind::Mod => { let module_id = module.def_id; - visible_module_children(tcx, module_id, self.current_module.to_def_id()) - .find(|child| child.res.matches_ns(ns) && child.ident == ident) + let current_mod = self.current_module.to_def_id(); + visible_module_children(tcx, module_id, current_mod) + .find(|child| { + child.res.matches_ns(ns) && tcx.hygienic_eq(ident, child.ident, current_mod) + }) .and_then(|child| fhir::Res::try_from(child.res).ok()) } ModuleKind::Trait => { @@ -702,6 +714,7 @@ impl<'tcx> hir::intravisit::Visitor<'tcx> for CrateResolver<'_, 'tcx> { } /// Akin to `rustc_resolve::Module` but specialized to what we support +#[derive(Debug)] struct Module { kind: ModuleKind, def_id: DefId, @@ -714,6 +727,7 @@ impl Module { } /// Akin to `rustc_resolve::ModuleKind` but specialized to what we support +#[derive(Debug)] enum ModuleKind { Mod, Trait, @@ -767,7 +781,8 @@ fn is_prelude_import(tcx: TyCtxt, item: &hir::Item) -> bool { .any(|attr| attr.path_matches(&[sym::prelude_import])) } -/// Abstraction over [`surface::PathSegment`] and [`surface::ExprPathSegment`] +/// Abstraction over a "segment" so we can use [`CrateResolver::resolve_path_with_ribs`] with paths +/// from different sources (e.g., [`surface::PathSegment`], [`surface::ExprPathSegment`]) trait Segment: std::fmt::Debug { fn record_segment_res(resolver: &mut CrateResolver, segment: &Self, res: fhir::Res); fn ident(&self) -> Ident; @@ -802,6 +817,14 @@ impl Segment for Ident { } } +impl Segment for hir::PathSegment<'_> { + fn record_segment_res(_resolver: &mut CrateResolver, _segment: &Self, _res: fhir::Res) {} + + fn ident(&self) -> Ident { + self.ident + } +} + struct ItemResolver<'a, 'genv, 'tcx> { resolver: &'a mut CrateResolver<'genv, 'tcx>, opaque: Option, // TODO: HACK! need to generalize to multiple opaque types/impls in a signature. From 85fed863d3be2ec25e016820625e6e5ffef43cff Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Mon, 18 Aug 2025 14:02:34 -0700 Subject: [PATCH 4/5] Upgrade to nightly-2025-08-18 --- .github/workflows/upgrade-toolchain.yml | 2 +- rust-toolchain.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/upgrade-toolchain.yml b/.github/workflows/upgrade-toolchain.yml index 79920528cd0..4adfb83e385 100644 --- a/.github/workflows/upgrade-toolchain.yml +++ b/.github/workflows/upgrade-toolchain.yml @@ -44,9 +44,9 @@ jobs: - name: Cherry pick changes from open PR run: | set -eu + cd flux existing_pr=$(gh pr list --base main --head toolchain-upgrade --state open --json number --jq '.[0].number' || true) if [ -n "$existing_pr" ]; then - cd flux git fetch --unshallow origin main toolchain-upgrade start=$(git merge-base main origin/toolchain-upgrade) end=origin/toolchain-upgrade diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 3bcd5c679a2..f7c57660197 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-08-16" +channel = "nightly-2025-08-18" components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt", "clippy"] From aa6acd1ba8a793339177d27aeba3dc75ac558ad5 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Mon, 18 Aug 2025 14:47:30 -0700 Subject: [PATCH 5/5] Update z3 for vtock --- .github/workflows/ci.yml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3576ab73bdb..29ea09aa3c9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,10 +8,6 @@ on: branches: [main] types: [opened, synchronize, reopened, ready_for_review] -concurrency: - group: ${{ github.head_ref || github.run_id }} - cancel-in-progress: true - jobs: tests: strategy: @@ -44,15 +40,11 @@ jobs: - name: Install fixpoint uses: ./.github/actions/install-fixpoint + # Older versions hang - name: Install Z3 uses: cda-tum/setup-z3@v1.6.6 with: - version: 4.12.1 - - - name: Install CVC5 - uses: ./.github/actions/install-cvc5 - with: - version: 1.2.1 + version: 4.15.3 - name: Rust Cache uses: Swatinem/rust-cache@v2.8.0