2f:Tc35,chart = { const x = d3.scaleLinear().rangeRound([0, width]); const y = d3.scaleLinear().rangeRound([0, height]); const svg = d3.create("svg") .attr("viewBox", [0.5, -30.5, width, height + 30]) .style("font", "10px sans-serif"); let group = svg.append("g") .call(render, treemap(data)); function render(group, root) { const node = group .selectAll("g") .data(root.children.concat(root)) .join("g"); node.filter(d => d === root ? d.parent : d.children) .attr("cursor", "pointer") .on("click", d => d === root ? zoomout(root) : zoomin(d)); node.append("title") .text(d => `${name(d)}\n${format(d.value)}`); node.append("rect") .attr("id", d => (d.leafUid = DOM.uid("leaf")).id) .attr("fill", d => d === root ? "#fff" : d.children ? "#ccc" : "#ddd") .attr("stroke", "#fff"); node.append("clipPath") .attr("id", d => (d.clipUid = DOM.uid("clip")).id) .append("use") .attr("xlink:href", d => d.leafUid.href); node.append("text") .attr("clip-path", d => d.clipUid) .attr("font-weight", d => d === root ? "bold" : null) .selectAll("tspan") .data(d => (d === root ? name(d) : d.data.name).split(/(?=[A-Z][^A-Z])/g).concat(format(d.value))) .join("tspan") .attr("x", 3) .attr("y", (d, i, nodes) => `${(i === nodes.length - 1) * 0.3 + 1.1 + i * 0.9}em`) .attr("fill-opacity", (d, i, nodes) => i === nodes.length - 1 ? 0.7 : null) .attr("font-weight", (d, i, nodes) => i === nodes.length - 1 ? "normal" : null) .text(d => d); group.call(position, root); } function position(group, root) { group.selectAll("g") .attr("transform", d => d === root ? `translate(0,-30)` : `translate(${x(d.x0)},${y(d.y0)})`) .select("rect") .attr("width", d => d === root ? width : x(d.x1) - x(d.x0)) .attr("height", d => d === root ? 30 : y(d.y1) - y(d.y0)); } // When zooming in, draw the new nodes on top, and fade them in. function zoomin(d) { const group0 = group.attr("pointer-events", "none"); const group1 = group = svg.append("g").call(render, d); x.domain([d.x0, d.x1]); y.domain([d.y0, d.y1]); svg.transition() .duration(750) .call(t => group0.transition(t).remove() .call(position, d.parent)) .call(t => group1.transition(t) .attrTween("opacity", () => d3.interpolate(0, 1)) .call(position, d)); } // When zooming out, draw the old nodes on top, and fade them out. function zoomout(d) { const group0 = group.attr("pointer-events", "none"); const group1 = group = svg.insert("g", "*").call(render, d.parent); x.domain([d.parent.x0, d.parent.x1]); y.domain([d.parent.y0, d.parent.y1]); svg.transition() .duration(750) .call(t => group0.transition(t).remove() .attrTween("opacity", () => d3.interpolate(1, 0)) .call(position, d)) .call(t => group1.transition(t) .call(position, d.parent)); } return svg.node(); }30:[] 2d:{"title":"mathlib compile times: Zoomable Treemap","cells":[{"id":428,"value":"md`# mathlib compile times: Zoomable Treemap`","pinned":false,"hidden":false,"mode":"ojs"},{"id":435,"value":"viewof hash = viewTag`Select a profile JSON file from https://tqft.net/mathlib:\n

\n\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":0,"value":"md`This [treemap](/@d3/treemap) supports zooming: click any cell to zoom in, or the top to zoom out. Numbers are user + system times in seconds.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":10,"value":"$2f","pinned":false,"hidden":false,"mode":"ojs"},{"id":396,"value":"rawdata = (await fetch(\n `https://tqft.net/lean/mathlib/${hash.hash}.json`\n)).json()","pinned":false,"hidden":false,"mode":"ojs"},{"id":398,"value":"data = {\n const data = { name: \"mathlib\", children: [] };\n\n for (const [k, v] of Object.entries(rawdata)) {\n const path = k.split('/').slice(1);\n let place = data;\n for (const pathComponent of path) {\n // maybe skip any default.lean?\n const newPlace = place.children.find(\n ({ name }) => name === pathComponent\n );\n if (!newPlace) {\n const obj = pathComponent.endsWith('.lean')\n ? { name: pathComponent, value: v[0] + v[1] }\n : { name: pathComponent, children: [] };\n place.children.push(obj);\n place = obj;\n } else {\n place = newPlace;\n }\n }\n }\n return data;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":414,"value":"profiles = (await (await fetch(\n 'https://tqft.net/lean/mathlib/?C=M;O=D'\n)).text())\n .split('\\n')\n .map(s =>\n s.match(/ s)\n .map(s => ({ hash: s[1], date: s[2] }))","pinned":false,"hidden":false,"mode":"ojs"},{"id":58,"value":"treemap = data => d3.treemap()\n .tile(tile)\n (d3.hierarchy(data)\n .sum(d => d.value)\n .sort((a, b) => b.value - a.value))","pinned":false,"hidden":false,"mode":"ojs"},{"id":377,"value":"md`This custom tiling function adapts the built-in binary tiling function for the appropriate aspect ratio when the treemap is zoomed-in.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":361,"value":"function tile(node, x0, y0, x1, y1) {\n d3.treemapBinary(node, 0, 0, width, height);\n for (const child of node.children) {\n child.x0 = x0 + child.x0 / width * (x1 - x0);\n child.x1 = x0 + child.x1 / width * (x1 - x0);\n child.y0 = y0 + child.y0 / height * (y1 - y0);\n child.y1 = y0 + child.y1 / height * (y1 - y0);\n }\n}","pinned":true,"hidden":false,"mode":"ojs"},{"id":345,"value":"name = d => d.ancestors().reverse().map(d => d.data.name).join(\"/\")","pinned":true,"hidden":false,"mode":"ojs"},{"id":60,"value":"width = 954","pinned":true,"hidden":false,"mode":"ojs"},{"id":63,"value":"height = 924","pinned":true,"hidden":false,"mode":"ojs"},{"id":65,"value":"format = d3.format(\".2f\")","pinned":true,"hidden":false,"mode":"ojs"},{"id":7,"value":"d3 = require(\"d3@5\")","pinned":true,"hidden":false,"mode":"ojs"},{"id":433,"value":"import { viewTag } from \"2912613dea5a5003\"","pinned":true,"hidden":false,"mode":"ojs"}],"files":"$W30","stdlib":"1","titling":"auto"}