Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
dba1ead
Upgrade to nightly-2025-12-06
nilehmann Dec 23, 2025
73fc68e
ReifyFnPointer
nilehmann Dec 9, 2025
65da26d
Upgrade to nightly-2025-12-09
nilehmann Dec 23, 2025
109287f
BlobDecoder
nilehmann Dec 11, 2025
aaa041f
Upgrade to nightly-2025-12-11
nilehmann Dec 23, 2025
c546900
proc_macro_tracked_path
nilehmann Dec 12, 2025
17bf63f
Upgrade to nightly-2025-12-14
nilehmann Dec 23, 2025
877674e
RealFileName
nilehmann Dec 18, 2025
b36ee0b
Upgrade to nightly-2025-12-15
github-actions[bot] Dec 18, 2025
f6fc0fb
CrateSource::rmeta
nilehmann Dec 22, 2025
cb74f6c
Upgrade to nightly-2025-12-18
nilehmann Dec 23, 2025
87b7e48
AnnotateSnippetEmitter
nilehmann Dec 23, 2025
4b561f2
Upgrade to nightly-2025-12-23
nilehmann Dec 23, 2025
d9e15c4
NullOp -> Runtimechecks
nilehmann Jan 19, 2026
d963b23
Upgrade to nightly-2025-12-28
github-actions[bot] Jan 27, 2026
1b55bd3
Fix ValTree API changes
Copilot Jan 27, 2026
3d7ec46
Upgrade to nightly-2026-01-02
github-actions[bot] Jan 27, 2026
ac2c1f1
Upgrade to nightly-2026-01-07
github-actions[bot] Jan 27, 2026
62aa5d7
Fix toolchain upgrade issues for nightly-2026-01-07 (#1457)
Copilot Jan 27, 2026
2f24759
Patch libs for lean demo
nilehmann Jan 27, 2026
dbb95c0
Upgrade to nightly-2026-01-12
github-actions[bot] Jan 27, 2026
5719ad3
Fix ConstArg::span API change
Copilot Jan 28, 2026
8af0da7
Upgrade to nightly-2026-01-17
github-actions[bot] Jan 28, 2026
7467e9c
Fix Providers field access
Copilot Jan 28, 2026
8ac2535
Upgrade to nightly-2026-01-22
github-actions[bot] Jan 28, 2026
6350348
Upgrade to nightly-2026-01-27
github-actions[bot] Jan 28, 2026
37fd27b
Upgrade to nightly-2026-01-28
github-actions[bot] Jan 28, 2026
c6e63fe
Upgrade to nightly-2026-01-29
github-actions[bot] Jan 29, 2026
f01b96a
Upgrade to nightly-2026-01-30
github-actions[bot] Jan 30, 2026
0fb7407
BoundVariableKind
nilehmann Feb 10, 2026
06778bc
Upgrade to nightly-2026-02-01
github-actions[bot] Feb 10, 2026
a86891a
Upgrade to nightly-2026-02-03
github-actions[bot] Feb 10, 2026
6349df2
Upgrade to nightly-2026-02-05
github-actions[bot] Feb 10, 2026
67d714e
Fix rustc API change for queries module in nightly-2026-02-05 (#1471)
Copilot Feb 10, 2026
d4f5d27
Upgrade to nightly-2026-02-07
github-actions[bot] Feb 10, 2026
7de4a28
Adapt flux-driver to rustc ExitCode API changes (#1472)
Copilot Feb 10, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,14 @@ jobs:
run: |
git clone https://github.com/flux-rs/flux-to-lean-demo

- name: Patch flux-rs dependency if in pull request
if: github.event_name == 'pull_request'
run: |
echo '[patch."https://github.com/flux-rs/flux.git"]' >> flux-to-lean-demo/Cargo.toml
echo 'flux-rs = { path = "../lib/flux-rs" }' >> flux-to-lean-demo/Cargo.toml
echo 'flux-core = { path = "../lib/flux-core" }' >> flux-to-lean-demo/Cargo.toml
echo 'flux-alloc = { path = "../lib/flux-alloc" }' >> flux-to-lean-demo/Cargo.toml

- name: Generate Lean Project
continue-on-error: true
working-directory: flux-to-lean-demo
Expand Down
3 changes: 2 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,5 @@ target
log
sysroot/

.DS_Store
.DS_Store
fixpoint
2 changes: 1 addition & 1 deletion crates/flux-desugar/src/desugar/lift.rs
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ impl<'genv> RustItemCtxt<'_, 'genv, '_> {
}

fn lift_const_arg(&mut self, const_arg: &hir::ConstArg) -> fhir::ConstArg {
fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span: const_arg.span() }
fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span: const_arg.span }
}

#[track_caller]
Expand Down
12 changes: 8 additions & 4 deletions crates/flux-driver/src/bin/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,15 @@

extern crate rustc_driver;

use std::{env, io, process::exit};
use std::{env, io, process::{ExitCode, exit}};

use flux_config::{
self as config,
flags::{self, EXIT_FAILURE},
};
use flux_driver::callbacks::FluxCallbacks;
use flux_middle::metrics;
use rustc_driver::{EXIT_SUCCESS, catch_with_exit_code, run_compiler};
use rustc_driver::{catch_with_exit_code, run_compiler};

mod logger;

Expand Down Expand Up @@ -49,8 +49,12 @@ fn main() -> io::Result<()> {
let exit_code = catch_with_exit_code(move || {
run_compiler(&args, &mut FluxCallbacks);
});
if config::summary() && exit_code == EXIT_SUCCESS {
if config::summary() && exit_code == ExitCode::SUCCESS {
metrics::print_summary(start.elapsed())?;
};
exit(exit_code)
exit(if exit_code == ExitCode::SUCCESS {
rustc_driver::EXIT_SUCCESS
} else {
rustc_driver::EXIT_FAILURE
})
}
16 changes: 8 additions & 8 deletions crates/flux-driver/src/callbacks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ use rustc_hir::{
def_id::{DefId, LOCAL_CRATE, LocalDefId},
};
use rustc_interface::interface::Compiler;
use rustc_middle::{query, ty::TyCtxt};
use rustc_middle::{queries, ty::TyCtxt, util};
use rustc_session::config::OutputType;
use rustc_span::FileName;

Expand All @@ -37,7 +37,7 @@ impl Callbacks for FluxCallbacks {
assert!(config.override_queries.is_none());

config.override_queries = Some(|_, local| {
local.mir_borrowck = mir_borrowck;
local.queries.mir_borrowck = mir_borrowck;
});
// this should always be empty otherwise something changed in rustc and all our assumptions
// about symbol interning are wrong.
Expand Down Expand Up @@ -185,11 +185,11 @@ impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> {
let span = tcx.def_span(def_id);
let sm = tcx.sess.source_map();
let FileName::Real(file_name) = sm.span_to_filename(span) else { return true };
let mut file_path = file_name.local_path_if_available();
let Some(mut file_path) = file_name.local_path() else { return true };

// If the path is absolute try to normalize it to be relative to the working_dir
if file_path.is_absolute() {
let working_dir = tcx.sess.opts.working_dir.local_path_if_available();
let Some(working_dir) = sm.working_dir().local_path() else { return true };
let Ok(p) = file_path.strip_prefix(working_dir) else { return true };
file_path = p;
}
Expand Down Expand Up @@ -355,7 +355,7 @@ fn force_conv(genv: GlobalEnv, def_id: DefId) -> QueryResult {
fn mir_borrowck<'tcx>(
tcx: TyCtxt<'tcx>,
def_id: LocalDefId,
) -> query::queries::mir_borrowck::ProvidedValue<'tcx> {
) -> queries::mir_borrowck::ProvidedValue<'tcx> {
let bodies_with_facts = rustc_borrowck::consumers::get_bodies_with_borrowck_facts(
tcx,
def_id,
Expand All @@ -368,8 +368,8 @@ fn mir_borrowck<'tcx>(
flux_common::mir_storage::store_mir_body(tcx, def_id, body_with_facts);
}
}
let mut providers = query::Providers::default();
rustc_borrowck::provide(&mut providers);
let original_mir_borrowck = providers.mir_borrowck;
let mut providers = util::Providers::default();
rustc_borrowck::provide(&mut providers.queries);
let original_mir_borrowck = providers.queries.mir_borrowck;
original_mir_borrowck(tcx, def_id)
}
21 changes: 2 additions & 19 deletions crates/flux-errors/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ pub use rustc_errors::ErrorGuaranteed;
use rustc_errors::{
Diagnostic, ErrCode, FatalAbort, FatalError, LazyFallbackBundle, TerminalUrl,
annotate_snippet_emitter_writer::AnnotateSnippetEmitter,
emitter::{Emitter, HumanEmitter, HumanReadableErrorType, OutputTheme, stderr_destination},
emitter::{Emitter, HumanReadableErrorType, OutputTheme, stderr_destination},
json::JsonEmitter,
translation::Translator,
};
Expand Down Expand Up @@ -100,7 +100,7 @@ fn emitter(
match sopts.error_format {
config::ErrorOutputType::HumanReadable { kind, color_config } => {
match kind {
HumanReadableErrorType::AnnotateSnippet { short, unicode } => {
HumanReadableErrorType { short, unicode } => {
let emitter =
AnnotateSnippetEmitter::new(stderr_destination(color_config), translator)
.sm(source_map)
Expand All @@ -118,23 +118,6 @@ fn emitter(
);
Box::new(emitter.ui_testing(sopts.unstable_opts.ui_testing))
}
HumanReadableErrorType::Default { short } => {
let emitter = HumanEmitter::new(stderr_destination(color_config), translator)
.sm(source_map)
.short_message(short)
.diagnostic_width(sopts.diagnostic_width)
.macro_backtrace(macro_backtrace)
.track_diagnostics(track_diagnostics)
.terminal_url(terminal_url)
.theme(OutputTheme::Ascii)
.ignored_directories_in_source_blocks(
sopts
.unstable_opts
.ignore_directory_in_diagnostics_source_blocks
.clone(),
);
Box::new(emitter.ui_testing(sopts.unstable_opts.ui_testing))
}
}
}
config::ErrorOutputType::Json { pretty, json_rendered, color_config } => {
Expand Down
24 changes: 15 additions & 9 deletions crates/flux-macros/src/diagnostics/fluent.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,19 @@
use std::collections::{HashMap, HashSet};
use std::fs::read_to_string;
use std::path::{Path, PathBuf};
use std::{
collections::{HashMap, HashSet},
fs::read_to_string,
path::{Path, PathBuf},
};

use annotate_snippets::{Renderer, Snippet};
use fluent_bundle::{FluentBundle, FluentError, FluentResource};
use fluent_syntax::ast::{
Attribute, Entry, Expression, Identifier, InlineExpression, Message, Pattern, PatternElement,
use fluent_syntax::{
ast::{
Attribute, Entry, Expression, Identifier, InlineExpression, Message, Pattern,
PatternElement,
},
parser::ParserError,
};
use fluent_syntax::parser::ParserError;
use proc_macro::tracked_path::path;
use proc_macro::{Diagnostic, Level, Span};
use proc_macro::{Diagnostic, Level, Span, tracked::path};
use proc_macro2::TokenStream;
use quote::quote;
use syn::{Ident, LitStr, parse_macro_input};
Expand Down Expand Up @@ -158,7 +162,9 @@ pub(crate) fn fluent_messages(input: proc_macro::TokenStream) -> proc_macro::Tok
for entry in resource.entries() {
if let Entry::Message(msg) = entry {
let Message { id: Identifier { name }, attributes, value, .. } = msg;
let _ = previous_defns.entry((*name).to_string()).or_insert(resource_span);
let _ = previous_defns
.entry((*name).to_string())
.or_insert(resource_span);
if name.contains('-') {
Diagnostic::spanned(
resource_span,
Expand Down
8 changes: 7 additions & 1 deletion crates/flux-macros/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,10 @@
#![feature(proc_macro_diagnostic, never_type, proc_macro_span, if_let_guard, track_path)]
#![feature(
proc_macro_diagnostic,
never_type,
proc_macro_span,
if_let_guard,
proc_macro_tracked_path
)]

mod diagnostics;
mod fold;
Expand Down
73 changes: 38 additions & 35 deletions crates/flux-metadata/src/decoder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,8 @@ use rustc_serialize::{
};
use rustc_session::StableCrateId;
use rustc_span::{
BytePos, ByteSymbol, DUMMY_SP, SourceFile, Span, SpanDecoder, Symbol, SyntaxContext,
BlobDecoder, BytePos, ByteSymbol, DUMMY_SP, SourceFile, Span, SpanDecoder, Symbol,
SyntaxContext,
def_id::{CrateNum, DefIndex},
hygiene::{HygieneDecodeContext, SyntaxContextKey},
};
Expand Down Expand Up @@ -103,6 +104,42 @@ pub(super) fn decode_crate_metadata(

implement_ty_decoder!(DecodeContext<'a, 'tcx>);

impl BlobDecoder for DecodeContext<'_, '_> {
fn decode_symbol(&mut self) -> Symbol {
let tag = self.read_u8();

match tag {
SYMBOL_STR => {
let s = self.read_str();
Symbol::intern(s)
}
SYMBOL_OFFSET => {
// read str offset
let pos = self.read_usize();

// move to str offset and read
self.opaque.with_position(pos, |d| {
let s = d.read_str();
Symbol::intern(s)
})
}
SYMBOL_PREDEFINED => {
let symbol_index = self.read_u32();
Symbol::new(symbol_index)
}
_ => unreachable!(),
}
}

fn decode_byte_symbol(&mut self) -> ByteSymbol {
ByteSymbol::intern(self.read_byte_str())
}

fn decode_def_index(&mut self) -> DefIndex {
DefIndex::from_u32(self.read_u32())
}
}

impl SpanDecoder for DecodeContext<'_, '_> {
fn decode_attr_id(&mut self) -> rustc_ast::AttrId {
self.tcx.sess.psess.attr_id_generator.mk_attr_id()
Expand All @@ -113,10 +150,6 @@ impl SpanDecoder for DecodeContext<'_, '_> {
self.tcx.stable_crate_id_to_crate_num(stable_id)
}

fn decode_def_index(&mut self) -> DefIndex {
DefIndex::from_u32(self.read_u32())
}

fn decode_def_id(&mut self) -> DefId {
DefId { krate: Decodable::decode(self), index: Decodable::decode(self) }
}
Expand Down Expand Up @@ -165,36 +198,6 @@ impl SpanDecoder for DecodeContext<'_, '_> {

Span::new(lo, hi, ctxt, None)
}

fn decode_symbol(&mut self) -> rustc_span::Symbol {
let tag = self.read_u8();

match tag {
SYMBOL_STR => {
let s = self.read_str();
Symbol::intern(s)
}
SYMBOL_OFFSET => {
// read str offset
let pos = self.read_usize();

// move to str offset and read
self.opaque.with_position(pos, |d| {
let s = d.read_str();
Symbol::intern(s)
})
}
SYMBOL_PREDEFINED => {
let symbol_index = self.read_u32();
Symbol::new(symbol_index)
}
_ => unreachable!(),
}
}

fn decode_byte_symbol(&mut self) -> ByteSymbol {
ByteSymbol::intern(self.read_byte_str())
}
}

impl<'tcx> TyDecoder<'tcx> for DecodeContext<'_, 'tcx> {
Expand Down
7 changes: 2 additions & 5 deletions crates/flux-metadata/src/encoder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,8 +77,6 @@ fn file_indices(
let mut file_index_to_stable_id =
FxHashMap::with_capacity_and_hasher(files.len(), Default::default());
use rustc_span::def_id::LOCAL_CRATE;
let source_map = tcx.sess.source_map();
let working_directory = &tcx.sess.opts.working_dir;
let local_crate_stable_id = tcx.stable_crate_id(LOCAL_CRATE);

// This portion of the code is adapted from the rustc metadata encoder, while the rest of
Expand All @@ -95,9 +93,8 @@ fn file_indices(
use rustc_span::FileName;
match file.name {
FileName::Real(ref original_file_name) => {
let adapted_file_name = source_map
.path_mapping()
.to_embeddable_absolute_path(original_file_name.clone(), working_directory);
let mut adapted_file_name = original_file_name.clone();
adapted_file_name.update_for_crate_metadata();

adapted_source_file.name = FileName::Real(adapted_file_name);
}
Expand Down
2 changes: 1 addition & 1 deletion crates/flux-metadata/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -489,7 +489,7 @@ fn flux_metadata_extern_location(tcx: TyCtxt, crate_num: CrateNum) -> Option<Pat
tcx.used_crate_source(crate_num)
.rmeta
.as_ref()
.map(|(path, _)| path.with_extension("fluxmeta"))
.map(|path| path.with_extension("fluxmeta"))
}

// Tags for encoding Symbol's
Expand Down
2 changes: 1 addition & 1 deletion crates/flux-middle/src/fhir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1175,7 +1175,7 @@ impl<Id1, Id2> TryFrom<rustc_hir::def::Res<Id1>> for Res<Id2> {
match res {
rustc_hir::def::Res::Def(kind, did) => Ok(Res::Def(kind, did)),
rustc_hir::def::Res::PrimTy(prim_ty) => Ok(Res::PrimTy(prim_ty)),
rustc_hir::def::Res::SelfTyAlias { alias_to, forbid_generic: false, is_trait_impl } => {
rustc_hir::def::Res::SelfTyAlias { alias_to, is_trait_impl } => {
Ok(Res::SelfTyAlias { alias_to, is_trait_impl })
}
rustc_hir::def::Res::SelfTyParam { trait_ } => Ok(Res::SelfTyParam { trait_ }),
Expand Down
8 changes: 4 additions & 4 deletions crates/flux-middle/src/global_env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -697,9 +697,9 @@ impl ErrorEmitter for GlobalEnv<'_, '_> {

fn lean_parent_dir(tcx: TyCtxt) -> PathBuf {
tcx.sess
.opts
.working_dir
.local_path_if_available()
.to_path_buf()
.source_map()
.working_dir()
.local_path()
.unwrap()
.join(config::lean_dir())
}
8 changes: 4 additions & 4 deletions crates/flux-middle/src/rty/binder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,12 @@ use flux_common::tracked_span_bug;
use flux_macros::{TypeFoldable, TypeVisitable};
use flux_rustc_bridge::{
ToRustc,
ty::{BoundRegion, Region},
ty::{BoundRegion, BoundRegionKind, Region},
};
use itertools::Itertools;
use rustc_data_structures::unord::UnordMap;
use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable};
use rustc_middle::ty::{BoundRegionKind, TyCtxt};
use rustc_middle::ty::TyCtxt;
use rustc_span::Symbol;

use super::{
Expand Down Expand Up @@ -263,11 +263,11 @@ impl BoundVariableKind {
fn to_rustc<'tcx>(
vars: &[Self],
tcx: TyCtxt<'tcx>,
) -> &'tcx rustc_middle::ty::List<rustc_middle::ty::BoundVariableKind> {
) -> &'tcx rustc_middle::ty::List<rustc_middle::ty::BoundVariableKind<'tcx>> {
tcx.mk_bound_variable_kinds_from_iter(vars.iter().flat_map(|kind| {
match kind {
BoundVariableKind::Region(brk) => {
Some(rustc_middle::ty::BoundVariableKind::Region(*brk))
Some(rustc_middle::ty::BoundVariableKind::Region(brk.to_rustc(tcx)))
}
BoundVariableKind::Refine(..) => None,
}
Expand Down
Loading
Loading