Add fix-whitespace, bump actions

.github/workflows/docs-ci-cd.yml

@@ -7,7 +7,7 @@ jobs:
   build-docs-job:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v6
       - uses: cachix/install-nix-action@v22
         with:
           nix_path: nixpkgs=channel:nixos-unstable
@@ -21,7 +21,7 @@ jobs:
           nix-shell --pure --run "make NO_STACK=y html"
           nix-shell --pure --run "make NO_STACK=y pdf"
           cp dist/pbook.pdf _site/book.pdf
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         with:
           name: generated-site
           path: _site
@@ -34,7 +34,7 @@ jobs:
     if: success() && github.ref == 'refs/heads/main'
     steps:
       - uses: actions/checkout@v3
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         with:
           name: generated-site
           path: _site

.github/workflows/whitespace.yml

@@ -0,0 +1,12 @@
+name: Whitespace
+
+on:
+  pull_request:
+  push:
+
+jobs:
+  whitespace:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: andreasabel/fix-whitespace-action@v1

.gitignore

@@ -4,4 +4,4 @@
 .stack-work
 liquidhaskell-tutorial.cabal
 _site
-dist
+dist

Main.hs

@@ -1,6 +1,6 @@
-module Main where 
+module Main where
 
-import qualified Data.List as L 
+import qualified Data.List as L
 import System.Directory (listDirectory)
 import System.FilePath (addExtension)
 import System.FilePath ((</>))
@@ -21,7 +21,7 @@ hideIgnore file = do
   writeFile tmpFile str
 
 hide :: String -> String
-hide str 
+hide str
   | L.isPrefixOf "{-@ ignore " str = "-- " ++ str
   | L.isPrefixOf "{-@ fail "   str = "-- " ++ str
-  | otherwise                      = str
+  | otherwise                      = str

README.md

@@ -10,7 +10,7 @@ the github repository and run locally for best results.
 
 LH is available as a GHC plugin from version 0.8.10.
 
-Thus, **the best way** to do this tutorial is to 
+Thus, **the best way** to do this tutorial is to
 
 **Step 1** Clone this repository,
 
@@ -24,13 +24,13 @@ $ git clone https://github.com/ucsd-progsys/liquidhaskell-tutorial.git
 $ cabal v2-build
 ```
 
-or 
+or
 
 ```
 $ stack build --fast --file-watch
 ```
 
-The above workflow will let you use whatever Haskell tooling you use for your 
+The above workflow will let you use whatever Haskell tooling you use for your
 favorite editor, to automatically display LH errors as well.
 
 ## Contents

build.sh

@@ -2,14 +2,14 @@
 
 mkHTML() {
    srcFile=$1
-  
+
    echo "HTML for $srcFile"
 
    PANDOC_TARGET=src/$srcFile.html PANDOC_CODETEMPLATE=../liquid-client/templates/code.template stack exec -- pandoc --from=markdown+lhs+raw_html --to=html5 -s --mathjax --standalone --mathjax --toc --section-divs --filter filters/Codeblock.hs --filter filters/Figures.hs --filter filters/Html.hs --variable=notitle --highlight-style=tango --template=dist/page.template templates/preamble.lhs src/$srcFile.lhs templates/bib.lhs -o src/$srcFile.html
 }
 
 
-mkLHS() { 
+mkLHS() {
    echo "Build single LHS file"
    cat src/Tutorial_01_Introduction.lhs src/Tutorial_02_Logic.lhs src/Tutorial_03_Basic.lhs src/Tutorial_04_Polymorphism.lhs src/Tutorial_05_Datatypes.lhs src/Tutorial_06_Measure_Bool.lhs src/Tutorial_07_Measure_Int.lhs src/Tutorial_08_Measure_Set.lhs src/Tutorial_09_Case_Study_Lazy_Queues.lhs src/Tutorial_10_Case_Study_Associative_Maps.lhs src/Tutorial_11_Case_Study_Pointers.lhs src/Tutorial_12_Case_Study_AVL.lhs > dist/pbook.lhs
 }

filters/Figures.hs

@@ -104,7 +104,7 @@ isFigure s    = s `elem` ["figure", "marginfigure"]
 
 makeFigure tgt prefix t r id cls kvs
   = RawBlock (Format tgtTxt) . pad prefix t id cls kvs <$> getCount r id
-    where tgtTxt = T.pack $ show tgt 
+    where tgtTxt = T.pack $ show tgt
 
 -- pad :: Text -> _ -> _ -> _ -> [(Text, Text)]
 pad prefix tplt id cls kvs n
@@ -139,7 +139,7 @@ emptyInfo
 
 getCount r id
   = do info <- readIORef r
-       let idS = T.unpack id 
+       let idS = T.unpack id
        let m  = label info
        let c  = chapter info
        let i  = count info

filters/Latex.hs

@@ -31,7 +31,7 @@ toLaTeX :: Text -> Text -> [Block] -> Text
 toLaTeX cls id                        = wrapLatex cls id . either errHandler (\x -> x) . runPure . writeLaTeX def . Pandoc mempty
   where errHandler = error $ unpack $ mconcat ["toLaTex: ", cls, " ", id]
 
-wrapLatex :: Text -> Text -> Text -> Text 
+wrapLatex :: Text -> Text -> Text -> Text
 wrapLatex "footnotetext" _ str        = T.pack $ printf "\\footnotetext{%s}" (T.unpack str)
 wrapLatex "hwex" name str             = T.pack $ printf "\\begin{hwex}[%s]\n%s\n\\end{hwex}" (T.unpack name) (T.unpack str)
 wrapLatex cls name str                = error $ printf "WrapLatex: %s %s" cls name
@@ -76,7 +76,7 @@ txBlock _ b                  = [b]
 
 expandCodeBlock :: Block -> [Block]
 expandCodeBlock (CodeBlock a s) = CodeBlock a `fmap` tWords s
-  where 
+  where
     tWords = fmap pack . words . unpack
 -------------------------------------------------------------------------------------
 -------------------------------------------------------------------------------------

fix-whitespace.yaml

@@ -0,0 +1,81 @@
+# This file contains the project-specific settings for `fix-whitespace` a tiny
+# but useful tool to
+#
+# * Removes trailing whitespace.
+# * Removes trailing lines containing nothing but whitespace.
+# * Ensures that the file ends in a newline character.
+#
+# By default, fix-whitespace checks every directory under the current working
+# directory but no files. This program should be placed under a text-based
+# project.
+#
+# For directories,
+#
+# 1) excluded-dirs is a black-list of directories,
+# 2) included-dirs is a white-list of excluded-dirs
+#
+# For files,
+#
+# 3) included-files is a white-list of files,
+# 4) excluded-files is a black-list of included-files.
+#
+# The extended glob pattern can be used to specify file/direcotory names.
+# For details, see http://hackage.haskell.org/package/filemanip-0.3.6.3/docs/System-FilePath-GlobPattern.html
+#
+included-dirs:
+    # Without this line the above path will be excluded.
+
+excluded-dirs:
+  - "**/dist*"   # matches every dist* in any directory
+  - .git
+  - .stack-work
+  - .vscode
+  - js
+  - css
+
+# Every matched filename is included unless it is matched by excluded-files.
+included-files:
+  - "*.ac"
+  - "*.bat"
+  - "*.c"
+  - "*.cabal"
+  - "*.cfg"
+  - "*.cmm"
+  - "*.conf"
+  - "*.config"
+  - "*.cpp"
+  - "*.css"
+  - "*.dhall"
+  - "*.h"
+  - "*.hs"
+  - "*.hs-boot"
+  - "*.hsc"
+  - "*.hsig"
+  - "*.html"
+  - "*.in"
+  - "*.inc"
+  - "*.js"
+  - "*.json"
+  - "*.lhs"
+  - "*.md"
+  - "*.project"
+  - "*.py"
+  - "*.rst"
+  - "*.sh"
+  - "*.sty"
+  - "*.tex"
+  - "*.toml"
+  - "*.txt"
+  - "*.yaml"
+  - "*.yml"
+  - "cabal.project.*"
+  - .gitattributes
+  - .gitignore
+  - AUTHORS
+  - LICENSE
+
+excluded-files:
+# Exceptions
+
+# Files that use tabs
+  - Makefile

src/Tutorial_01_Introduction.lhs

@@ -55,7 +55,7 @@ with modern languages like Go, Python, JavaScript and Lua; and of
 course, they're widely used in Haskell too.
 
 ~~~~~{.ghci}
-ghci> :m +Data.Map 
+ghci> :m +Data.Map
 ghci> let m = fromList [ ("haskell", "lazy")
                        , ("ocaml"  , "eager")]
 
@@ -177,9 +177,9 @@ Getting Started
 As of July 2020, LiquidHaskell, version 0.8.10 onwards, is available
 as a [GHC plugin](https://downloads.haskell.org/~ghc/8.10.1/docs/html/users_guide/extending_ghc.html).
 
-This means, roughly, that you need simply 
+This means, roughly, that you need simply
 
-1. Add LH to your project dependencies, after which 
+1. Add LH to your project dependencies, after which
 2. GHC produces LH type errors whenever you compile the code, so that you can
 3. View errors using your favorite editor's existing Haskell tooling.
 
@@ -256,4 +256,3 @@ via pull-requests on github.
 
 \noindent Lets begin!
 
-

src/Tutorial_03_Basic.lhs

@@ -76,7 +76,7 @@ nonsense :: Int
 nonsense = one'
   where
   {-@ one' :: Zero @-}
-  one' = 1 
+  one' = 1
 \end{code}
 
 \noindent

src/Tutorial_04_Polymorphism.lhs

@@ -302,7 +302,7 @@ absoluteSum     = undefined
 
 \newthought{Inference}
 LiquidHaskell verifies `vectorSum` -- or, to be precise,
-the safety of the vector accesses `vec ! i`. 
+the safety of the vector accesses `vec ! i`.
 The verification works out because LiquidHaskell is able to
 *automatically infer* ^[In your editor, click on `go` to see the inferred type.]
 
@@ -315,8 +315,8 @@ between `0` and the length of `vec` (inclusive). LiquidHaskell
 uses this and the test that `i < sz` to establish that `i` is
 between `0` and `(vlen vec)` to prove safety.
 
-**Note** you need to run `liquid` with the option `--no-termination` 
-or make sure your source file has `{-@ LIQUID "--no-termination" @-}, 
+**Note** you need to run `liquid` with the option `--no-termination`
+or make sure your source file has `{-@ LIQUID "--no-termination" @-},
 otherwise the code for `go` fails the now default termination check.
 We will come back to this example later to see how to verify termination
 using metrics.

src/Tutorial_06_Measure_Bool.lhs

@@ -389,5 +389,3 @@ In this chapter we saw how LiquidHaskell lets you
 \noindent
 Of course, we can do a lot more with measures, so let's press on!
 
-
-

src/Tutorial_07_Measure_Int.lhs

@@ -460,7 +460,7 @@ We can use the dimension aware lists to create a safe vector API.
 
 \begin{code}
 {-@ data Vector a = V { vDim  :: Nat
-                      , vElts :: ListN a vDim }         
+                      , vElts :: ListN a vDim }
   @-}
 \end{code}
 

src/Tutorial_09_Case_Study_Lazy_Queues.lhs

@@ -14,8 +14,8 @@ invariant with LiquidHaskell.
 {-@ LIQUID "--no-termination" @-}
 {-@ LIQUID "--maxparams=3"    @-}
 
-module Tutorial_09_Case_Study_Lazy_Queues 
-  (Queue, insert, remove, emp, realSize) 
+module Tutorial_09_Case_Study_Lazy_Queues
+  (Queue, insert, remove, emp, realSize)
   where
 
 import Prelude hiding (replicate, take, length)

src/Tutorial_12_Case_Study_AVL.lhs

@@ -23,7 +23,7 @@ module Tutorial_12_Case_Study_AVL
   , elems, hasElem, addElem, delElem
   )
   where
-    
+
 import qualified Data.Set as S
 import Prelude hiding (max)
 -- import Language.Haskell.Liquid.Prelude (liquidAssume)

src/todo/case-study-kmeans.lhs

@@ -433,4 +433,3 @@ implementation) to verify that KMeans indeed produces at most `k` clusters...
 [demo]:          http://goto.ucsd.edu/~rjhala/liquid/haskell/demo/#?demo=KMeansHelper.hs
 [URL-kmeans]:    http://hackage.haskell.org/package/kmeans
 
-

stack.yaml

@@ -17,4 +17,3 @@ extra-deps:
   - git: https://github.com/ucsd-progsys/liquid-fixpoint
     commit: 1aab5d84e3dd96f3052dd27b92316cbb5254def1
 
-

templates/bib.lhs

@@ -4,13 +4,13 @@
 [vecspec]:         https://github.com/ucsd-progsys/liquidhaskell/blob/91e1074575ca102df810ea399c5a13063e8c8011/include/Data/Vector.spec
 [vec]:             http://hackage.haskell.org/package/vector
 [agdavec]:         http://code.haskell.org/Agda/examples/Vec.agda
-[ref101]:          /blog/2013/01/01/refinement-types-101.lhs/ 
-[ref102]:          /blog/2013/01/27/refinements-101-reax.lhs/ 
+[ref101]:          /blog/2013/01/01/refinement-types-101.lhs/
+[ref102]:          /blog/2013/01/27/refinements-101-reax.lhs/
 [data-list]:       https://hackage.haskell.org/package/base-4.18.0.0/docs/Data-List.html
 [foldl]:           https://hackage.haskell.org/package/base-4.18.0.0/docs/Data-List.html#v:foldl
 [listtail]:        /blog/2013/01/31/safely-catching-a-list-by-its-tail.lhs/
 [dmlarray]:        https://www.cs.cmu.edu/~fp/papers/pldi98dml.pdf
-[liquid-tutorial]: http://github.com/ucsd-progsys/liquidhaskell-tutorial.git 
+[liquid-tutorial]: http://github.com/ucsd-progsys/liquidhaskell-tutorial.git
 [liquid-emacs]:    https://github.com/ucsd-progsys/liquid-types.el
 [liquid-vim]:      https://github.com/ucsd-progsys/liquid-types.vim
 [liquid-spacemacs]: https://github.com/ucsd-progsys/liquid-types-spacemacs

templates/book.tex

@@ -6,7 +6,7 @@
 
 \usepackage{amssymb,amsmath}
 \usepackage{ifxetex,ifluatex}
-\usepackage{fixltx2e} 
+\usepackage{fixltx2e}
 
 \ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
   \usepackage[T1]{fontenc}
@@ -104,14 +104,14 @@
 
 \VerbatimFootnotes % allows verbatim text in footnotes
 
-\title{LiquidHaskell} 
+\title{LiquidHaskell}
 
 \author{Ranjit Jhala}
 
 \date{\today}
 
 \newcommand\cc[1]{\texttt{#1}}
-\newcommand\myfootnote[1]{\footnotetext{#1}} 
+\newcommand\myfootnote[1]{\footnotetext{#1}}
 
 
 %% EXERCISE: HANDROLLED
@@ -131,22 +131,22 @@
 \usepackage{xcolor}
 
 
-% spec 
+% spec
 \DefineVerbatimEnvironment%
   {spec}{Verbatim}
   {}
 
-% error 
+% error
 \DefineVerbatimEnvironment%
   {liquiderror}{Verbatim}
   {}
 
-% shell 
+% shell
 \DefineVerbatimEnvironment%
   {shell}{Verbatim}
   {}
 
-% orig 
+% orig
 \DefineVerbatimEnvironment%
   {redverbatim}{Verbatim}
   {formatcom=\color{red}}