diff --git a/Makefile.toml b/Makefile.toml index 1fe56e6..8cdd217 100644 --- a/Makefile.toml +++ b/Makefile.toml @@ -21,7 +21,7 @@ cargo test -p argus-lib --lib export_bindings --locked [tasks.evaluation] script = """ cd ide && depot build && cd .. -node ide/packages/evaluation/dist/evaluation.cjs ./data +node ide/packages/evaluation/dist/evaluation.cjs -s ./data python3 -m webbrowser http://localhost:8080/eval ./scripts/evaluation.scm """ diff --git a/ide/packages/common/src/lib.ts b/ide/packages/common/src/lib.ts index dc9fff0..71afec4 100644 --- a/ide/packages/common/src/lib.ts +++ b/ide/packages/common/src/lib.ts @@ -30,9 +30,11 @@ export const ConfigConsts = { export type PanoptesInitialData = { data: [Filename, ObligationsInBody[]][]; target?: ErrorJumpTargetInfo; + evalMode?: EvaluationMode; }; export type SystemSpec = Omit; +export type EvaluationMode = "release" | "rank" | "random"; export type PanoptesConfig = PanoptesInitialData & ( diff --git a/ide/packages/evaluation/src/main.ts b/ide/packages/evaluation/src/main.ts index 1863161..90c8cb5 100644 --- a/ide/packages/evaluation/src/main.ts +++ b/ide/packages/evaluation/src/main.ts @@ -1,17 +1,28 @@ import { BodyBundle } from "@argus/common/bindings"; -import { Filename, Result } from "@argus/common/lib"; +import { EvaluationMode, Filename, Result } from "@argus/common/lib"; import { ExecNotifyOpts, execNotify as _execNotify } from "@argus/system"; import fs from "fs"; import _ from "lodash"; import path from "path"; -import { chromium } from "playwright"; +import { + BrowserContext, + ElementHandle, + Page, + chromium, + selectors, +} from "playwright"; import tmp from "tmp"; //@ts-ignore import uniqueFilename from "unique-filename"; import { webHtml } from "./page"; +import { rootCauses } from "./rootCauses"; import { PORT, fileServer } from "./serve"; +declare global { + var debugging: boolean; +} + // See: https://doc.rust-lang.org/cargo/reference/external-tools.html // https://doc.rust-lang.org/rustc/json.html // for up-to-date information on the structure of diagnostics output. @@ -45,38 +56,81 @@ async function sleep(waitTime: number) { return new Promise(resolve => setTimeout(resolve, waitTime)); } +async function forFileInBundle( + bundles: BodyBundle[], + f: (filename: Filename, bundles: BodyBundle[]) => Promise +) { + const groupedByFilename = _.groupBy(bundles, b => b.filename); + return await Promise.all( + _.map(groupedByFilename, async (bundles, filename) => { + return f(filename, bundles); + }) + ); +} + +async function openPage( + context: BrowserContext, + filename: string, + bundles: BodyBundle[], + evalMode: EvaluationMode +) { + const tmpobj = tmp.fileSync({ postfix: ".html" }); + const html = webHtml("EVAL", filename, bundles, evalMode); + fs.writeSync(tmpobj.fd, html); + const page = await context.newPage(); + await page.goto(`file://${tmpobj.name}`, { + waitUntil: "domcontentloaded", + timeout: 30_000, + }); + return page; +} + +async function expandBottomUpView(page: Page) { + let bs = await page.getByText("Bottom Up").all(); + try { + // await Promise.all( + // _.map(bs, async b => { + // try { + // await b.waitFor({ state: "visible" }); + // } catch (e: any) {} + // }) + // ); + await Promise.all( + _.map(bs, async b => { + try { + await b.click(); + } catch (e: any) {} + }) + ); + } catch (e: any) { + console.debug("Error clicking bottom up", e); + } +} + // Take bundled argus output and take a screenshot of the tree loaded into the browser. async function argusScreenshots( outDir: fs.PathLike, bundles: BodyBundle[], title: string = "Argus Output" ) { - const browser = await chromium.launch({ headless: true }); + const browser = await chromium.launch({ headless: !global.debugging }); const context = await browser.newContext(); const innerDoScreenshot = async ( - tmpobj: tmp.FileResult, out: string, filename: Filename, bundles: BodyBundle[] ) => { - const html = webHtml(title, filename, bundles); - fs.writeSync(tmpobj.fd, html); - const page = await context.newPage(); - await page.goto(`file://${tmpobj.name}`); - await sleep(6000); - await page.screenshot({ path: out, fullPage: false }); + const page = await openPage(context, filename, bundles, "rank"); + await expandBottomUpView(page); + await page.screenshot({ path: out, fullPage: true }); }; - const groupedByFilename = _.groupBy(bundles, b => b.filename); - return await Promise.all( - _.map(groupedByFilename, async (bundles, filename) => { - const tmpobj = tmp.fileSync({ postfix: ".html" }); - const outfile = uniqueFilename(outDir) + ".png"; - await innerDoScreenshot(tmpobj, outfile, filename, bundles); - return { filename, outfile }; - }) - ); + return forFileInBundle(bundles, async (filename, bundles) => { + const outfile = uniqueFilename(outDir) + ".png"; + await innerDoScreenshot(outfile, filename, bundles); + return { filename, outfile }; + }); } async function argusData(dir: string) { @@ -116,6 +170,145 @@ const testCases = [ "uom", ] as const; +async function runForJson(func: () => Promise) { + return JSON.stringify(JSON.stringify(await func())); +} + +async function runRandom(N: number) { + fileServer().listen(PORT); + const workspaceDir = path.resolve(__dirname, "..", "workspaces"); + const browser = await chromium.launch({ headless: !global.debugging }); + const context = await browser.newContext(); + context.setDefaultTimeout(5_000); + + const innerF = async (workspace: string, causes: any[]) => { + const fullSubdir = path.resolve(workspaceDir, workspace); + const argusBundles = await argusData(fullSubdir); + + if (!("Ok" in argusBundles)) throw new Error("Argus failed"); + const fileBundles = (await forFileInBundle( + argusBundles.Ok, + async (filename, bundles) => [filename, bundles] + )) as [string, BodyBundle[]][]; + + let results = []; + for (const [filename, bundles] of fileBundles) { + const cause = _.find(causes, cause => filename.endsWith(cause.file)); + + if (!cause) { + console.error(`No cause found for ${filename} in ${workspace}`); + continue; + } + console.debug(`Running ${N} samples for ${filename}`); + let ranks = await Promise.all( + _.times(N, async () => { + const page = await openPage(context, filename, bundles, "random"); + await sleep(3000); + await expandBottomUpView(page); + await sleep(3000); + try { + const goals = await page + .locator(".BottomUpArea .EvalGoal") + .filter({ hasText: cause.message }) + .all(); + + const ranksStr = await Promise.all( + _.map(goals, goal => goal.getAttribute("data-rank")) + ); + + return _.min(_.map(_.compact(ranksStr), r => Number(r))); + } catch (e) { + return undefined; + } finally { + await page.close(); + } + }) + ); + + const noUndef = _.compact(ranks); + if (noUndef.length === 0) { + console.error(`No ranks found for ${filename} in ${workspace}`); + } + + results.push({ + workspace, + filename, + cause: cause.message, + ranks: noUndef, + }); + } + + return results; + }; + + let results = []; + for (const { workspace, causes } of rootCauses) { + results.push(await innerF(workspace, causes)); + } + + return _.flatten(results); +} + +async function runEvaluation() { + fileServer().listen(PORT); + const workspaceDir = path.resolve(__dirname, "..", "workspaces"); + const browser = await chromium.launch({ headless: !global.debugging }); + const context = await browser.newContext(); + const results = await Promise.all( + _.map(rootCauses, async ({ workspace, causes }) => { + const fullSubdir = path.resolve(workspaceDir, workspace); + const argusBundles = await argusData(fullSubdir); + + if (!("Ok" in argusBundles)) throw new Error("Argus failed"); + return forFileInBundle(argusBundles.Ok, async (filename, bundles) => { + const cause = _.find(causes, cause => filename.endsWith(cause.file)) as + | { file: string; message: string } + | undefined; + + if (!cause) return; + const page = await openPage(context, filename, bundles, "rank"); + + await sleep(5000); + await expandBottomUpView(page); + await sleep(5000); + + const goals = await page + .locator(".BottomUpArea .EvalGoal") + .filter({ hasText: cause.message }) + .all(); + + console.debug( + `Found ${filename}:${goals.length} goals ${cause.message}` + ); + + const ranksStr = await Promise.all( + _.map(goals, goal => goal.getAttribute("data-rank")) + ); + const rank = _.min(_.map(_.compact(ranksStr), r => Number(r))); + + const numberTreeNodes = _.max( + _.flatten( + _.map(bundles, bundle => + _.map(_.values(bundle.trees), tree => tree.nodes.length) + ) + ) + ); + + await page.close(); + return { + workspace, + filename, + cause: cause.message, + numberTreeNodes, + rank, + }; + }); + }) + ); + + return _.filter(_.compact(_.flatten(results)), v => v.rank !== undefined); +} + async function outputInDir(resultsDir: string) { fileServer().listen(PORT); ensureDir(resultsDir); @@ -158,15 +351,35 @@ async function outputInDir(resultsDir: string) { ); } -async function main() { - const cacheDirectory = process.argv[2]; - if (cacheDirectory === undefined) { - throw new Error("Must provide a cache directory"); - } - +async function runScreenshots(cacheDirectory: string) { const results = await outputInDir(cacheDirectory); const mapFile = path.resolve(cacheDirectory, "results-map.json"); fs.writeFileSync(mapFile, JSON.stringify(results)); +} + +async function main() { + global.debugging = _.includes(process.argv, "--debug"); + const argv = _.filter(process.argv, arg => arg !== "--debug"); + + switch (argv[2]) { + case "-r": { + const N = Number(argv[3] ?? "10"); + await runForJson(() => runRandom(N)).then(console.log); + break; + } + case "-h": { + await runForJson(() => runEvaluation()).then(console.log); + break; + } + case "-s": { + const cacheDirectory = argv[3]; + if (cacheDirectory === undefined) + throw new Error("Must provide a cache directory"); + await runScreenshots(cacheDirectory); + } + default: + throw new Error("Invalid CLI argument"); + } process.exit(0); } diff --git a/ide/packages/evaluation/src/page.ts b/ide/packages/evaluation/src/page.ts index 88c8d82..3fbe680 100644 --- a/ide/packages/evaluation/src/page.ts +++ b/ide/packages/evaluation/src/page.ts @@ -2,6 +2,7 @@ import { BodyBundle } from "@argus/common/bindings"; import { ConfigConsts, ErrorJumpTargetInfo, + EvaluationMode, Filename, PanoptesConfig, configToString, @@ -13,6 +14,41 @@ import { PORT } from "./serve"; // Default VSCode Light styles export const defaultStyles = ` +--background: #ffffff; +--contrast-active-border: transparent; +--focus-border: #0090f1; +--font-family: -apple-system, BlinkMacSystemFont, sans-serif; +--font-weight: normal; +--foreground: #616161; +--scrollbar-slider-background: rgba(100, 100, 100, 0.4); +--scrollbar-slider-hover-background: rgba(100, 100, 100, 0.7); +--scrollbar-slider-active-background: rgba(0, 0, 0, 0.6); +--badge-background: #c4c4c4; +--badge-foreground: #333333; +--button-primary-background: #007acc; +--button-primary-hover-background: #0062a3; +--button-secondary-background: #5f6a79; +--button-secondary-hover-background: #4c5561; +--checkbox-background: #ffffff; +--checkbox-border: #919191; +--checkbox-foreground: #616161; +--list-active-selection-background: #0060c0; +--list-hover-background: #e8e8e8; +--divider-background: #c8c8c8; +--dropdown-background: #ffffff; +--dropdown-border: #cecece; +--dropdown-foreground: #616161; +--input-background: #ffffff; +--input-foreground: #616161; +--input-placeholder-foreground: #767676; +--link-active-foreground: #006ab1; +--link-foreground: #006ab1; +--panel-tab-active-border: #424242; +--panel-tab-active-foreground: #424242; +--panel-tab-foreground: rgba(66, 66, 66, 0.75); +--panel-view-background: #ffffff; +--panel-view-border: rgba(128, 128, 128, 0.35); + --vscode-foreground: #616161; --vscode-disabledForeground: rgba(97, 97, 97, 0.5); --vscode-errorForeground: #a1260d; @@ -704,13 +740,15 @@ function findErrorTargetInBundles(bundles: BodyBundle[]) { export function webHtml( title: string, filename: Filename, - bundles: BodyBundle[] + bundles: BodyBundle[], + evalMode: EvaluationMode = "rank" ) { const config: PanoptesConfig = { type: "WEB_BUNDLE", target: findErrorTargetInBundles(bundles), data: [[filename, bundles.map(b => b.body)]], closedSystem: bundles, + evalMode, }; const panoptesDir = path.resolve(__dirname, "..", "..", "panoptes"); diff --git a/ide/packages/evaluation/src/rootCauses.ts b/ide/packages/evaluation/src/rootCauses.ts new file mode 100644 index 0000000..29ea31a --- /dev/null +++ b/ide/packages/evaluation/src/rootCauses.ts @@ -0,0 +1,80 @@ +export interface RootCause { + workspace: string; + causes: [ + { + file: string; + message: string; + } + ]; +} + +export const rootCauses = [ + { + workspace: "diesel", + causes: [ + { + file: "bad_sql_query.rs", + message: "User: QueryableByName", + }, + { + file: "queryable_order_mismatch.rs", + message: "(String, i32): FromSql", + }, + { + file: "invalid_select.rs", + message: "id: SelectableExpression", + }, + { + file: "invalid_query.rs", + message: "Count == Once", + }, + ], + }, + { + workspace: "axum", + causes: [ + { + file: "argument_not_extractor.rs", + message: "bool: FromRequestParts", + }, + { + file: "extract_self_mut.rs", + message: "&'_ mut A: FromRequestParts", + }, + { + file: "extract_self_ref.rs", + message: "&'_ A: FromRequestParts", + }, + { + file: "missing_deserialize.rs", + message: "Test: Deserialize", + }, + { + file: "multiple_body_extractors.rs", + message: "String: FromRequestParts", + }, + { + file: "request_not_last.rs", + message: "Request: FromRequestParts", + }, + ], + }, + { + workspace: "bevy", + causes: [ + { + file: "main.rs", + message: "Timer: SystemParam", + }, + ], + }, + { + workspace: "nalgebra", + causes: [ + { + file: "mat_mul.rs", + message: "ShapeConstraint", + }, + ], + }, +]; diff --git a/ide/packages/extension/src/view.ts b/ide/packages/extension/src/view.ts index d71cb21..b88c4f4 100644 --- a/ide/packages/extension/src/view.ts +++ b/ide/packages/extension/src/view.ts @@ -66,6 +66,7 @@ export class View { this.panel = vscode.window.createWebviewPanel("argus", "Argus", column, { enableScripts: true, retainContextWhenHidden: true, + enableFindWidget: true, localResourceRoots: [this.extensionUri], }); this.isPanelDisposed = false; diff --git a/ide/packages/panoptes/src/App.tsx b/ide/packages/panoptes/src/App.tsx index 7e34384..01f55e6 100644 --- a/ide/packages/panoptes/src/App.tsx +++ b/ide/packages/panoptes/src/App.tsx @@ -1,5 +1,6 @@ import { ErrorJumpTargetInfo, + EvaluationMode, PanoptesConfig, SystemSpec, SystemToPanoptesCmds, @@ -42,6 +43,10 @@ const App = observer(({ config }: { config: PanoptesConfig }) => { const systemSpec = config.type === "VSCODE_BACKING" ? config.spec : webSysSpec; + config.evalMode = config.evalMode ?? "release"; + const configNoUndef: PanoptesConfig & { evalMode: EvaluationMode } = + config as any; + // NOTE: this listener should only listen for posted messages, not // for things that could be an expected response from a webview request. const listener = (e: MessageEvent) => { @@ -84,11 +89,13 @@ const App = observer(({ config }: { config: PanoptesConfig }) => { }; return ( - - - - - + + + + + + + ); }); diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.css b/ide/packages/panoptes/src/TreeView/BottomUp.css new file mode 100644 index 0000000..e69de29 diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx index bfd3850..dd1ea72 100644 --- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx +++ b/ide/packages/panoptes/src/TreeView/BottomUp.tsx @@ -1,15 +1,19 @@ import { ProofNodeIdx, TreeTopology } from "@argus/common/bindings"; import _ from "lodash"; import React, { useContext } from "react"; +import { flushSync } from "react-dom"; +import { createRoot } from "react-dom/client"; -import { TreeAppContext } from "../utilities/context"; -import { mean, mode, searchObject, stdDev } from "../utilities/func"; +import { PrintGoal } from "../print/print"; +import { AppContext, TreeAppContext } from "../utilities/context"; +import "./BottomUp.css"; import { CollapsibleElement, DirRecursive, TreeRenderParams, } from "./Directory"; import { TreeInfo, TreeView } from "./TreeInfo"; +import { treeHeuristic } from "./heuristic"; type TreeViewWithRoot = TreeView & { root: ProofNodeIdx }; @@ -79,7 +83,7 @@ class TopologyBuilder { function invertViewWithRoots( leaves: ProofNodeIdx[], tree: TreeInfo -): Array { +): TreeViewWithRoot[] { const groups: ProofNodeIdx[][] = _.values( _.groupBy(leaves, leaf => { const node = tree.node(leaf); @@ -109,146 +113,79 @@ function invertViewWithRoots( }); } -const BottomUp = () => { - const tree = useContext(TreeAppContext.TreeContext)!; - const mkGetChildren = (view: TreeView) => (idx: ProofNodeIdx) => - view.topology.children[idx] ?? []; - - const liftTo = (idx: ProofNodeIdx, target: "Goal" | "Candidate") => { - let curr: ProofNodeIdx | undefined = idx; - while (curr !== undefined && !(target in tree.node(curr))) { - curr = tree.parent(curr); - } - return curr; +const RenderEvaluationViews = ({ + recommended, + others, + mode, +}: { + recommended: TreeViewWithRoot[]; + others: TreeViewWithRoot[]; + mode: "rank" | "random"; +}) => { + const nodeToString = (node: React.ReactNode) => { + const div = document.createElement("div"); + const root = createRoot(div); + flushSync(() => root.render(node)); + return div.innerText; }; - const leaves = _.uniq( - _.compact(_.map(tree.errorLeaves(), n => liftTo(n, "Goal"))) - ); - const failedGroups = _.groupBy(leaves, leaf => tree.parent(leaf)); - - // Operations on groups of errors - const numMainUninferred = (group: ProofNodeIdx[]) => - _.reduce( - group, - (acc, leaf) => - acc + - (() => { - const node = tree.node(leaf); - if ("Goal" in node) { - const goal = tree.goal(node.Goal); - return goal.isMainTv ? 1 : 0; - } else { - return 0; - } - })(), - 0 - ); - - const getNumPrincipaled = (group: ProofNodeIdx[]) => - group.length - numMainUninferred(group); - - const sortByNPT = (group: ProofNodeIdx[]) => -getNumPrincipaled(group); - - const sortByNPTRatio = (group: ProofNodeIdx[]) => - group.length / getNumPrincipaled(group); - - const sortByDepth = (group: ProofNodeIdx[]) => - -_.max(_.map(group, leaf => tree.depth(leaf)))!; - - const takeN = (n: number) => (groups: ProofNodeIdx[][]) => - [_.take(groups, n), _.tail(groups)] as [ProofNodeIdx[][], ProofNodeIdx[][]]; - - const takeAll = (groups: ProofNodeIdx[][]) => - [groups, []] as [ProofNodeIdx[][], ProofNodeIdx[][]]; - - // HACK: this crappy heuristic needs to be replaced with a proper analysis. - const [sortStrategy, firstFilter] = (() => { - const npts = _.map(failedGroups, getNumPrincipaled); - const meanNPT = mean(npts); - const stdDevNPT = stdDev(npts, meanNPT); - const onlyHigh = _.filter(npts, npt => npt > meanNPT + stdDevNPT); - if (onlyHigh.length > 0) { - return [sortByNPT, takeN(onlyHigh.length)]; - } - - const nptRatioEq = _.filter( - failedGroups, - group => group.length === getNumPrincipaled(group) - ); - if (nptRatioEq.length > 0) { - return [sortByNPTRatio, takeN(nptRatioEq.length)]; - } - - return [sortByDepth, takeAll]; - })(); - - const sortedGroups = _.sortBy(_.values(failedGroups), [ - // Getting the right group is important but it's not precise. - // We currently use the following metrics. - // - // 1. The number of obligations whose "principle types" are known (NPT). - // What this entails is that in an obligation such as `TYPE: TRAIT`, - // neither TYPE nor TRAIT is an unresolved type variable `_`. - // - // We use this number, NPT, to find groups whose NPT is more than - // one standard deviation from the mean. This is useful when trait impls are - // macro generated for varying arities, larger arities have a high number of - // unresolved type variables. - // - // The above is useful, until it isn't. Then, we can use tha ratio - // of group size vs the NPT. This favors smaller groups with more - // concrete types. - // - // 2. Depth of the group. Generally, deep obligations are "more interesting." - sortStrategy, - ]); + const tree = useContext(TreeAppContext.TreeContext)!; + let together = _.concat(recommended, others); - const [importantGroups, rest] = firstFilter(sortedGroups); + if (mode === "random") { + together = _.shuffle(together); + } - // The "Argus recommended" errors are shown expanded, and the - // "others" are collapsed. Argus recommended errors are the ones - // that failed or are ambiguous with a concrete type on the LHS. - const [argusRecommendedLeaves, others] = _.partition( - _.flatten(importantGroups), - leaf => { - const node = tree.node(leaf); - if ("Goal" in node) { - const goal = tree.goal(node.Goal); - const result = tree.result(goal.result); - return ( - !goal.isMainTv && (result === "no" || result === "maybe-overflow") - ); - } else { - // Leaves should only be goals... - throw new Error(`Leaves should only be goals ${node}`); - } - } + const [goals, setGoals] = React.useState([]); + const nodeList: React.ReactNode[] = _.compact( + _.map(together, (leaf, i) => { + const node = tree.node(leaf.root); + return "Goal" in node ? ( + + ) : null; + }) ); - const hiddenLeaves = _.concat(_.flatten(rest), others); - const argusViews = invertViewWithRoots(argusRecommendedLeaves, tree); - const otherViews = invertViewWithRoots(hiddenLeaves, tree); + React.useEffect(() => { + // run outside of react lifecycle + window.setTimeout(() => setGoals(_.map(nodeList, nodeToString))); + }, []); - const LeafElement = ({ leaf }: { leaf: TreeViewWithRoot }) => ( - + return ( +
+ {_.map(goals, (s, i) => ( +
+ {s} +
+ ))} +
); +}; - const recommendedSortedViews = tree.sortByRecommendedOrder( - _.flatten(argusViews), - v => v.root - ); - const recommended = _.map(recommendedSortedViews, (leaf, i) => ( - - )); +/** + * The actual entry point for rendering the bottom up view. All others are used in testing or evaluation. + */ +const RenderBottomUpViews = ({ + recommended, + others, +}: { + recommended: TreeViewWithRoot[]; + others: TreeViewWithRoot[]; +}) => { + const mkGetChildren = (view: TreeView) => (idx: ProofNodeIdx) => + view.topology.children[idx] ?? []; + const mkTopLevel = (views: TreeViewWithRoot[]) => + _.map(views, (leaf, i) => ( + + )); + + const argusViews = mkTopLevel(recommended); const fallbacks = others.length === 0 ? null : ( Other failures ...} - Children={() => - _.map(otherViews, (leaf, i) => ) - } + info={Other failures ...} + Children={() => mkTopLevel(others)} /> ); @@ -265,10 +202,49 @@ const BottomUp = () => { return ( - {recommended} + {fallbacks} ); }; +const BottomUp = () => { + const tree = useContext(TreeAppContext.TreeContext)!; + const evaluationMode = + useContext(AppContext.ConfigurationContext)?.evalMode ?? "release"; + + const liftTo = (idx: ProofNodeIdx, target: "Goal" | "Candidate") => { + let curr: ProofNodeIdx | undefined = idx; + while (curr !== undefined && !(target in tree.node(curr))) { + curr = tree.parent(curr); + } + return curr; + }; + + const H = treeHeuristic(tree); + + const leaves = _.uniq( + _.compact(_.map(tree.errorLeaves(), n => liftTo(n, "Goal"))) + ); + + const failedGroups = _.groupBy(leaves, leaf => tree.parent(leaf)); + const [argusRecommendedLeaves, hiddenLeaves] = H.partition(failedGroups); + const sortViews = (views: TreeViewWithRoot[]) => H.rank(views, v => v.root); + const argusViews = sortViews( + invertViewWithRoots(argusRecommendedLeaves, tree) + ); + const otherViews = sortViews(invertViewWithRoots(hiddenLeaves, tree)); + + // A bit of a hack to allow the evaluation script to render the bottom up view differently. + return evaluationMode === "release" ? ( + + ) : ( + + ); +}; + export default BottomUp; diff --git a/ide/packages/panoptes/src/TreeView/Directory.tsx b/ide/packages/panoptes/src/TreeView/Directory.tsx index 5e0de69..ec9c564 100644 --- a/ide/packages/panoptes/src/TreeView/Directory.tsx +++ b/ide/packages/panoptes/src/TreeView/Directory.tsx @@ -10,7 +10,7 @@ import { IcoTriangleDown, IcoTriangleRight, } from "../Icons"; -import { TreeAppContext } from "../utilities/context"; +import { AppContext, TreeAppContext } from "../utilities/context"; import "./Directory.css"; import { Node } from "./Node"; @@ -34,7 +34,10 @@ export const CollapsibleElement = ({ startOpen?: boolean; Children: React.FC | null; }) => { - const [isOpen, setIsOpen] = useState(startOpen); + const config = useContext(AppContext.ConfigurationContext)!; + const openByDefault = startOpen || config.evalMode !== "release"; + + const [isOpen, setIsOpen] = useState(openByDefault); const [openIco, closedIco] = icons; let [children, setChildren] = useState( undefined diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx index c7230dd..c5596fa 100644 --- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx +++ b/ide/packages/panoptes/src/TreeView/TreeApp.tsx @@ -5,9 +5,9 @@ import { VSCodePanels, } from "@vscode/webview-ui-toolkit/react"; import _ from "lodash"; -import React from "react"; +import React, { useContext } from "react"; -import { TreeAppContext } from "../utilities/context"; +import { AppContext, TreeAppContext } from "../utilities/context"; import BottomUp from "./BottomUp"; import TopDown from "./TopDown"; import "./TreeApp.css"; @@ -21,6 +21,7 @@ const TreeApp = ({ tree: SerializedTree | undefined; showHidden?: boolean; }) => { + const evalMode = useContext(AppContext.ConfigurationContext)!.evalMode; // FIXME: this shouldn't ever happen, if a properly hashed // value is sent and returned. I need to think more about how to handle // when we want to display "non-traditional" obligations. @@ -46,7 +47,8 @@ const TreeApp = ({ tabs.unshift(["Bottom Up", BottomUp]); } - if (tree.cycle !== undefined) { + // HACK: we shouldn't test for eval mode here but Playwright is off on the button click. + if (tree.cycle !== undefined && evalMode === "release") { // FIXME: why do I need the '!' here? - - - - - -------- VVVVVVVV tabs.unshift(["Cycle Detected", () => ]); } diff --git a/ide/packages/panoptes/src/TreeView/TreeInfo.ts b/ide/packages/panoptes/src/TreeView/TreeInfo.ts index 2991c42..befbc17 100644 --- a/ide/packages/panoptes/src/TreeView/TreeInfo.ts +++ b/ide/packages/panoptes/src/TreeView/TreeInfo.ts @@ -232,56 +232,6 @@ export class TreeInfo { return errorLeaves; } - public sortByRecommendedOrder(data: T[], f: (t: T) => ProofNodeIdx): T[] { - const sortErrorsFirst = (t: T) => { - const leaf = f(t); - switch (this.nodeResult(leaf)) { - case "no": - return 0; - case "maybe-overflow": - case "maybe-ambiguity": - return 1; - case "yes": - return 2; - } - }; - - const sortWeightPaths = (t: T) => { - const leaf = f(t); - const pathToRoot = this.pathToRoot(leaf); - const len = pathToRoot.path.length; - const numVars = _.reduce( - pathToRoot.path, - (sum, k) => sum + this.inferVars(k), - 0 - ); - - return numVars / len; - }; - - const bubbleTraitClauses = (t: T) => { - const leaf = f(t); - const n = this.node(leaf); - if ("Goal" in n && isTraitClause(this.goal(n.Goal).value.predicate)) { - return 0; - } - return 1; - }; - - const recommendedOrder = _.sortBy(data, [ - bubbleTraitClauses, - sortErrorsFirst, - sortWeightPaths, - ]); - - return recommendedOrder; - } - - public errorLeavesRecommendedOrder(): ProofNodeIdx[] { - const viewLeaves = this.errorLeaves(); - return this.sortByRecommendedOrder(viewLeaves, _.identity); - } - public inferVars(n: ProofNodeIdx): number { const current = this.numInferVars.get(n); if (current !== undefined) { diff --git a/ide/packages/panoptes/src/TreeView/heuristic.ts b/ide/packages/panoptes/src/TreeView/heuristic.ts new file mode 100644 index 0000000..a7321ea --- /dev/null +++ b/ide/packages/panoptes/src/TreeView/heuristic.ts @@ -0,0 +1,267 @@ +import { ProofNodeIdx } from "@argus/common/bindings"; +import _ from "lodash"; + +import { isTraitClause, mean, stdDev } from "../utilities/func"; +import TreeInfo from "./TreeInfo"; + +interface HeuristicI { + // Partition sets of failed nodes into two groups. + partition( + groups: _.Dictionary + ): [ProofNodeIdx[], ProofNodeIdx[]]; + + rank(data: T[], f: (t: T) => ProofNodeIdx): T[]; +} + +export function treeHeuristic(tree: TreeInfo): HeuristicI { + return new Heuristic(tree); +} + +type Strategy = { + size: number; + sorter: (group: ProofNodeIdx[]) => number; + partitioner: (n: number) => (groups: T[]) => [T[], T[]]; +}; + +type PartitionTup = [T[], T[]]; +function takeN(n: number) { + return function (groups: T[]): PartitionTup { + return [_.slice(groups, 0, n), _.slice(groups, n)]; + }; +} + +function takeAll(groups: T[]) { + return takeN(groups.length)(groups); +} + +class Heuristic implements HeuristicI { + public constructor(readonly tree: TreeInfo) {} + + numMainUninferred(group: ProofNodeIdx[]) { + return _.reduce( + group, + (acc, leaf) => + acc + + (() => { + const node = this.tree.node(leaf); + if ("Goal" in node) { + const goal = this.tree.goal(node.Goal); + return goal.isMainTv ? 1 : 0; + } else { + return 0; + } + })(), + 0 + ); + } + + numPrincipled(group: ProofNodeIdx[]) { + return group.length - this.numMainUninferred(group); + } + + maxDepth(group: ProofNodeIdx[]) { + return _.max(_.map(group, leaf => this.tree.depth(leaf)))!; + } + + numOutliers(group: T[], f: (g: T) => number) { + const data = _.map(group, f); + const meanD = mean(data); + const stdDevD = stdDev(data, meanD); + return _.filter(data, d => d > meanD + stdDevD).length; + } + + sortByNPT() { + return (group: ProofNodeIdx[]) => -this.numPrincipled(group); + } + + sortByNPTRatio() { + return (group: ProofNodeIdx[]) => group.length / this.numPrincipled(group); + } + + sortByDepth() { + return (group: ProofNodeIdx[]) => + -_.max(_.map(group, leaf => this.tree.depth(leaf)))!; + } + + // ---------------------- + // Partitioning Algorithm + + // NOTE: partitioning with heuristics can alsways be improved. + partition( + failedGroups: _.Dictionary + ): PartitionTup { + // Getting the right group is important but it's not precise. + // We currently use the following metrics. + // + // 1. Depth of the group. Generally, deep obligations are "more interesting." + // + // 2. The number of obligations whose "principle types" are known (NPT). + // What this entails is that in an obligation such as `TYPE: TRAIT`, + // neither TYPE nor TRAIT is an unresolved type variable `_`. + // + // We use this number, NPT, to find groups whose NPT is more than + // one standard deviation from the mean. This is useful when trait impls are + // macro generated for varying arities, larger arities have a high number of + // unresolved type variables. + // + // 3. The NPT is useful, until it isn't. We use the ratio of group size by + // NPT to favor smaller groups with more concrete types. + const failedValues = _.values(failedGroups); + const strategies: Strategy[] = [ + { + size: this.numOutliers(failedValues, g => this.maxDepth(g)), + sorter: this.sortByDepth(), + partitioner: takeN, + }, + { + size: this.numOutliers(failedValues, g => this.numPrincipled(g)), + sorter: this.sortByNPT(), + partitioner: takeN, + }, + { + size: this.numOutliers( + failedValues, + group => group.length / this.numPrincipled(group) + ), + sorter: this.sortByNPTRatio(), + partitioner: takeN, + }, + ]; + + const sortedAndPartitioned = _.map(strategies, s => + this.applyStrategy(failedValues, s) + ); + + // Combine all strategies to get the final partition. + const [importantGroupsNonUnq, restNonUnq] = _.reduce( + sortedAndPartitioned, + ([accImp, accRest], [imp, rest]) => [ + _.concat(accImp, _.flatten(imp)), + _.concat(accRest, _.flatten(rest)), + ], + [[], []] as PartitionTup + ); + + const [importantGroups, restWithDups] = [ + _.uniq(importantGroupsNonUnq), + _.uniq(restNonUnq), + ]; + + // Remove recommended nodes from the hidden nodes, this can happen if + // one sort strategy recommends one while another doesn't. + const rest = _.difference(restWithDups, importantGroups); + + // The "Argus recommended" errors are shown expanded, and the + // "others" are collapsed. Argus recommended errors are the ones + // that failed or are ambiguous with a concrete type on the LHS. + const [argusRecommendedLeaves, others] = + this.partitionSingles(importantGroups); + + // Fallback to sorting by depth and showing everything. This, of course, is a HACK. + if (argusRecommendedLeaves.length === 0) { + return this.partitionDefault(failedValues); + } + + const hiddenLeaves = _.concat(rest, others); + return [argusRecommendedLeaves, hiddenLeaves]; + } + + applyStrategy( + groups: ProofNodeIdx[][], + { size, sorter, partitioner }: Strategy + ) { + return size > 0 + ? partitioner(size)(_.sortBy(groups, sorter)) + : ([[], []] as PartitionTup); + } + + partitionSingles(group: ProofNodeIdx[]) { + return _.partition(group, leaf => { + const node = this.tree.node(leaf); + if ("Goal" in node) { + const goal = this.tree.goal(node.Goal); + const result = this.tree.result(goal.result); + return ( + !goal.isMainTv && (result === "no" || result === "maybe-overflow") + ); + } else { + // Leaves should only be goals... + throw new Error(`Leaves should only be goals ${node}`); + } + }); + } + + partitionDefault(failedGroups: ProofNodeIdx[][]) { + const defaultStrategy = { + size: failedGroups.length, + sorter: this.sortByDepth(), + partitioner: (_: any) => takeAll, + }; + const [important, hiddenLeaves] = this.applyStrategy( + failedGroups, + defaultStrategy + ); + const [argusRecommendedLeaves, others] = this.partitionSingles( + _.flatten(important) + ); + return [ + argusRecommendedLeaves, + _.concat(_.flatten(hiddenLeaves), others), + ] as PartitionTup; + } + + // ------------------------- + // Sort a list of flat nodes + + rank(data: T[], f: (t: T) => ProofNodeIdx) { + const sortErrorsFirst = (t: T) => { + const leaf = f(t); + switch (this.tree.nodeResult(leaf)) { + case "no": + return 0; + case "maybe-overflow": + case "maybe-ambiguity": + return 1; + case "yes": + return 2; + } + }; + + const sortWeightPaths = (t: T) => { + const leaf = f(t); + const pathToRoot = this.tree.pathToRoot(leaf); + const len = pathToRoot.path.length; + const numVars = _.reduce( + pathToRoot.path, + (sum, k) => sum + this.tree.inferVars(k), + 0 + ); + + return numVars / len; + }; + + const bubbleTraitClauses = (t: T) => { + const leaf = f(t); + const n = this.tree.node(leaf); + if ( + "Goal" in n && + isTraitClause(this.tree.goal(n.Goal).value.predicate) + ) { + return 0; + } + return 1; + }; + + const recommendedOrder = _.sortBy(data, [ + sortErrorsFirst, + bubbleTraitClauses, + sortWeightPaths, + ]); + + return recommendedOrder; + } + + errorLeavesInSimpleRecommendedOrder() { + return this.rank(this.tree.errorLeaves(), _.identity); + } +} diff --git a/ide/packages/panoptes/src/Workspace.tsx b/ide/packages/panoptes/src/Workspace.tsx index d36abe0..6cf7d47 100644 --- a/ide/packages/panoptes/src/Workspace.tsx +++ b/ide/packages/panoptes/src/Workspace.tsx @@ -72,7 +72,7 @@ const Workspace = ({ return ( <> -
{checkbox}
+ {/*
{checkbox}
*/} {tabs} {fileComponents} diff --git a/ide/packages/panoptes/src/utilities/context.ts b/ide/packages/panoptes/src/utilities/context.ts index 6c4ebb3..e07be3d 100644 --- a/ide/packages/panoptes/src/utilities/context.ts +++ b/ide/packages/panoptes/src/utilities/context.ts @@ -1,4 +1,4 @@ -import { SystemSpec } from "@argus/common/lib"; +import { EvaluationMode, PanoptesConfig, SystemSpec } from "@argus/common/lib"; import { createContext } from "react"; import { TreeRenderParams } from "../TreeView/Directory"; @@ -7,6 +7,9 @@ import { MessageSystem } from "../communication"; export const AppContext = { MessageSystemContext: createContext(undefined), + ConfigurationContext: createContext< + (PanoptesConfig & { evalMode: EvaluationMode }) | undefined + >(undefined), SystemSpecContext: createContext(undefined), }; diff --git a/scripts/evaluation.scm b/scripts/evaluation.scm index 3f55719..9521d14 100755 --- a/scripts/evaluation.scm +++ b/scripts/evaluation.scm @@ -54,7 +54,7 @@ (result-diagnostics result)))) `(div (@ (style "padding: 0.5em; border: 1px dashed black;")) (h2 ,fn) - (div (@ (style "max-height: 25em;overflow: hidden;")) + (div (@ (style "max-height: 25em;overflow-y: scroll;")) (img (@ (src ,(local-file screenshotfn))))) "Principal message: " (pre (code ,(string-join rustc-msgs "\n")))