From 24de9f41a436556bd34c7ccb82f1a990f264aaae Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 28 Feb 2026 00:50:13 +0200 Subject: [PATCH 1/4] Explicitly ensure all used packages --- .config/emacs/init.el | 53 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 45 insertions(+), 8 deletions(-) diff --git a/.config/emacs/init.el b/.config/emacs/init.el index 38679d2..b457fe1 100644 --- a/.config/emacs/init.el +++ b/.config/emacs/init.el @@ -89,15 +89,19 @@ ) ) -(use-package diminish) +(use-package diminish + :ensure t + ) (use-package better-defaults :ensure (:repo "https://git.sr.ht/~technomancy/better-defaults")) (use-package treemacs-icons-dired + :ensure t :hook (dired-mode . treemacs-icons-dired-mode)) (use-package dired-subtree + :ensure t :after dired :bind (:map dired-mode-map ("" . dired-subtree-toggle) @@ -119,11 +123,14 @@ :diminish undo-tree-mode ) -(use-package transient) +(use-package transient + :ensure t + ) (use-package cond-let :ensure (:repo "https://github.com/tarsius/cond-let")) (use-package magit + :ensure t :bind (("C-x g" . magit-status) ("C-x M-g" . magit-list-repositories)) :init @@ -134,6 +141,7 @@ ("~/Projects/" . 1)))) (use-package nyan-mode + :ensure t :init (nyan-mode 1) :custom @@ -141,9 +149,11 @@ (nyan-wavy-trail t)) (use-package mozc + :ensure t :bind (("C-c m" . mozc-mode))) (use-package material-theme + :ensure t :config (load-theme 'material t)) @@ -155,6 +165,7 @@ ("s-d" . windmove-right))) (use-package counsel + :ensure t :bind (("C-s" . swiper-isearch) ("M-x" . counsel-M-x) ("M-y" . counsel-yank-pop) @@ -209,8 +220,11 @@ ;; keep-sorted end ) -(use-package org-contrib) +(use-package org-contrib + :ensure t + ) (use-package org-contacts + :ensure t :after org-contrib) (use-package deflate @@ -230,6 +244,7 @@ ) (use-package age + :ensure t :custom (age-default-identity "~/.age/key") (age-default-recipient "~/.age/key.pub") @@ -238,6 +253,7 @@ ;; EPUB reader (use-package nov + :ensure t :init (setq auto-mode-alist (map-merge 'list @@ -246,13 +262,16 @@ ) (use-package company + :ensure t :config (global-company-mode) :diminish company-mode) (use-package apt-mode + :ensure t :disabled t) (use-package docker + :ensure t :bind ("C-c d" . docker) :custom (docker-command "podman") @@ -261,10 +280,15 @@ (:name "Name" :width 50 :template "{{ json .Name }}" :sort nil :format nil) (:name "Driver" :width 10 :template "{{ json .Driver }}" :sort nil :format nil)))) -(use-package iedit) -(use-package wgrep) +(use-package iedit + :ensure t + ) +(use-package wgrep + :ensure t + ) (use-package apheleia + :ensure t :config (apheleia-global-mode) (setf (alist-get 'ruff-isort apheleia-formatters) @@ -294,10 +318,14 @@ ) ;; Note: debugging Python in a virtualenv requires debugpy to be installed inside the venv -(use-package dape) +(use-package dape + :ensure t + ) ;; Requires poetry to be installed -(use-package poetry) +(use-package poetry + :ensure t + ) (defun load-python-env () "Set up the Python IDE in the current project." @@ -308,6 +336,7 @@ (eglot-ensure)))) (use-package python + :ensure t :bind (:map python-ts-mode-map ("C-c C-p" . nil) ("C-c C-l" . nil) @@ -321,6 +350,7 @@ ;; Jupyter notebook integration (use-package ein + :ensure t :bind (("C-z j" . ein:run) :map ein:notebook-mode-map ("C-c C-x k" . ein:notebook-switch-kernel)) @@ -334,10 +364,12 @@ ) (use-package direnv + :ensure t :config (direnv-mode)) (use-package rustic + :ensure t :custom (rustic-lsp-client 'eglot) ) @@ -378,6 +410,7 @@ :models (enrich-ollama-models (list-ollama-models) gptel--local-models))) (use-package gptel + :ensure t :hook ;; keep-sorted start (gptel-mode . gptel-highlight-mode) @@ -402,9 +435,12 @@ (generate-ollama-declaration) ) -(use-package power-mode) +(use-package power-mode + :ensure t + ) (use-package emms + :ensure t :config (require 'emms-setup) (emms-all) @@ -425,4 +461,5 @@ (qrencode--encode-to-buffer url))))) (use-package qrencode + :ensure t :bind (("C-z q" . my-qr-selection))) From de599d1850c7e66bb00e020aa705f87859f5915e Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 28 Feb 2026 08:54:03 +0200 Subject: [PATCH 2/4] Add a hint argument to more steps in the spec-driven workflow --- .claude/commands/formspec.check.8.md | 1 + .claude/commands/formspec.verify.3.md | 1 + 2 files changed, 2 insertions(+) diff --git a/.claude/commands/formspec.check.8.md b/.claude/commands/formspec.check.8.md index 500277f..9060ada 100644 --- a/.claude/commands/formspec.check.8.md +++ b/.claude/commands/formspec.check.8.md @@ -1,5 +1,6 @@ --- description: Cross-artifact consistency check across all formspec artifacts +argument-hint: [scope] allowed-tools: [Read, Glob, Grep, Bash, Task] --- diff --git a/.claude/commands/formspec.verify.3.md b/.claude/commands/formspec.verify.3.md index a19354b..caeb654 100644 --- a/.claude/commands/formspec.verify.3.md +++ b/.claude/commands/formspec.verify.3.md @@ -1,5 +1,6 @@ --- description: Run the TLC model checker on the formal specification +argument-hint: [property-name] allowed-tools: [Read, Glob, Grep, Bash] --- From eeb5e6159ec491fa1889bfb04d554b52ddc9ca87 Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 28 Feb 2026 08:55:16 +0200 Subject: [PATCH 3/4] Fix instruction order in the spec-formalization step --- .claude/commands/formspec.formalize.2.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/.claude/commands/formspec.formalize.2.md b/.claude/commands/formspec.formalize.2.md index a4d20f5..a45376c 100644 --- a/.claude/commands/formspec.formalize.2.md +++ b/.claude/commands/formspec.formalize.2.md @@ -85,7 +85,10 @@ Every requirement from Phase 1 must appear in this table. If a requirement canno ## Phase 4 — Run TLC model checker -Run: +If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running locally (see `/formspec.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs, and skip to Phase 5. + +If the hook does not exist or fails, run TLC locally: + ```bash tlc spec/formal/System.tla -config spec/formal/System.cfg -workers auto -metadir /tmp/tlc-states -cleanup ``` @@ -113,11 +116,7 @@ Parse the TLC output to determine: ### All properties pass -If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running TLC locally (see `/formspec.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs. - -If the hook does not exist or fails, run TLC locally as described in Phase 4. - -In either case, update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.plan.4` to create an implementation plan. +Update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.plan.4` to create an implementation plan. ### Meaning drift detected (Phase 2 issue) From 65d8a4677cba5ed83b77b8cc02b919b364d13d3e Mon Sep 17 00:00:00 2001 From: Ohad Livne Date: Sat, 28 Feb 2026 08:55:57 +0200 Subject: [PATCH 4/4] Add human-in-the-loop interactivity to the implementation step --- .claude/commands/formspec.implement.6.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.claude/commands/formspec.implement.6.md b/.claude/commands/formspec.implement.6.md index 1bdf960..7a7ee9f 100644 --- a/.claude/commands/formspec.implement.6.md +++ b/.claude/commands/formspec.implement.6.md @@ -66,7 +66,9 @@ After unit tests pass, mark the task complete in `spec/tasks.md` (e.g., append ` **e. Continue to next task**: -After completing a task, if the next task's dependencies are all met, continue implementing it without stopping. Keep going until either: +After completing a task, present a brief summary of what was implemented and the test results. Then ask the developer whether to continue to the next task or pause for review. If the developer chooses to continue (or has previously indicated they want uninterrupted execution), proceed to the next task whose dependencies are all met. + +Stop regardless of the developer's preference when: - A unit test failure or spec inconsistency requires developer input - A verification milestone is reached (all of its tasks are now complete) - No more tasks are ready (unmet dependencies)