Tooling and more day 1 cleanup

Author: eutro

.dir-locals.el

@@ -0,0 +1,8 @@
+((lean4-mode
+  (eval . (unless (featurep 'aoc2025-eutro)
+            (let ((load-path (cons (locate-dominating-file
+                                    (or load-file-name (buffer-file-name))
+                                    "aoc2025-eutro.el")
+                                   load-path)))
+              (require 'aoc2025-eutro))))
+  (eval . (aoc2025-eutro-mode))))

Aoc2025.lean

@@ -1 +0,0 @@
-import Aoc2025.Basic

Aoc2025/Basic.lean

@@ -1,24 +1,41 @@
-def dialInit : Int := 50
-def dialSize : Int := 100
+abbrev Dial := Int
+def dialSize : Nat := 100
+def dialInit : Dial := 50
 
-abbrev DialState α := StateM Int α
+abbrev DialState α := StateM Dial α
 
 -- Rotate the dial by the given command.
 def stepDial (command : Int) : DialState Unit := do
   let dial <- get
   set $ (dial + command) % dialSize
 
+theorem step_dial_homomorphism 
+  : ∀ c0 c1, stepDial (c0 + c1) = (do stepDial c0; stepDial c1) := by
+  intros
+  apply StateT.ext
+  intros
+  simp [stepDial]
+  grind
+
 -- Rotate the dial at once, only counting 0 at the end.
 def stepAtomic (command : Int) : DialState Int := do
   stepDial command
   let dial' <- get
   return if dial' = 0 then 1 else 0
 
 -- Rotate the dial one step at a time, counting every 0.
-def stepIncremental (command : Int) : DialState Int :=
-  0 |> command.natAbs.foldM fun _ _ a ↦ do
-    let a' <- stepAtomic command.sign
-    return a + a'
+def stepIncrementalSlow (command : Int) : DialState Int := do
+  let substates <- (List.replicate command.natAbs command.sign).mapM stepAtomic
+  return substates.sum
+
+def stepIncremental (command : Int) : DialState Int := do
+  let dial <- get
+  stepDial command
+  let rawDial' := dial + command
+  let mut fullRotations := rawDial'.natAbs / dialSize
+  if rawDial' <= 0 ∧ dial % dialSize != 0 then
+    fullRotations := fullRotations + 1
+  return fullRotations
 
 -- Run the stepping function over the commands.
 def runPart (step : Int -> DialState Int) (commands : Array Int) : Int :=

Aoc2025/Day01.lean

@@ -0,0 +1,115 @@
+;;; aoc2025-eutro.el --- Advent of Code utilities -*- lexical-binding: t -*-
+
+;;; Code:
+
+(defgroup aoc2025-eutro nil
+  "Group for Eutro's Advent of Code 2025"
+  :prefix 'aoc2025-eutro-
+  :group 'misc)
+
+(defconst aoc-root
+  (locate-dominating-file
+   (or load-file-name (buffer-file-name))
+   "README.md"))
+
+(defconst aoc-dayfile-pattern "Day\\([0-9]\\{2\\}\\)")
+
+(defvar-local aoc-pinned-day-number nil)
+
+(defun aoc-day-number ()
+  "Determine the day number of the current file, or the current day."
+  (or
+   aoc-pinned-day-number
+   (when-let ((file-name (buffer-file-name)))
+     (and (string-match aoc-dayfile-pattern file-name)
+          (string-to-number (match-string 1 file-name))))
+   (progn
+     (require 'calendar)
+     (cadr (calendar-current-date)))))
+
+(defun aoc-get-out-buffer (&optional clear day)
+  "Get the *aoc-output* buffer."
+  (let ((buf (get-buffer-create "*aoc-output*")))
+    (when (or clear
+              (not (eq 'aoc-run-mode
+                       (buffer-local-value 'major-mode buf))))
+      (with-current-buffer buf
+        (erase-buffer)
+        (when day (setq aoc-pinned-day-number day))
+        (aoc-run-mode)))
+    buf))
+
+(defconst aoc--run-script (expand-file-name "run.sh" aoc-root))
+
+(defconst aoc--display-buffer-action nil
+  ;;'display-buffer-use-least-recent-window
+  )
+
+(defun aoc-run (&optional prefix)
+  "Run the current day.
+
+With PREFIX, read input from the buffer."
+  (interactive "P")
+  (let* ((day (aoc-day-number))
+         (inp-args (when prefix '("--")))
+         (buf (aoc-get-out-buffer t day))
+         (args (cons (number-to-string day) inp-args))
+         (proc (apply #'start-process "aoc-run" buf aoc--run-script args))
+         (win (selected-window)))
+    (set-process-sentinel
+     proc
+     (lambda (_proc msg)
+       (when-let ((win (get-buffer-window buf)))
+         (with-selected-window win 
+           (recenter -1)))))
+    (unless (eq (window-buffer win) buf)
+      (if prefix
+          (pop-to-buffer buf aoc--display-buffer-action)
+        (display-buffer buf aoc--display-buffer-action)))
+    (message "./run.sh %s" (string-join (mapcar #'shell-quote-argument args) " "))))
+
+(defun aoc-copy-part-answer (part)
+  "Copy the answer for the given PART from *aoc-output*."
+  (with-current-buffer (aoc-get-out-buffer)
+    (goto-char (point-max))
+    (unless (re-search-backward (format "Part %d: " part) nil t)
+      (user-error "Part %d not found in buffer" part))
+    (goto-char (match-end 0))
+    (let ((start (point)))
+      (end-of-line)
+      (copy-region-as-kill start (point))
+      (message "Copied: %s" (current-kill 0 t)))))
+
+(defmacro aoc-copy-n (part)
+  `(defun ,(intern (format "aoc-copy-%d" part)) ()
+     ,(format "Copy the answer for part %d in *aoc-output*." part)
+     (interactive)
+     (aoc-copy-part-answer ,part)))
+
+(aoc-copy-n 1)
+(aoc-copy-n 2)
+
+(defconst aoc-mode-map
+  (let ((keys (make-sparse-keymap)))
+    (define-key keys (kbd "C-c C-c") #'aoc-run)
+    (define-key keys (kbd "C-c 1") #'aoc-copy-1)
+    (define-key keys (kbd "C-c 2") #'aoc-copy-2)
+    keys))
+
+(define-minor-mode aoc-mode
+  "Minor mode for Advent of Code utilities"
+  :lighter " AoC24")
+
+(defconst aoc-run-mode-map
+  (let ((keys (copy-keymap aoc-mode-map)))
+    keys))
+
+(define-derived-mode aoc-run-mode comint-mode "AoC-Run"
+  "Major mode for the *aoc-run* buffer.")
+
+;; Local Variables:
+;; read-symbol-shorthands: (("aoc-" . "aoc2025-eutro-"))
+;; End:
+
+(provide 'aoc2025-eutro)
+;;; aoc2025-eutro.el ends here

aoc2025-eutro.el

@@ -0,0 +1,13 @@
+#!/usr/bin/env sh
+
+DIR="$(readlink -f "$(dirname "$0")")"
+cd "$DIR" || exit 1
+
+case "$1" in
+  ''|*[!0-9]*) DAYN="$(date +%d)" ;;
+  *) DAYN="$1"; shift ;;
+esac
+DAY="$(echo "$DAYN" | sed 's/^0*//')"
+DAYP="$(printf "%02d" "$DAY")"
+
+lake build --no-ansi "Day$DAYP:exe" "$@"

build.sh

@@ -16,3 +16,7 @@ scope = "leanprover-community"
 
 [[lean_lib]]
 name = "Aoc2025"
+
+[[lean_exe]]
+name = "Day01"
+root = "Aoc2025.Day01"

lakefile.toml

@@ -0,0 +1,28 @@
+#!/usr/bin/env sh
+
+DIR="$(readlink -f "$(dirname "$0")")"
+cd "$DIR" || exit 1
+
+case "$1" in
+  ''|*[!0-9]*) DAYN="$(date +%d)" ;;
+  *) DAYN="$1"; shift ;;
+esac
+DAY="$(echo "$DAYN" | sed 's/^0*//')"
+DAYP="$(printf "%02d" "$DAY")"
+
+export AOC_INPUT
+if [ "$1" = "--" ]
+then AOC_INPUT="/dev/stdin"; shift
+elif [ "$1" = "-e"  -o "$1" = "--example" ]
+then AOC_INPUT="$DIR/inputs/example$DAYP.txt"; shift
+elif [ "$1" = "-i" -o "$1" = "--input" ]
+then AOC_INPUT="$2"; shift; shift
+else
+    AOC_INPUT="$DIR/inputs/day$DAYP.txt"
+    if ! [ -f "$AOC_INPUT" ]
+    then raco aoc -y 2025 -d "$DAY" > "$AOC_INPUT" || exit 1
+    fi
+fi
+
+./build.sh "$DAY"
+time ".lake/build/bin/Day$DAYP" "$@" < "$AOC_INPUT"