From edfaa2a1b9bbe13edc251d26122483c11a2cd184 Mon Sep 17 00:00:00 2001 From: chorewer <1175794600@qq.com> Date: Mon, 27 Apr 2026 16:49:32 +0800 Subject: [PATCH 1/2] feat: unify annotation system to use server-backed review API (#15) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the localStorage-based annotation system with the existing server-backed review API so comments persist in status.yaml and are visible to all users across both chapter pages and the dependency graph. - Rewrite annotations.js (~580→200 lines): fetch from GET /api/status, post via POST /api/review, scan _thmwrapper elements for indicators - Simplify annotations.css (~345→200 lines): remove edit/resolve/toolbar styles, add topic selector and feedback message styles - Fix "Complete (definition)" duplication bug in dep_graph: use .completion-label class selector instead of unreliable inline style attribute matching - Add Docker deployment: Dockerfile (multi-stage build), docker-compose, .dockerignore - Add project homepage (homepage/index.html) Closes #15 Co-Authored-By: Claude Opus 4.7 --- .dockerignore | 15 + Dockerfile | 46 ++ blueprint/src/annotations.css | 181 +---- blueprint/src/annotations.js | 621 ++++-------------- docker-compose.yml | 9 + homepage/index.html | 63 ++ .../leanblueprint/Packages/blueprint.py | 6 +- .../plastexdepgraph/templates/dep_graph.html | 5 +- 8 files changed, 298 insertions(+), 648 deletions(-) create mode 100644 .dockerignore create mode 100644 Dockerfile create mode 100644 docker-compose.yml create mode 100644 homepage/index.html diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 0000000..2586e7e --- /dev/null +++ b/.dockerignore @@ -0,0 +1,15 @@ +.git +.github +.lake +.claude +node_modules +env +__pycache__ +*.pyc +*.egg-info +ui +agents +docs +draft-hint +README.md +LICENSE diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..7c7068f --- /dev/null +++ b/Dockerfile @@ -0,0 +1,46 @@ +# Stage 1: Build blueprint web output (Alpine + TeXLive) +FROM ghcr.io/xu-cheng/texlive-full:20250401 AS builder + +RUN apk update && apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev + +WORKDIR /app + +COPY tools/ tools/ +COPY blueprint/ blueprint/ +COPY lakefile.toml lean-toolchain lake-manifest.json ./ + +RUN git init && git config --global --add safe.directory /app + +RUN python3 -m venv /env && . /env/bin/activate \ + && pip install --upgrade pip requests wheel \ + && pip install pygraphviz \ + --config-settings="--global-option=build_ext" \ + --config-settings="--global-option=-L/usr/lib/graphviz/" \ + --config-settings="--global-option=-R/usr/lib/graphviz/" \ + && pip install -e ./tools/plastexdepgraph \ + && pip install -e ./tools/leanblueprint + +RUN . /env/bin/activate && cd blueprint && leanblueprint web + +# Stage 2: Lightweight runtime (Debian) +FROM python:3.12-slim + +RUN apt-get update && apt-get install -y --no-install-recommends \ + git graphviz libgraphviz-dev gcc pkg-config libc6-dev \ + && rm -rf /var/lib/apt/lists/* + +WORKDIR /app + +COPY tools/ tools/ +COPY lakefile.toml lean-toolchain lake-manifest.json ./ +COPY --from=builder /app/blueprint blueprint/ + +RUN pip install --no-cache-dir pygraphviz \ + && pip install --no-cache-dir -e ./tools/plastexdepgraph \ + && pip install --no-cache-dir -e ./tools/leanblueprint + +RUN git init && git config --global --add safe.directory /app + +EXPOSE 8000 + +CMD ["leanblueprint", "serve"] diff --git a/blueprint/src/annotations.css b/blueprint/src/annotations.css index 9b23713..f6c4924 100644 --- a/blueprint/src/annotations.css +++ b/blueprint/src/annotations.css @@ -1,6 +1,5 @@ /* ── Annotation / Comment System ── */ -/* Indicator icon on each annotatable element */ .annotation-indicator { display: inline-flex; align-items: center; @@ -35,15 +34,6 @@ text-align: center; } -/* Paragraph-level indicator (absolutely positioned) */ -.ann-indicator-float { - position: absolute; - top: 2px; - right: -30px; - z-index: 10; -} - -/* Highlight for elements that have annotations */ .has-annotations { border-left: 3px solid #E69F00 !important; } @@ -64,7 +54,6 @@ display: block; } -/* Panel header */ .ann-panel-header { display: flex; justify-content: space-between; @@ -103,10 +92,6 @@ border: 1px solid #eee; border-radius: 3px; } -.ann-entry.resolved { - opacity: 0.55; - background: #f0f0f0; -} .ann-entry-header { display: flex; justify-content: space-between; @@ -127,30 +112,15 @@ white-space: pre-wrap; word-break: break-word; } -.ann-actions { - display: flex; - gap: 8px; - margin-top: 6px; -} -.ann-actions button { - font-size: 0.72rem; - padding: 1px 6px; - border: 1px solid #ccc; - border-radius: 2px; - background: #fff; - color: #666; - cursor: pointer; -} -.ann-actions button:hover { - background: #eee; - color: #333; -} -.ann-actions .ann-resolve-btn.is-resolved { - color: #28a745; - border-color: #28a745; + +/* Topic badge */ +.ann-topic-badge { + font-size: 0.7rem; + font-weight: 700; + text-transform: uppercase; + margin-right: 4px; } -/* Empty state */ .ann-empty { color: #999; font-style: italic; @@ -172,7 +142,7 @@ .ann-input-row label { font-size: 0.78rem; color: #666; - min-width: 40px; + min-width: 50px; } .ann-author-input { flex: 1; @@ -181,6 +151,13 @@ border-radius: 3px; font-size: 0.82rem; } +.ann-comment-topic { + flex: 1; + padding: 3px 8px; + border: 1px solid #ccc; + border-radius: 3px; + font-size: 0.82rem; +} .ann-text-input { width: 100%; min-height: 50px; @@ -205,110 +182,31 @@ .ann-submit-btn:hover { background: #cc8c00; } - -/* Edit mode */ -.ann-edit-textarea { - width: 100%; - min-height: 40px; - padding: 4px 6px; - border: 1px solid #E69F00; - border-radius: 3px; - font-size: 0.84rem; - font-family: inherit; - resize: vertical; - box-sizing: border-box; -} -.ann-edit-actions { - display: flex; - gap: 6px; - margin-top: 4px; -} -.ann-edit-actions button { - font-size: 0.75rem; - padding: 2px 10px; - border-radius: 2px; - cursor: pointer; -} -.ann-save-btn { - background: #E69F00; - color: #fff; - border: 1px solid #E69F00; -} -.ann-cancel-btn { - background: #fff; - color: #666; - border: 1px solid #ccc; +.ann-submit-btn:disabled { + background: #ccc; + cursor: not-allowed; } -/* ── Floating toolbar ── */ -#annotation-toolbar { - position: fixed; - bottom: 1.2rem; - right: 1.2rem; - z-index: 9999; - display: flex; - flex-direction: column; - align-items: flex-end; - gap: 6px; -} -#annotation-toolbar .ann-toolbar-main { - display: flex; - align-items: center; - gap: 6px; - background: #fff; - border: 1px solid #ccc; - border-radius: 6px; - padding: 6px 12px; - box-shadow: 0 2px 8px rgba(0,0,0,0.12); - font-size: 0.82rem; -} -#annotation-toolbar .ann-toolbar-badge { - background: #E69F00; - color: #fff; - font-size: 0.72rem; - font-weight: 700; - padding: 1px 6px; - border-radius: 10px; - min-width: 18px; - text-align: center; -} -#annotation-toolbar button { - padding: 4px 10px; - font-size: 0.78rem; - border: 1px solid #ccc; - border-radius: 3px; - background: #fff; - color: #555; - cursor: pointer; -} -#annotation-toolbar button:hover { - background: #f0f0f0; -} -.ann-toolbar-options { - display: flex; - align-items: center; - gap: 6px; +/* Feedback message */ +.ann-feedback { + display: none; + margin-top: 6px; font-size: 0.78rem; - color: #666; + color: #cc0000; } -.ann-toolbar-options input[type="checkbox"] { - margin: 0; +.ann-feedback:not(:empty) { + display: block; } /* ── Print styles ── */ @media print { - /* Hide interactive controls */ .annotation-indicator, - #annotation-toolbar, - .ann-actions, .ann-input-area, .ann-panel-close, - .ann-edit-actions { + .ann-feedback { display: none !important; } - - /* Show annotation panels that have comments */ - .annotation-panel.has-print-comments { + .annotation-panel.open { display: block !important; border: 1px solid #999; border-left: 3px solid #E69F00; @@ -316,29 +214,4 @@ background: #fafafa; box-shadow: none; } - - /* Show resolved comments in print */ - .ann-entry.resolved { - opacity: 1 !important; - display: block !important; - } - - /* Print label for comment section */ - .ann-print-label { - display: block; - font-weight: 700; - font-size: 0.8rem; - color: #666; - margin-bottom: 4px; - } - - /* Hide in screen */ - @media screen { - .ann-print-label { display: none; } - } -} - -/* Screen-only: hide print label */ -@media screen { - .ann-print-label { display: none; } } diff --git a/blueprint/src/annotations.js b/blueprint/src/annotations.js index 34e56b2..3a4ed0d 100644 --- a/blueprint/src/annotations.js +++ b/blueprint/src/annotations.js @@ -1,243 +1,65 @@ -/* Blueprint Annotation System — localStorage-based comments for blueprint pages */ +/* Blueprint Annotation System — server-backed comments via review API */ (function($) { 'use strict'; - var STORAGE_KEY = 'blueprint_annotations'; - var AUTHOR_KEY = 'blueprint_annotations_author'; - - var ANNOTATABLE_SELECTORS = [ - '[class$="_thmwrapper"]', - '.proof_wrapper', - '.main-text > p', - '[class$="_thmcontent"] > p' - ]; - - // ── AnnotationStore ── - - var AnnotationStore = { - _data: null, - - load: function() { - if (this._data) return this._data; - try { - var raw = localStorage.getItem(STORAGE_KEY); - this._data = raw ? JSON.parse(raw) : { version: 1, annotations: {} }; - } catch(e) { - this._data = { version: 1, annotations: {} }; - } - return this._data; - }, - - save: function() { - try { - localStorage.setItem(STORAGE_KEY, JSON.stringify(this._data)); - } catch(e) { /* quota exceeded — silent */ } - }, - - getForElement: function(elId) { - var data = this.load(); - return (data.annotations[elId] || []).slice(); - }, - - countForElement: function(elId) { - var data = this.load(); - return (data.annotations[elId] || []).length; - }, - - totalCount: function() { - var data = this.load(); - var n = 0; - for (var k in data.annotations) n += data.annotations[k].length; - return n; - }, - - addComment: function(elId, text, author) { - var data = this.load(); - if (!data.annotations[elId]) data.annotations[elId] = []; - var comment = { - id: 'ann_' + this._uuid(), - text: text, - author: author || 'Anonymous', - created: new Date().toISOString(), - modified: null, - resolved: false - }; - data.annotations[elId].push(comment); - this.save(); - return comment; - }, - - editComment: function(elId, commentId, newText) { - var list = this.load().annotations[elId] || []; - for (var i = 0; i < list.length; i++) { - if (list[i].id === commentId) { - list[i].text = newText; - list[i].modified = new Date().toISOString(); - this.save(); - return list[i]; - } - } - return null; - }, - - deleteComment: function(elId, commentId) { - var data = this.load(); - var list = data.annotations[elId] || []; - data.annotations[elId] = list.filter(function(c) { return c.id !== commentId; }); - if (data.annotations[elId].length === 0) delete data.annotations[elId]; - this.save(); - }, - - toggleResolved: function(elId, commentId) { - var list = this.load().annotations[elId] || []; - for (var i = 0; i < list.length; i++) { - if (list[i].id === commentId) { - list[i].resolved = !list[i].resolved; - this.save(); - return list[i]; - } - } - return null; - }, - - exportJSON: function() { - var data = this.load(); - var enriched = { version: data.version, annotations: {} }; - for (var elId in data.annotations) { - var $el = $('[data-annotation-id="' + elId + '"]'); - var context = _buildContext($el, elId); - enriched.annotations[elId] = { - context: context, - comments: data.annotations[elId] - }; - } - return JSON.stringify(enriched, null, 2); - }, - - importJSON: function(jsonStr) { - try { - var incoming = JSON.parse(jsonStr); - if (!incoming.annotations) return { added: 0, error: null }; - var data = this.load(); - var added = 0; - for (var elId in incoming.annotations) { - var entry = incoming.annotations[elId]; - var comments = Array.isArray(entry) ? entry : (entry.comments || []); - if (!data.annotations[elId]) data.annotations[elId] = []; - var existing = {}; - data.annotations[elId].forEach(function(c) { existing[c.id] = true; }); - comments.forEach(function(c) { - if (!existing[c.id]) { - data.annotations[elId].push(c); - added++; - } - }); - } - this.save(); - return { added: added, error: null }; - } catch(e) { - return { added: 0, error: e.message }; - } - }, - - _uuid: function() { - return 'xxxx-xxxx'.replace(/x/g, function() { - return (Math.random() * 16 | 0).toString(16); - }) + '-' + Date.now().toString(36); - } - }; - - function _buildContext($el, elId) { - var ctx = { id: elId, page: window.location.pathname.split('/').pop() || 'index.html' }; - - if (!$el.length) return ctx; - - var wrapper = $el.closest('[class$="_thmwrapper"]'); - if (wrapper.length) { - var caption = wrapper.find('[class$="_thmcaption"]').first().text().trim(); - var label = wrapper.find('[class$="_thmlabel"]').first().text().trim(); - ctx.type = caption || 'Statement'; - ctx.label = label; - ctx.title = (caption && label) ? caption + ' ' + label : (caption || label || ''); - var content = wrapper.find('[class$="_thmcontent"]').first().text().trim(); - ctx.excerpt = content.substring(0, 120).replace(/\s+/g, ' '); - if (content.length > 120) ctx.excerpt += '...'; - return ctx; - } - - if ($el.hasClass('proof_wrapper')) { - ctx.type = 'Proof'; - var prev = $el.prev('[class$="_thmwrapper"]'); - if (prev.length) { - var pc = prev.find('[class$="_thmcaption"]').first().text().trim(); - var pl = prev.find('[class$="_thmlabel"]').first().text().trim(); - ctx.title = 'Proof of ' + ((pc && pl) ? pc + ' ' + pl : (pc || pl || '')); - } - return ctx; - } - - ctx.type = 'Paragraph'; - var text = $el.text().trim(); - ctx.excerpt = text.substring(0, 120).replace(/\s+/g, ' '); - if (text.length > 120) ctx.excerpt += '...'; - - var section = $el.closest('[id^="sec:"]'); - if (section.length) { - ctx.section = section.find('h1,h2,h3,h4').first().text().trim() || section.attr('id'); - } - return ctx; - } - - // ── Stable ID assignment ── - - function getPageName() { - var path = window.location.pathname; - var parts = path.split('/'); - var file = parts[parts.length - 1] || 'index'; - return file.replace(/\.html$/, ''); + var REVIEWER_KEY = 'leanblueprint_reviewer_name'; + var TOPIC_COLORS = { review: '#E69F00', align: '#009E73', general: '#666' }; + + var _statusCache = null; + var _apiAvailable = false; + + function getReviewer() { return localStorage.getItem(REVIEWER_KEY) || ''; } + function setReviewer(name) { localStorage.setItem(REVIEWER_KEY, name); } + + function fetchStatus() { + return fetch('/api/status') + .then(function(r) { if (!r.ok) throw new Error(r.status); return r.json(); }) + .then(function(data) { + _statusCache = data.nodes || {}; + _apiAvailable = true; + return _statusCache; + }) + .catch(function() { + _statusCache = {}; + _apiAvailable = false; + return _statusCache; + }); } - function findNearestIdAncestor(el) { - var node = el.parentElement; - while (node) { - if (node.id) return node.id; - node = node.parentElement; - } - return 'root'; + function postComment(nodeId, text, topic, reviewer) { + return fetch('/api/review', { + method: 'POST', + headers: { 'Content-Type': 'application/json' }, + body: JSON.stringify({ + node_id: nodeId, + action: 'comment', + text: text, + topic: topic || 'general', + reviewer: reviewer || 'Anonymous' + }) + }).then(function(r) { return r.json(); }); } - function assignAnnotationIds() { - var page = getPageName(); - $(ANNOTATABLE_SELECTORS.join(',')).each(function() { - var el = this; - if (el.id) { - el.setAttribute('data-annotation-id', el.id); - } else { - var ancestor = findNearestIdAncestor(el); - var siblings = $(el).parent().children(el.tagName); - var idx = siblings.index(el); - var genId = page + '--' + ancestor + '--p' + idx; - el.setAttribute('data-annotation-id', genId); - } - }); + function getNodeComments(nodeId) { + if (!_statusCache || !_statusCache[nodeId]) return []; + return _statusCache[nodeId].comments || []; } - // ── Author helpers ── - - function getAuthor() { - return localStorage.getItem(AUTHOR_KEY) || ''; + function escHtml(str) { + var div = document.createElement('div'); + div.appendChild(document.createTextNode(str)); + return div.innerHTML; } - function setAuthor(name) { - localStorage.setItem(AUTHOR_KEY, name); + function formatDate(dateStr) { + if (!dateStr) return ''; + if (/^\d{4}-\d{2}-\d{2}$/.test(dateStr)) return dateStr; + var d = new Date(dateStr); + return isNaN(d) ? dateStr : d.toLocaleDateString(); } - // ── UI rendering ── - - var showResolved = false; - - function createIndicator(annId, count) { - var $ind = $('' + + function createIndicator(nodeId, count) { + var $ind = $('' + '✍' + '' + (count || '') + '' + ''); @@ -245,135 +67,89 @@ return $ind; } - function formatTime(iso) { - if (!iso) return ''; - var d = new Date(iso); - return d.toLocaleDateString() + ' ' + d.toLocaleTimeString([], {hour:'2-digit', minute:'2-digit'}); - } - - function renderPanel(annId) { - var comments = AnnotationStore.getForElement(annId); + function renderPanel(nodeId) { + var comments = getNodeComments(nodeId); + var $panel = $('
'); - var $panel = $('
'); - - // Header var $header = $('
' + 'Comments' + '' + '
'); $panel.append($header); - // Print label (visible only in print) - $panel.append('
Comments:
'); - - // Comments list var $list = $('
'); if (comments.length === 0) { $list.append('
No comments yet.
'); } else { - var hasVisiblePrint = false; - comments.forEach(function(c) { - if (c.resolved && !showResolved) { - hasVisiblePrint = true; // still exists for print - var $entry = renderEntry(annId, c); - $entry.css('display', 'none').addClass('ann-hidden-resolved'); - $list.append($entry); - return; - } - hasVisiblePrint = true; - $list.append(renderEntry(annId, c)); - }); - if (hasVisiblePrint) $panel.addClass('has-print-comments'); + comments.forEach(function(c) { $list.append(renderEntry(c)); }); } $panel.append($list); - // Input area + var topicOpts = '' + + '' + + ''; + + var disabledAttr = _apiAvailable ? '' : ' disabled'; var $input = $('
' + '
' + - '' + - '' + + '' + + '' + + '
' + + '
' + + '' + + '' + '
' + '' + '
' + - '' + + '' + '
' + + '
' + '
'); $panel.append($input); + if (!_apiAvailable) { + $panel.find('.ann-feedback').text('Server unavailable — comments are read-only.').show(); + } + return $panel; } - function renderEntry(annId, c) { - var $entry = $('
'); - if (c.resolved) $entry.addClass('resolved'); - - var timeStr = formatTime(c.modified || c.created); + function renderEntry(c) { + var topicColor = TOPIC_COLORS[c.topic] || TOPIC_COLORS.general; + var $entry = $('
'); $entry.append('
' + - '' + escHtml(c.author) + '' + - '' + timeStr + '' + + '' + + '' + escHtml(c.topic || 'general') + ' ' + + escHtml(c.by || 'Anonymous') + + '' + + '' + formatDate(c.at) + '' + '
'); - $entry.append('
' + escHtml(c.text) + '
'); - - var $actions = $('
'); - var resLabel = c.resolved ? 'Unresolve' : 'Resolve'; - var resCls = c.resolved ? ' is-resolved' : ''; - $actions.append(''); - $actions.append(''); - $actions.append(''); - $entry.append($actions); - + $entry.append('
' + escHtml(c.text || '') + '
'); return $entry; } - function refreshPanel(annId) { - var $old = $('[data-panel-for="' + annId + '"]'); + function refreshPanel(nodeId) { + var $old = $('[data-panel-for="' + nodeId + '"]'); if ($old.length && $old.hasClass('open')) { - var $new = renderPanel(annId); + var $new = renderPanel(nodeId); $old.replaceWith($new); } - refreshIndicator(annId); - refreshToolbar(); + refreshIndicator(nodeId); } - function refreshIndicator(annId) { - var count = AnnotationStore.countForElement(annId); - var $ind = $('[data-for="' + annId + '"]'); + function refreshIndicator(nodeId) { + var count = getNodeComments(nodeId).length; + var $ind = $('[data-for="' + nodeId + '"]'); $ind.find('.ann-count').text(count || ''); $ind.toggleClass('has-comments', count > 0); - // highlight the element - $('[data-annotation-id="' + annId + '"]').toggleClass('has-annotations', count > 0); - } - - function refreshToolbar() { - var total = AnnotationStore.totalCount(); - $('#annotation-toolbar .ann-toolbar-badge').text(total); - } - - // ── Toolbar ── - - function createToolbar() { - var total = AnnotationStore.totalCount(); - var $tb = $('
' + - '
' + - '' + total + ' annotations ' + - '' + - '' + - '
' + - '
' + - '' + - '
' + - '
'); - $('body').append($tb); + $('[id="' + nodeId + '"]').toggleClass('has-annotations', count > 0); } - // ── Event handlers ── - function bindEvents() { - // Toggle panel $(document).on('click', '.annotation-indicator', function(e) { e.stopPropagation(); - var annId = $(this).data('for'); - var $existing = $('[data-panel-for="' + annId + '"]'); + var nodeId = $(this).data('for'); + var $existing = $('[data-panel-for="' + nodeId + '"]'); if ($existing.length) { if ($existing.hasClass('open')) { $existing.removeClass('open').slideUp(150); @@ -382,201 +158,66 @@ } return; } - // Create new panel - var $panel = renderPanel(annId); - var $el = $('[data-annotation-id="' + annId + '"]'); - $el.after($panel); - $panel.hide().slideDown(200); + var $panel = renderPanel(nodeId); + var $el = $('[id="' + nodeId + '"]').filter('[class*="_thmwrapper"]'); + if ($el.length) { + $el.after($panel); + $panel.hide().slideDown(200); + } }); - // Close panel $(document).on('click', '.ann-panel-close', function() { $(this).closest('.annotation-panel').removeClass('open').slideUp(150); }); - // Submit comment $(document).on('click', '.ann-submit-btn', function() { - var $panel = $(this).closest('.annotation-panel'); - var annId = $panel.data('panel-for'); + var $btn = $(this); + var $panel = $btn.closest('.annotation-panel'); + var nodeId = $panel.data('panel-for'); var text = $panel.find('.ann-text-input').val().trim(); - var author = $panel.find('.ann-author-input').val().trim() || 'Anonymous'; + var topic = $panel.find('.ann-comment-topic').val(); + var reviewer = $panel.find('.ann-author-input').val().trim() || 'Anonymous'; if (!text) return; - setAuthor(author); - AnnotationStore.addComment(annId, text, author); - refreshPanel(annId); - }); - - // Resolve toggle - $(document).on('click', '.ann-resolve-btn', function() { - var annId = $(this).data('el'); - var cid = $(this).data('cid'); - AnnotationStore.toggleResolved(annId, cid); - refreshPanel(annId); - }); - - // Edit - $(document).on('click', '.ann-edit-btn', function() { - var $entry = $(this).closest('.ann-entry'); - var annId = $(this).data('el'); - var cid = $(this).data('cid'); - var currentText = $entry.find('.ann-text').text(); - $entry.find('.ann-text').replaceWith( - '' + - '
' + - '' + - '' + - '
' - ); - $entry.find('.ann-actions').hide(); - }); - - // Save edit - $(document).on('click', '.ann-save-btn', function() { - var annId = $(this).data('el'); - var cid = $(this).data('cid'); - var newText = $(this).closest('.ann-entry').find('.ann-edit-textarea').val().trim(); - if (newText) AnnotationStore.editComment(annId, cid, newText); - refreshPanel(annId); - }); - - // Cancel edit - $(document).on('click', '.ann-cancel-btn', function() { - var annId = $(this).data('el'); - refreshPanel(annId); - }); - - // Delete - $(document).on('click', '.ann-delete-btn', function() { - if (!confirm('Delete this comment?')) return; - var annId = $(this).data('el'); - var cid = $(this).data('cid'); - AnnotationStore.deleteComment(annId, cid); - refreshPanel(annId); - }); - // Show resolved toggle - $(document).on('change', '.ann-show-resolved-chk', function() { - showResolved = $(this).is(':checked'); - // Re-render all open panels - $('.annotation-panel.open').each(function() { - var annId = $(this).data('panel-for'); - refreshPanel(annId); - }); - // Restore checkbox state - $('.ann-show-resolved-chk').prop('checked', showResolved); - }); - - // Export - $(document).on('click', '.ann-export-btn', function() { - var json = AnnotationStore.exportJSON(); - var blob = new Blob([json], { type: 'application/json' }); - var url = URL.createObjectURL(blob); - var a = document.createElement('a'); - var date = new Date().toISOString().slice(0,10); - a.href = url; - a.download = 'blueprint-annotations-' + date + '.json'; - document.body.appendChild(a); - a.click(); - document.body.removeChild(a); - URL.revokeObjectURL(url); - }); + $btn.prop('disabled', true).text('Sending...'); + setReviewer(reviewer); - // Import - $(document).on('click', '.ann-import-btn', function() { - var input = document.createElement('input'); - input.type = 'file'; - input.accept = '.json'; - input.onchange = function(e) { - var file = e.target.files[0]; - if (!file) return; - var reader = new FileReader(); - reader.onload = function(ev) { - var result = AnnotationStore.importJSON(ev.target.result); - if (result.error) { - alert('Import failed: ' + result.error); - } else { - alert('Imported ' + result.added + ' new comment(s).'); - // Refresh all indicators - $('[data-annotation-id]').each(function() { - refreshIndicator($(this).data('annotation-id')); - }); - refreshToolbar(); + postComment(nodeId, text, topic, reviewer) + .then(function(resp) { + if (resp.error) { + $panel.find('.ann-feedback').text('Error: ' + resp.error).show(); + $btn.prop('disabled', false).text('Send'); + return; } - }; - reader.readAsText(file); - }; - input.click(); + if (_statusCache[nodeId]) { + _statusCache[nodeId].comments = resp.comments || []; + } + refreshPanel(nodeId); + }) + .catch(function(err) { + $panel.find('.ann-feedback').text('Network error — is the server running?').show(); + $btn.prop('disabled', false).text('Send'); + }); }); } - // ── Print preparation ── - - function preparePrint() { - // Before printing, inject panels for elements with comments so they appear in print - window.addEventListener('beforeprint', function() { - $('[data-annotation-id]').each(function() { - var annId = $(this).data('annotation-id'); - var count = AnnotationStore.countForElement(annId); - if (count === 0) return; - var $existing = $('[data-panel-for="' + annId + '"]'); - if ($existing.length === 0) { - var $panel = renderPanel(annId); - $panel.removeClass('open').addClass('has-print-comments'); - $(this).after($panel); - } else { - $existing.addClass('has-print-comments'); + function init() { + fetchStatus().then(function() { + $('[class*="_thmwrapper"]').each(function() { + var nodeId = this.id; + if (!nodeId || !_statusCache[nodeId]) return; + + var count = getNodeComments(nodeId).length; + var $ind = createIndicator(nodeId, count); + var $extras = $(this).find('> [class$="_thmheading"] .thm_header_extras').first(); + if ($extras.length) { + $extras.append($ind); } + if (count > 0) $(this).addClass('has-annotations'); }); + bindEvents(); }); } - // ── Helpers ── - - function escHtml(str) { - var div = document.createElement('div'); - div.appendChild(document.createTextNode(str)); - return div.innerHTML; - } - - // ── Init ── - - function init() { - assignAnnotationIds(); - - // Insert indicators - $('[data-annotation-id]').each(function() { - var $el = $(this); - var annId = $el.data('annotation-id'); - var count = AnnotationStore.countForElement(annId); - var $ind = createIndicator(annId, count); - - // For theorem-like wrappers: put in thm_header_extras - var $extras = $el.find('> [class$="_thmheading"] .thm_header_extras').first(); - if ($extras.length) { - $extras.append($ind); - } - // For proof wrappers: put in proof_heading - else if ($el.hasClass('proof_wrapper')) { - $el.find('> .proof_heading').first().append($ind); - } - // For paragraphs: float to the right - else if ($el.is('p')) { - $el.css('position', 'relative'); - $ind.addClass('ann-indicator-float'); - $el.append($ind); - } - - if (count > 0) $el.addClass('has-annotations'); - }); - - createToolbar(); - bindEvents(); - preparePrint(); - } - - // Run on DOM ready - $(document).ready(function() { - init(); - }); - + $(document).ready(init); })(jQuery); diff --git a/docker-compose.yml b/docker-compose.yml new file mode 100644 index 0000000..898941f --- /dev/null +++ b/docker-compose.yml @@ -0,0 +1,9 @@ +services: + server: + build: . + container_name: kip-server + ports: + - "8082:8000" + volumes: + - ./blueprint/status.yaml:/app/blueprint/status.yaml + restart: unless-stopped diff --git a/homepage/index.html b/homepage/index.html new file mode 100644 index 0000000..476c311 --- /dev/null +++ b/homepage/index.html @@ -0,0 +1,63 @@ + + + + + + On the Last Kervaire Invariant Problem + + + +

On the Last Kervaire Invariant Problem

+

by Weinan Lin, Guozhen Wang, and Zhouli Xu

+

+ This is a Lean 4 formalization project for the paper On the Last Kervaire Invariant Problem, + which proves that framed manifolds of Kervaire invariant one exist in dimension 126. +

+
    +
  • + Blueprint +
    Interactive blueprint with dependency graph and review system
    +
    • +
  • + Blueprint as PDF +
    Downloadable PDF version of the blueprint
    +
    • +
  • + Lean API Docs +
    Auto-generated documentation for the Lean formalization
    +
    • +
  • + Source Code +
    GitHub repository
    +
    • +
+ + diff --git a/tools/leanblueprint/leanblueprint/Packages/blueprint.py b/tools/leanblueprint/leanblueprint/Packages/blueprint.py index e7e49b9..0986b9e 100644 --- a/tools/leanblueprint/leanblueprint/Packages/blueprint.py +++ b/tools/leanblueprint/leanblueprint/Packages/blueprint.py @@ -342,11 +342,11 @@ def digest(self, tokens): {%- endif -%} {%- if st.get('kind') == 'definition' and st.get('aligned') -%} - Complete (definition) + Complete (definition) {%- elif st.get('kind') == 'axiom' and st.get('aligned') -%} - Complete (axiom — no proof needed) + Complete (axiom — no proof needed) {%- elif st.get('kind') not in ('definition', 'axiom') and st.get('proved') -%} - Complete (proved) + Complete (proved) {%- endif -%}
diff --git a/tools/plastexdepgraph/plastexdepgraph/templates/dep_graph.html b/tools/plastexdepgraph/plastexdepgraph/templates/dep_graph.html index 5aba542..a1be0b4 100644 --- a/tools/plastexdepgraph/plastexdepgraph/templates/dep_graph.html +++ b/tools/plastexdepgraph/plastexdepgraph/templates/dep_graph.html @@ -308,7 +308,7 @@

{{ title }}

} }); // Update completion labels - var completionSpans = panel.querySelectorAll('span[style*="font-weight:bold"]'); + var completionSpans = panel.querySelectorAll('.completion-label'); completionSpans.forEach(function(s) { s.remove(); }); var btnRow = panel.querySelector('div'); if (btnRow) { @@ -316,16 +316,19 @@

{{ title }}

var state = nodeState(st); if (kind === 'definition' && st.aligned) { var s = document.createElement('span'); + s.className = 'completion-label'; s.style.cssText = 'color:#009E73;font-size:0.8em;font-weight:bold;'; s.textContent = 'Complete (definition)'; btnRow.appendChild(s); } else if (kind === 'axiom' && st.aligned) { var s = document.createElement('span'); + s.className = 'completion-label'; s.style.cssText = 'color:#CC79A7;font-size:0.8em;font-weight:bold;'; s.textContent = 'Complete (axiom \u2014 no proof needed)'; btnRow.appendChild(s); } else if (isThmKind(kind) && st.proved) { var s = document.createElement('span'); + s.className = 'completion-label'; s.style.cssText = 'color:#1CAC78;font-size:0.8em;font-weight:bold;'; s.textContent = 'Complete (proved)'; btnRow.appendChild(s); From a5fb6c654511a266ec4735047b3dc59fa616238b Mon Sep 17 00:00:00 2001 From: chorewer <1175794600@qq.com> Date: Mon, 27 Apr 2026 17:00:39 +0800 Subject: [PATCH 2/2] chore: include status.yaml with review comments data Co-Authored-By: Claude Opus 4.7 --- blueprint/status.yaml | 61 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 48 insertions(+), 13 deletions(-) diff --git a/blueprint/status.yaml b/blueprint/status.yaml index 31fdf2b..547baca 100644 --- a/blueprint/status.yaml +++ b/blueprint/status.yaml @@ -7,18 +7,18 @@ nodes: proved: false kind: definition comments: - - topic: align - text: SSData字段顺序和NL不一致，建议p q互换 - by: surenny - at: '2026-04-19' - - topic: general - text: 这个定义是整个谱序列的基础 - by: wangguozhen - at: '2026-04-19' - - topic: general - text: 这是一个非常正确的形式化 - by: web-reviewer - at: '2026-04-19' + - topic: align + text: SSData字段顺序和NL不一致，建议p q互换 + by: surenny + at: '2026-04-19' + - topic: general + text: 这个定义是整个谱序列的基础 + by: wangguozhen + at: '2026-04-19' + - topic: general + text: 这是一个非常正确的形式化 + by: web-reviewer + at: '2026-04-19' nl_reviewer: test align_reviewer: web-reviewer nl_hash: 192c2f3b92f48706 @@ -117,6 +117,39 @@ nodes: kind: definition nl_hash: ac0cf089df4b4690 aligned_by: surenny + comments: + - topic: general + text: test + by: wangpan + at: '2026-04-27' + - topic: general + text: 这是一个测试评论存储功能的信息 + by: surenny + at: '2026-04-27' + - topic: general + text: test2 + by: surenny + at: '2026-04-27' + - topic: general + text: hi + by: wangpan + at: '2026-04-27' + - topic: general + text: hi + by: wangpan + at: '2026-04-27' + - topic: general + text: hi + by: wangpan + at: '2026-04-27' + - topic: general + text: hi + by: wangpan + at: '2026-04-27' + - topic: general + text: '111' + by: wangpan + at: '2026-04-27' prereq:def:filtered-morphism: lean_decl: KIP.SpectralSequence.FilteredMorphism nl_reviewed: true @@ -538,10 +571,12 @@ nodes: lean_decl: KIP.StableHomotopy.InAdamsFiltration nl_reviewed: true bound: true - aligned: false + aligned: true proved: false kind: definition nl_hash: 49238adaaf6a20fa + align_reviewer: web-reviewer + aligned_at: '2026-04-27' prereq:def:adams-filtration-maps: lean_decl: KIP.StableHomotopy.AF nl_reviewed: true