herd · Roman-Manevich · Mar 30, 2026 · Mar 30, 2026 · Mar 25, 2026 · Mar 25, 2026
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -42,7 +42,10 @@ repos:
             )|
 
             # Expected files should be left verbatim.
-            \.expected(-failure)?$
+            \.expected(-failure)?$|
+
+            # Cram tests may include trailing whitespace.
+            (^|/)run\.t$
           )
 - repo: https://github.com/arenadotio/pre-commit-ocamlformat
   rev: 0439858f79b3bcb49e757278eb1312e212d7dd4f

diff --git a/asllib/aslspec/builtins.spec b/asllib/aslspec/builtins.spec
@@ -16,11 +16,8 @@ variadic operator cond_op[T](cases: list1(T)) -> T
   prose_application = "\begin{itemize}{cases}\end{itemize}",
 };
 
-// This constant is for internal use only.
-constant bot { "bottom", math_macro = \bot };
-
-constant None {
-  "the  \hyperlink{constant-None}{empty} \optionalterm{}"
+constant none {
+  "the  \hyperlink{constant-none}{empty} \optionalterm{}"
 };
 
 constant empty_set

diff --git a/asllib/aslspec/spec.ml b/asllib/aslspec/spec.ml
@@ -3486,9 +3486,9 @@ let make_spec_with_builtins ast =
   {
     ast;
     id_to_defining_node;
-    bottom_constant = get_builtin_constant "bot";
+    bottom_constant = Constant.make missing_location "bot" None None [];
     bottom_term = Label { loc = missing_location; label = "bot" };
-    none_constant = get_builtin_constant "None";
+    none_constant = get_builtin_constant "none";
     empty_set = get_builtin_constant "empty_set";
     empty_list = get_builtin_constant "empty_list";
     bool = get_builtin_type "Bool";
@@ -3502,6 +3502,19 @@ let make_spec_with_builtins ast =
     field_to_containing_variant = make_field_to_containing_variant ast;
   }
 
+(** [remove_bottom_constant spec] removes the bottom constant from [spec], since
+    it is only used for typechecking and should not be rendered. *)
+let remove_bottom_constant spec =
+  let ast =
+    List.filter
+      (function
+        | Elem_Constant { Constant.name; _ } when String.equal name "bot" ->
+            false
+        | _ -> true)
+      spec.ast
+  in
+  { spec with ast }
+
 let from_ast ast =
   let spec = make_spec_with_builtins ast in
   let () = Check.check_no_undefined_ids spec in
@@ -3516,4 +3529,5 @@ let from_ast ast =
   let spec = ExtendNames.extend spec in
   let () = Check.CheckRules.check spec in
   let spec = add_default_rule_renders spec in
+  let spec = remove_bottom_constant spec in
   spec
diff --git a/asllib/aslspec/tests.t/hello.expected b/asllib/aslspec/tests.t/hello.expected
@@ -16,8 +16,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant

diff --git a/asllib/aslspec/tests.t/operators.expected b/asllib/aslspec/tests.t/operators.expected
@@ -15,8 +15,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
@@ -52,8 +50,8 @@ The relation
 \DefineProse{f}{
 \AllApply
   \begin{itemize}
-    \item the sum of all numbers in  (1) \texttt{a}, and  (2) \texttt{b} is equal to \texttt{c};
-    \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c};
+    \item the sum of \texttt{a} and \texttt{b} is equal to \texttt{c}
+    \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c}
     \item \textbf{the result is:} \texttt{d}.
   \end{itemize}
 } % EndDefineProse
diff --git a/asllib/aslspec/tests.t/relations.expected b/asllib/aslspec/tests.t/relations.expected
@@ -23,8 +23,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant

diff --git a/asllib/aslspec/tests.t/rule.expected b/asllib/aslspec/tests.t/rule.expected
@@ -17,8 +17,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
@@ -79,10 +77,10 @@ The relation
 \DefineProse{r}{
 \AllApply
   \begin{itemize}
-    \item define \texttt{res} as  (1) if \texttt{a} is equal to \texttt{b} holds then \texttt{a},  (2) if \texttt{a} is greater than \texttt{b} holds then the sum of  (1) \texttt{a}, and  (2) \texttt{b}, and  (3) if \texttt{a} is less than \texttt{b} holds then \texttt{b};
-    \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b};
-    \item define \texttt{r\_f} as the sum of  (1) the field $\FIELDf$ of \texttt{r}, and  (2) the field $\FIELDg$ of \texttt{r};
-    \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res};
-    \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'}.
+    \item define \texttt{res} as \begin{itemize}\item \texttt{a} if \texttt{a} is equal to \texttt{b}, \item the sum of \texttt{a} and \texttt{b} if \texttt{a} is greater than \texttt{b}, and \item \texttt{b} if \texttt{a} is less than \texttt{b}\end{itemize}
+    \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b}
+    \item define \texttt{r\_f} as the sum of the field $\FIELDf$ of \texttt{r} and the field $\FIELDg$ of \texttt{r}
+    \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res}
+    \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'} (for the output variable \texttt{r'}).
   \end{itemize}
 } % EndDefineProse
diff --git a/asllib/aslspec/tests.t/run.t b/asllib/aslspec/tests.t/run.t
@@ -1,33 +1,54 @@
 # Basic tests
   $ aslspec hello.spec --render; diff -w generated_macros.tex hello.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
+  11c11
+  < \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
+  ---
+  > \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
+  19c19
+  < \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
+  ---
+  > \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
   $ aslspec typedefs.spec --render; diff -w generated_macros.tex typedefs.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
+  12a13
+  > \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
+  24d24
+  < \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
+  30c30
+  < \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
+  ---
+  > \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
   $ aslspec relations.spec --render; diff -w generated_macros.tex relations.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
+  9a10
+  > \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
+  18d18
+  < \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
+  26c26
+  < \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
+  ---
+  > \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
   $ aslspec rule.spec --render; diff -w generated_macros.tex rule.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
-  82,86c82,86
-  <     \item define \texttt{res} as \begin{itemize}\item \texttt{a} if \texttt{a} is equal to \texttt{b}, \item the sum of \texttt{a} and \texttt{b} if \texttt{a} is greater than \texttt{b}, and \item \texttt{b} if \texttt{a} is less than \texttt{b}\end{itemize}
-  <     \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b}
-  <     \item define \texttt{r\_f} as the sum of the field $\FIELDf$ of \texttt{r} and the field $\FIELDg$ of \texttt{r}
-  <     \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res}
-  <     \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'} (for the output variable \texttt{r'}).
+  8a9
+  > \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
+  12d12
+  < \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
+  20c20
+  < \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
   ---
-  >     \item define \texttt{res} as  (1) if \texttt{a} is equal to \texttt{b} holds then \texttt{a},  (2) if \texttt{a} is greater than \texttt{b} holds then the sum of  (1) \texttt{a}, and  (2) \texttt{b}, and  (3) if \texttt{a} is less than \texttt{b} holds then \texttt{b};
-  >     \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b};
-  >     \item define \texttt{r\_f} as the sum of  (1) the field $\FIELDf$ of \texttt{r}, and  (2) the field $\FIELDg$ of \texttt{r};
-  >     \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res};
-  >     \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'}.
+  > \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
   $ aslspec operators.spec --render; diff -w generated_macros.tex operators.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
-  55,56c55,56
-  <     \item the sum of \texttt{a} and \texttt{b} is equal to \texttt{c}
-  <     \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c}
+  10a11
+  > \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
+  12d12
+  < \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
+  18c18
+  < \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
   ---
-  >     \item the sum of all numbers in  (1) \texttt{a}, and  (2) \texttt{b} is equal to \texttt{c};
-  >     \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c};
-
+  > \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
   $ aslspec type_name.bad
   Syntax Error: type_name.bad:1:9: illegal element-defining identifier: t2
   [1]

diff --git a/asllib/aslspec/tests.t/typedefs.expected b/asllib/aslspec/tests.t/typedefs.expected
@@ -27,8 +27,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant