From 6e10d9d04aefe1b80ead05e4a767b67b7a5010f9 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:29:50 +0100 Subject: [PATCH] docs(formal): remove the duplicated Set Printing Width comment (9 modules) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #202 landed the same three-line explanatory comment twice in every module — once above `Set Printing Width 400.` where it belongs, and once orphaned immediately below it. My fault: I ran the insertion, then deleted only the `Set Printing Width 400.` line to A/B-test whether the ~78-column wrap was actually hiding any axiom from the guard, then re-ran the insertion. The sed that undid the test matched only the directive, not its comment, so the second pass stacked a fresh copy on top of the leftover. Comment-only; no directive, no proof and no guard changes. `formal/Justfile` is untouched. To be accurate about scope, since the obvious worry is that a text edit near the imports clipped something: it did not. `Import ListNotations.` and every `Require Import` are intact in all nine modules — verified before and after. (A *different* cleanup attempt of mine did briefly eat that import by skipping a fixed three lines past the marker, which in `Planner.v` overran the comment. That version was reset and never committed; it is mentioned only so the next person knows the offset-based approach is the wrong tool here. This commit removes the second matched block specifically, keyed on occurrence count.) Verified: real coqc 8.20.1 -> `check-assumptions` exits 0, 9/9 OK; stub coqc -> exit 127, so the gate from #202 still fails when it should; `Normalizer.out` still prints at 157 columns, so the wrap fix is unaffected; `reuse lint` compliant. --- formal/Drift.v | 3 --- formal/Normalizer.v | 3 --- formal/Octad.v | 3 --- formal/Planner.v | 3 --- formal/PlannerSemantic.v | 3 --- formal/Provenance.v | 3 --- formal/Transaction.v | 3 --- formal/VCL.v | 3 --- formal/WAL.v | 3 --- 9 files changed, 27 deletions(-) diff --git a/formal/Drift.v b/formal/Drift.v index d9730be..6d7ce59 100644 --- a/formal/Drift.v +++ b/formal/Drift.v @@ -32,9 +32,6 @@ Require Import Coq.Init.Logic. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) (** ** Domain *) diff --git a/formal/Normalizer.v b/formal/Normalizer.v index b86c7d6..0d7dadd 100644 --- a/formal/Normalizer.v +++ b/formal/Normalizer.v @@ -52,9 +52,6 @@ Require Import Coq.Bool.Bool. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) (** ** Domain *) diff --git a/formal/Octad.v b/formal/Octad.v index cf4154f..f3f13e3 100644 --- a/formal/Octad.v +++ b/formal/Octad.v @@ -95,9 +95,6 @@ Require Import Coq.Logic.FunctionalExtensionality. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** [def:modset] — Modality Set diff --git a/formal/Planner.v b/formal/Planner.v index 093eb6a..56e9072 100644 --- a/formal/Planner.v +++ b/formal/Planner.v @@ -38,9 +38,6 @@ Require Import Coq.Sorting.Permutation. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain *) diff --git a/formal/PlannerSemantic.v b/formal/PlannerSemantic.v index 81cf126..95fe4b9 100644 --- a/formal/PlannerSemantic.v +++ b/formal/PlannerSemantic.v @@ -56,9 +56,6 @@ Require Import Coq.Sorting.Permutation. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain (reusing Planner.v abstractions) *) diff --git a/formal/Provenance.v b/formal/Provenance.v index 8caaefd..7bb1bfb 100644 --- a/formal/Provenance.v +++ b/formal/Provenance.v @@ -41,9 +41,6 @@ Require Import Coq.Lists.List. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain *) diff --git a/formal/Transaction.v b/formal/Transaction.v index b100dc6..1753771 100644 --- a/formal/Transaction.v +++ b/formal/Transaction.v @@ -43,9 +43,6 @@ Require Import Coq.Init.Logic. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) (** ** Domain *) diff --git a/formal/VCL.v b/formal/VCL.v index 4530de9..86db14b 100644 --- a/formal/VCL.v +++ b/formal/VCL.v @@ -48,9 +48,6 @@ Require Import Coq.Init.Logic. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) (** ** Syntax *) diff --git a/formal/WAL.v b/formal/WAL.v index 4df1c67..ec7b890 100644 --- a/formal/WAL.v +++ b/formal/WAL.v @@ -51,9 +51,6 @@ Require Import Coq.Logic.FunctionalExtensionality. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* Keep Print Assumptions output on one line per axiom: the CI and Justfile - guards match /^name :/ with awk, and Coq's default ~78-column wrap would - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain *)