Skip to content

Commit

Permalink
Update the evaluation framework to use Nix. Run Fmt and Fix. Restruct…
Browse files Browse the repository at this point in the history
…ure the Makefile
  • Loading branch information
gavinleroy committed Nov 8, 2024
1 parent bb1f36d commit d2038cc
Show file tree
Hide file tree
Showing 17 changed files with 292 additions and 112 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -26,3 +26,4 @@ bindings/

# Evaluation cache
data/
*.csv
83 changes: 70 additions & 13 deletions Makefile.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,27 +2,84 @@
skip_core_tasks = true
default_to_workspace = false

[tasks.watch-front]
script = "cargo watch -i frontend -x 'install --path crates/argus-cli'"
# #################### #
# Binding initializers #
# #################### #

[tasks.watch-front-debug]
script = "cargo watch -i frontend -x 'install --path crates/argus-cli --frozen --offline --debug'"
[tasks.init-bindings-lib]
command = "cargo"
args = [
"test", "-p", "argus-lib", "--lib", "export_bindings", "--locked"
]

[tasks.watch.run_task]
name = ["watch-front"]
parallel = true
[tasks.init-bindings-ser]
command = "cargo"
args = ["test", "-p", "argus-ser", "--locked"]

[tasks.init-bindings]
command = "./scripts/ts-rs.scm"
dependences = ["tasks.init-bindings-lib", "tasks.init-bindings-ser"]

[tasks.evaluation-node]
command = "node"
args = ["ide/packages/evaluation/dist/evaluation.cjs", "-s", "./data", "${@}"]

# #################### #
# Builders #
# #################### #

[tasks.build-back]
command = "cargo"
args = [
"install", "--path", "crates/argus-cli", "--locked",
]

# TODO: is there a way to set a command specific environment variable?
# The below will make the configuration global...
# [env]
# CARGO_MAKE_WORKING_DIRECTORY = "ide"
[tasks.build-ide]
script = """
cargo test -p argus-lib --lib export_bindings --locked
cargo test -p argus-ser --locked
./scripts/ts-rs.scm
cd ide && depot build
"""

[tasks.evaluation]
[tasks.build.run_task]
name = ["build-back", "build-ide"]
parallel = true

[tasks.watch-back]
command = "cargo"
args = [
"watch",
"-i",
"frontend",
"-x",
"'install", "--path", "crates/argus-cli", "${@}", "'",
]

[tasks.watch.run_task]
name = ["watch-back"]
parallel = true

# ############### #
# Evaluation Crap #
# ############### #

[tasks.evaluate-inertia]
command = "node"
args = ["ide/packages/evaluation/dist/evaluation.cjs", "-h", "${@}"]
dependencies = ["build"]

[tasks.evaluation-init]
command = "node"
args = ["ide/packages/evaluation/dist/evaluation.cjs", "-s", "./data", "${@}"]
dependencies = ["build"]

[tasks.evaluation-serve]
script = """
cd ide && depot build && cd ..
node ide/packages/evaluation/dist/evaluation.cjs -s ./data
python3 -m webbrowser http://localhost:8080/eval
./scripts/evaluation.scm
"""

[tasks.evaluation]
dependencies = ["evaluation-init", "evaluation-serve"]
27 changes: 21 additions & 6 deletions crates/argus-cli/tests/test_examples.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,16 @@
use std::{env, fs, path::Path, process::Command, sync::Once};
use std::{
env, fs,
path::Path,
process::{Command, Stdio},
sync::Once,
};

use anyhow::{ensure, Context, Result};

static SETUP: Once = Once::new();

static DNF_PERF_P: &str = "dnf-perf.csv";

fn run<P: AsRef<Path>>(dir: P, f: impl FnOnce(&mut Command)) -> Result<String> {
let root = env::temp_dir().join("argus");
let heredir = Path::new(".").canonicalize()?;
Expand All @@ -17,12 +24,13 @@ fn run<P: AsRef<Path>>(dir: P, f: impl FnOnce(&mut Command)) -> Result<String> {
if !status.success() {
panic!("installing argus failed")
}

fs::write(DNF_PERF_P, "Label,N,Time\n").unwrap();
});

let mut cmd = Command::new("cargo");
cmd.arg("argus");
cmd.arg("obligations");
// Don't specify a file to analyze all local crates.
cmd.arg("bundle");

let path = format!(
"{}:{}",
Expand All @@ -34,6 +42,14 @@ fn run<P: AsRef<Path>>(dir: P, f: impl FnOnce(&mut Command)) -> Result<String> {
let ws = heredir.join("tests").join(dir);
cmd.current_dir(&ws);

// NOTE: performance data is written to STDERR, so we capture it and place it in a file.
let perf_file = fs::OpenOptions::new()
.create(true)
.append(true)
.open(DNF_PERF_P)
.unwrap();
cmd.stderr(Stdio::from(perf_file));

f(&mut cmd);

let _ = fs::remove_dir_all(ws.join("target"));
Expand Down Expand Up @@ -61,13 +77,12 @@ macro_rules! mk_tests_for {
mk_tests_for! {
axum,
bevy,
// chumsky, // NOTE: as of now this consumes too much memory
// chumsky,
diesel,
easy_ml,
// easy_ml,
entrait,
nalgebra,
uom
// tauri_project
}

// TODO: include individual test if we want to see a particular output
Expand Down
6 changes: 5 additions & 1 deletion crates/argus/src/aadebug/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ use crate::proof_tree::{topology::TreeTopology, ProofNodeIdx};
pub struct Storage<'tcx> {
pub ns: IndexVec<ProofNodeIdx, tree::N<'tcx>>,
maybe_ambiguous: bool,
report_performance: bool,
}

#[derive(Serialize, Debug, Clone)]
Expand All @@ -30,9 +31,11 @@ pub struct AnalysisResults {

impl<'tcx> Storage<'tcx> {
pub fn new(maybe_ambiguous: bool) -> Self {
let report_performance = std::env::var("ARGUS_DNF_PERF").is_ok();
Self {
ns: IndexVec::new(),
maybe_ambiguous,
report_performance,
}
}

Expand Down Expand Up @@ -106,7 +109,8 @@ impl<'tcx> Storage<'tcx> {
root: ProofNodeIdx,
topo: &TreeTopology,
) -> AnalysisResults {
let tree = &tree::T::new(root, &self.ns, topo, false);
let tree =
&tree::T::new(root, &self.ns, topo, false, self.report_performance);
let tree_start = Instant::now();

let mut sets = vec![];
Expand Down
14 changes: 14 additions & 0 deletions crates/argus/src/aadebug/tree.rs
Original file line number Diff line number Diff line change
Expand Up @@ -333,6 +333,7 @@ pub struct T<'a, 'tcx: 'a> {
pub ns: &'a IndexVec<I, N<'tcx>>,
pub topology: &'a TreeTopology,
pub maybe_ambiguous: bool,
report_performance: bool,
dnf: RefCell<Option<Dnf<I>>>,
}

Expand All @@ -342,12 +343,14 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> {
ns: &'a IndexVec<I, N<'tcx>>,
topology: &'a TreeTopology,
maybe_ambiguous: bool,
report_performance: bool,
) -> Self {
Self {
root,
ns,
topology,
maybe_ambiguous,
report_performance,
dnf: RefCell::new(None),
}
}
Expand Down Expand Up @@ -436,8 +439,19 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> {

let root = self.goal(self.root).expect("invalid root");
let dnf = _goal(self, &root).unwrap_or_else(Dnf::default);

timer::elapsed(&dnf_report_msg, dnf_start);

// HACK to gather the performance report we write to stderr the CSV values `PERF<NODES><TIME>`
// The testing harness will take the stderr output and place it in a file for analysis.
if self.report_performance {
eprintln!(
"PERF,{:?},{:.04}",
self.ns.len(),
dnf_start.elapsed().as_secs_f64()
);
}

self.dnf.replace(Some(dnf));
self.expect_dnf()
}
Expand Down
4 changes: 3 additions & 1 deletion crates/argus/src/ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,9 @@ impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> {
let items = vec![LI::Iterator, LI::Sized, LI::Deref];
let lis = self.tcx.lang_items();
for i in items {
if let Some(def_id) = lis.get(i) && p.is_trait_pred_rhs(def_id) {
if let Some(def_id) = lis.get(i)
&& p.is_trait_pred_rhs(def_id)
{
return true;
}
}
Expand Down
34 changes: 2 additions & 32 deletions crates/argus/src/proof_tree/serialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ impl SerializedTreeVisitor<'_> {
}

fn check_goal_projection(&mut self, goal: &InspectGoal) {
// We only care about successful alias relations
if goal.result().is_yes()
&& let ty::PredicateKind::AliasRelate(
t1,
Expand All @@ -74,46 +75,15 @@ impl SerializedTreeVisitor<'_> {
let idx2: TyIdx = interner.borrow().get_idx(&t2)?;
Some((idx1, idx2))
}) && t1 != t2
&& !self.projection_values.contains_key(&t1)
{
let not_empty = self.projection_values.insert(t1, t2);
debug_assert!(not_empty.is_none());
}
}
}

#[cfg(debug_assertions)]
fn is_valid(&self) -> Result<()> {
for (pidx, node) in self.nodes.iter_enumerated() {
match node {
Node::Goal(g) => {
anyhow::ensure!(
!self.topology.is_leaf(pidx),
"non-leaf node (goal) has no children {:?}",
self.interners.goal(*g)
);
}
Node::Candidate(c) => {
anyhow::ensure!(
!self.topology.is_leaf(pidx),
"non-leaf node (candidate) has no children {:?}",
self.interners.candidate(*c)
);
}
Node::Result(..) => {
anyhow::ensure!(
self.topology.is_leaf(pidx),
"result node is not a leaf"
);
}
}
}
Ok(())
}

pub fn into_tree(self) -> Result<SerializedTree> {
#[cfg(debug_assertions)]
self.is_valid()?;

let SerializedTreeVisitor {
root: Some(root),
mut nodes,
Expand Down
Loading

0 comments on commit d2038cc

Please sign in to comment.