Support ghc 9.14 in nix

.github/workflows/cabal-build-all.yml

@@ -23,7 +23,7 @@ jobs:
     runs-on: [self-hosted, plutus-runner]
     strategy:
       matrix:
-        ghc: [ghc912, ghc96]
+        ghc: [ghc914, ghc96]
       fail-fast: false
 
     steps:

cabal.project

@@ -107,6 +107,11 @@ if impl (ghc >= 9.14)
     location: https://github.com/snowleopard/alga
     tag: d4e43fb42db05413459fb2df493361d5a666588a
 
+  -- microstache (dependency of criterion) does not allow aeson 2.3 yet,
+  -- and without this constraint the solver hits the backjump limit.
+  constraints:
+    , aeson <2.3
+
   allow-newer:
     , canonical-json:containers
     , cborg:base
@@ -120,5 +125,6 @@ if impl (ghc >= 9.14)
     , serialise:base
     , serialise:containers
     , serialise:time
+    , turtle:containers
     , turtle:time
     , with-utf8:base

doc/notes/fomega/lazy-machine/ckmachine.tex

@@ -11,8 +11,6 @@
                        &        &     & s \return V                 & \textrm{returning a term value}\\
                        &        &     & \ckerror{}                        & \textrm{throwing an error}\\
                        &        &     & \square V                        & \textrm{halt and return a value}
-
-
     \end{array}\]
 }
 \end{subfigure}

doc/papers/unraveling-recursion/RecursiveTerms.lagda

@@ -35,11 +35,11 @@ following types:
   selfApply s = unself s s
 \end{code}
 
-\noindent The first thing we defined was $\Fix0 : (\Type \kindArrow \Type)
+\noindent The first thing we defined was $\FixZero : (\Type \kindArrow \Type)
 \kindArrow \Type$, which is a fixpoint operator that only works at kind $\Type$.
 We won't need the full power of $\ifix$ for this section, so the techniques
 here should be applicable for other recursive variants of \FOM{}, provided
-they are able to define $\Fix0$.
+they are able to define $\FixZero$.
 
 Now we can define the Y combinator and its $\eta$-expanded version, the Z combinator.
 
@@ -75,7 +75,7 @@ a non-strict and strict setting. We will present the steps
 using recursive definitions for clarity, but all of these can be implemented
 with the Z combinator.
 
-Let us start with the function $\fix2$ which takes the fixpoint of a function
+Let us start with the function $\fixTwo$ which takes the fixpoint of a function
 of 2-tuples.
 \begin{code}
   fix₂ : ∀ {A B} → (A × B → A × B) → A × B

doc/papers/unraveling-recursion/RecursiveTermsFormal.tex

@@ -22,13 +22,10 @@
   \Lambda Q . 
   \lambda (k : F\ Q) . 
   r\ f\ \{ Q \}\ (f\ \{ Q \}\ k)))\\
-
   \selk{k}(\seq{T}) &=& \lambda (\seq{x:T}) . x_k\\
-
   \by(\seq{T}) &=& \lambda (r : \forall Q . (\seqFunArr{T}{Q}) \rightarrow Q) . \Lambda Q. 
   \lambda (k : \seqFunArr{T}{Q}).
   k\ \seq{\fixed{r}\ \{ \fixed{Q} \}\ (\selk{j} \fixed{(\seq{T})})}^j\\
-
   \fixml(\seq{T}) &=& \fixBy\ \{ \lambda Q . \seqFunArr{T}{Q} \}\ \by(\seq{T})\\
   \\
   \multicolumn{3}{l}{\textsc{Compilation function}}\\

doc/papers/unraveling-recursion/unraveling-recursion.tex

@@ -91,8 +91,8 @@
 \DeclareMathOperator{\fixo}{\texttt{fix}}
 % metalanguage version for functions
 \DeclareMathOperator{\fixml}{\mathsf{fix}}
-\DeclareMathOperator{\Fix0}{\mathsf{Fix}_0}
-\DeclareMathOperator{\fix2}{\mathsf{fix}_2}
+\DeclareMathOperator{\FixZero}{\mathsf{Fix}_0}
+\DeclareMathOperator{\fixTwo}{\mathsf{fix}_2}
 \DeclareMathOperator{\fixBy}{\mathsf{fixBy}}
 
 % fir syntax bits

doc/plutus-core-spec-old/figures/Builtins.tex

@@ -87,7 +87,6 @@
     \hspace{\builtinoffset}\(\begin{array}{llclll}
     \textrm{Builtin Name} & \textrm{Signature}& \textrm{Type Args} & \textrm{Term Args} & \textrm{Semantics} & \textrm{Success Conditions}\\
 \hline\\
-
 \texttt{ifThenElse}  &  \sig{\alpha}{\boolean, \alpha, \alpha}{\alpha} & \alpha & b, t_1, t_2 &
 \hspace{-2mm} \begin{array}{ll}
   t_1 & \mbox{if $b=\true$}\\
@@ -113,7 +112,6 @@
         \texttt{greaterThanByteString}  &   \sig{}{\str,\str}{\boolean}   & - & s_1 , s_2 & s_1 > s_2\\
         \texttt{takeByteString}         &   \sig{}{\integer,\str}{\str}   & - &   i, s    & \texttt{take} \ i \  s\\
         \texttt{dropByteString}         &   \sig{}{\integer,\str}{\str}   & - &   i, s    & \texttt{drop} \ i \  s\\
-
         \texttt{sha2$\_256$}         &  \sig{}{\str}{\str}  & - &   s           & sha2\_256 \  s\\
         \texttt{sha3$\_256$}         &  \sig{}{\str}{\str}  & - &   s           & sha3\_256\  s\\
 \\
@@ -124,7 +122,6 @@
   \\[-3mm]
   \mathtt{False} & \mbox{otherwise}
   \end{array} &\\
-
     \end{array}\)
 
     \vspace{1em}

doc/plutus-core-spec-old/figures/LexicalGrammar.tex

@@ -5,26 +5,18 @@
 \begin{minipage}{\linewidth}
     \centering
     \[\begin{array}{lrclr}
-
         \textrm{Name}        & n      & ::= & [\texttt{a}\!\hyphen{}\!\texttt{z}\texttt{A}\!\hyphen{}\!\texttt{Z}][\texttt{a}\!\hyphen{}\!\texttt{zA}\!\hyphen{}\!\texttt{Z0}\!\hyphen{}\!\texttt{9\_'}]^*   & \textrm{name}\\
-
         \textrm{Var}           & x      & ::= & n & \textrm{term variable}\\
         \textrm{TyVar}         & \alpha & ::= & n & \textrm{type variable}\\
         \textrm{BuiltinName}   & bn     & ::= & n & \textrm{builtin term name}\\
         \textrm{Integer} & i  & ::= & [\texttt{+-}]^?[\texttt{0}\!\hyphen{}\!\texttt{9}]^+ & \textrm{integer}\\
-
         \textrm{ByteString}   & s  & ::= & \texttt{\#}([\texttt{a}\!\hyphen{}\!\texttt{fA}\!\hyphen{}\!\texttt{F0}\!\hyphen{}\!\texttt{9}][\texttt{a}\!\hyphen{}\!\texttt{fA}\!\hyphen{}\!\texttt{F0}\!\hyphen{}\!\texttt{9}])^+ & \textrm{hex string}\\
-
         \textrm{Version} & v & ::= & [\texttt{0}\!\hyphen{}\!\texttt{9}]^+(.[\texttt{0}\!\hyphen{}\!\texttt{9}]^+)^* & \textrm{version}\\
-
         \textrm{Constant} & cn & ::= & \texttt{()} & \textrm{unit constant}\\
                           &    &     & \true \texttt{\,|\,} \false & \textrm{boolean constant}\\
                           &    &     & i & \textrm{integer constant}\\
                           &    &     & s & \textrm{bytestring constant}\\
-
         \textrm{TypeConstant} & tn    & ::= & n & \textrm{type constant}\\
-
-
     \end{array}\]
     \captionof{figure}{Lexical grammar of Plutus Core}
     \label{fig:lexical-grammar}

doc/plutus-core-spec-old/figures/TermReduction.tex

@@ -18,7 +18,6 @@
                        &   &     & \inAppLeftFrame{M}                 & \textrm{left application}\\
                        &   &     & \inAppRightFrame{V}                & \textrm{right application}\\
                        &   &     & \inBuiltin{bn}{A^*}{V^*}{\_}{M^*}   & \textrm{builtin application}\\
-
     \end{array}\]
     \caption{Grammar of reduction frames}
     \label{fig:reduction-frames}

doc/plutus-core-spec-old/figures/TypedGrammar.tex

@@ -29,7 +29,6 @@
         \textrm{Signature}        & G      & ::= & \sig{(\alpha :: K)^*}{B^*}{C}     & \textrm{signature}\\
         \textrm{Constant Signature}   & Q      & ::= & tn                     & \textrm{constant signature}\\
         \textrm{Program}          & P      & ::= & \version{v}{M}             & \textrm{versioned program}
-
     \end{array}\]
     \captionof{figure}{Grammar of Plutus Core}
     \label{fig:grammar}

doc/plutus-core-spec-old/figures/UntypedGrammar.tex

@@ -14,7 +14,6 @@
                         &        &     & \builtinU{bn}{M^*}     & \textrm{builtin}\\
                         &        &     & \errorU                & \textrm{error}\\
         \textrm{Program}& P      & ::= & \version{v}{M}         & \textrm{versioned program}
-
     \end{array}\]
     \captionof{figure}{Grammar of untyped Plutus Core}
     \label{fig:untyped-grammar}

doc/plutus-core-spec/builtins.tex

@@ -568,7 +568,6 @@ \subsubsection{Parametricity for fully-polymorphic arguments}
 
 %% \begin{minipage}{\linewidth}
 %%     \centering \[\begin{array}{llll}
-
 %%     t & ::= & b   &\text{for } b \in \Uni  \\
 %%     & & \typearg                 \\
 %%     & & \star               \\

doc/plutus-core-spec/untyped-cek-machine.tex

@@ -60,7 +60,6 @@ \section{The CEK machine}
                        &    &       & \inAppRightFrame{V}                                                 & \textrm{right application of value}\\
                        &    &       & \inConstrFrame{i}{\repetition{V}}{(\repetition{M}, \rho)}           & \textrm{constructor argument}\\
                        &    &       & \inCaseFrame{(\repetition{M}, \rho)}                                & \textrm{case scrutinee}
-
     \end{array}\]
     \caption{Grammar of CEK stack frames}
     \label{fig:untyped-cek-reduction-frames}

doc/plutus-core-spec/untyped-grammar.tex

@@ -15,15 +15,12 @@ \subsection{Lexical grammar}
 \begin{minipage}{\linewidth}
     \centering
     \[\begin{array}{lrclr}
-
         \textrm{Name}          & n      & ::= & \texttt{[a-zA-Z][a-zA-Z0-9\_\textquotesingle]*(-[0-9]+)?}   & \textrm{name}\\
-
         \textrm{Var}           & x      & ::= & n & \textrm{term variable}\\
         \textrm{BuiltinName}   & bn     & ::= & n & \textrm{built-in function name}\\
         \textrm{Version} & v & ::= & \texttt{[0-9]+.[0-9]+.[0-9]+}& \textrm{version}\\
         \textrm{Natural}  & k      & ::= & \texttt{[0-9]+} & \textrm{a natural number}\\
         \textrm{Constant} & c & ::= & \langle{\textrm{literal constant}}\rangle& \\
-
     \end{array}\]
     \captionof{figure}{Lexical grammar of Plutus Core}
     \label{fig:lexical-grammar-untyped}
@@ -76,7 +73,6 @@ \subsection{Grammar}
                         &        &     & \kase{M}{N_1 \ldots N_n}        & \textrm{case analysis with $n$ alternatives ($n \geq 0$)}\\
                         &        &     & \errorU                         & \textrm{error}\\
         \textrm{Program}& P      & ::= & \version{v}{M}                  & \textrm{versioned program}
-
     \end{array}\]
     \captionof{figure}{Grammar of untyped Plutus Core}
     \label{fig:untyped-grammar}