Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
10 changes: 6 additions & 4 deletions dsl/std/realization_schedule.dag
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ type Runnable
source_roots: List<String>
scan_dirs: List<String>
explicit_entries: List<ScheduleWitnessEntry>
skip_unaffected_node_frontier: Bool
}

type Schedule = List<List<Runnable>>
Expand All @@ -89,7 +90,7 @@ type RealizationPlan {
fn runnable_step_label(r: Runnable) -> String {
match r {
RunnableSingleClaim { entry: _, function: f } => f
RunnableDiscoveryBatch { source_roots: _, scan_dirs: _, explicit_entries: _ } => "__discovery_corpus__"
RunnableDiscoveryBatch { source_roots: _, scan_dirs: _, explicit_entries: _, skip_unaffected_node_frontier: _ } => "__discovery_corpus__"
}
}

Expand Down Expand Up @@ -217,14 +218,15 @@ fn runnable_eq(left: Runnable, right: Runnable) -> Bool {
match left {
RunnableSingleClaim { entry: le, function: lf } => match right {
RunnableSingleClaim { entry: re, function: rf } => (le == re) && (lf == rf)
RunnableDiscoveryBatch { source_roots: _, scan_dirs: _, explicit_entries: _ } => false
RunnableDiscoveryBatch { source_roots: _, scan_dirs: _, explicit_entries: _, skip_unaffected_node_frontier: _ } => false
}
RunnableDiscoveryBatch { source_roots: lsr, scan_dirs: lsd, explicit_entries: lex } => match right {
RunnableDiscoveryBatch { source_roots: lsr, scan_dirs: lsd, explicit_entries: lex, skip_unaffected_node_frontier: lskip } => match right {
RunnableSingleClaim { entry: _, function: _ } => false
RunnableDiscoveryBatch { source_roots: rsr, scan_dirs: rsd, explicit_entries: rex } =>
RunnableDiscoveryBatch { source_roots: rsr, scan_dirs: rsd, explicit_entries: rex, skip_unaffected_node_frontier: rskip } =>
string_list_eq(left: lsr, right: rsr)
&& string_list_eq(left: lsd, right: rsd)
&& schedule_witness_entry_list_eq(left: lex, right: rex)
&& (lskip == rskip)
}
}
}
Expand Down
1 change: 1 addition & 0 deletions dsl/test/claim/realization_schedule_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ fn synthetic_correct_schedule() -> List<List<Runnable>> {
source_roots: ["dsl"]
scan_dirs: []
explicit_entries: []
skip_unaffected_node_frontier: false
},
RunnableSingleClaim { entry: gate_entry, function: "rust_monolith_gate_passes" }
]
Expand Down
38 changes: 33 additions & 5 deletions src/v1/stage0/src/bin/claim_executor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ use std::process::ExitCode;
use std::thread;

use v1_compiler::cli_run::{
make_eval_context, resolve_entry_graph, run_claim, run_discovery_corpus, run_value,
ClaimOutcome,
make_eval_context, resolve_entry_graph, run_claim, run_discovery_corpus_with_options,
run_value, ClaimOutcome, DiscoveryCorpusOptions,
};
use v1_compiler::v1_interpreter::{ExecutionMode, InterpContext, Value};

Expand All @@ -66,6 +66,7 @@ enum Runnable {
source_roots: Vec<String>,
scan_dirs: Vec<String>,
explicit_entries: Vec<(String, String)>,
skip_unaffected_node_frontier: bool,
},
}

Expand Down Expand Up @@ -218,10 +219,24 @@ fn runnable_from_value(value: &Value, ctx: &InterpContext) -> Result<Runnable, S
}
None => Vec::new(),
};
let skip_unaffected_node_frontier =
match ctx.field(fields, "skip_unaffected_node_frontier") {
Some(v) => match v {
Value::Bool(b) => *b,
other => {
return Err(format!(
"RunnableDiscoveryBatch.skip_unaffected_node_frontier must be Bool, got {}",
other.type_label_public()
))
}
},
None => false,
};
Ok(Runnable::DiscoveryBatch {
source_roots,
scan_dirs,
explicit_entries,
skip_unaffected_node_frontier,
})
}
other => Err(format!(
Expand Down Expand Up @@ -262,7 +277,13 @@ fn run_one_runnable(source_roots: Vec<String>, runnable: Runnable) -> ClaimResul
source_roots: roots,
scan_dirs,
explicit_entries,
} => run_discovery_batch_node(roots, scan_dirs, explicit_entries),
skip_unaffected_node_frontier,
} => run_discovery_batch_node(
roots,
scan_dirs,
explicit_entries,
skip_unaffected_node_frontier,
),
}
}

Expand Down Expand Up @@ -322,22 +343,27 @@ fn run_discovery_batch_node(
source_roots: Vec<String>,
scan_dirs: Vec<String>,
explicit_entries: Vec<(String, String)>,
skip_unaffected_node_frontier: bool,
) -> ClaimResult {
let label = format!(
"discovery-corpus[{} root(s)+{} explicit]",
source_roots.len(),
explicit_entries.len()
);
match run_discovery_corpus(
match run_discovery_corpus_with_options(
&source_roots,
&scan_dirs,
&explicit_entries,
ExecutionMode::Wet,
DiscoveryCorpusOptions {
skip_unaffected_node_frontier,
},
) {
Ok(summary) if summary.failures.is_empty() => {
eprintln!(
"[measurement] discovery corpus: {} witness(es), resolve {:.3}ms, evalu {:.3}ms, CostAccount.time basis=Measured {}ns",
"[measurement] discovery corpus: {} witness(es) ({} skipped), resolve {:.3}ms, evalu {:.3}ms, CostAccount.time basis=Measured {}ns",
summary.total,
summary.skipped,
summary.total_resolve_nanos as f64 / 1.0e6,
summary.total_measured_nanos as f64 / 1.0e6,
summary.total_measured_nanos,
Expand Down Expand Up @@ -621,10 +647,12 @@ fn run_perturb_check(
source_roots: roots,
scan_dirs,
explicit_entries,
skip_unaffected_node_frontier,
} => Runnable::DiscoveryBatch {
source_roots: roots.iter().map(|r| remap_root(r)).collect(),
scan_dirs: scan_dirs.iter().map(|d| remap_root(d)).collect(),
explicit_entries: explicit_entries.clone(),
skip_unaffected_node_frontier: *skip_unaffected_node_frontier,
},
})
.collect()
Expand Down
Loading
Loading