diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean
index 7f3e731d1c..54d31c8cb8 100644
--- a/tests/bench/binarytrees.lean
+++ b/tests/bench/binarytrees.lean
@@ -40,22 +40,22 @@ partial def depth : Nat -> Nat -> List (Nat × Nat × Task UInt32)
 
 def main : List String → IO UInt32
 | [s] := do
-  let n := s.toNat,
-  let maxN := Nat.max (minN + 2) n,
-  let stretchN := maxN + 1,
+  let n := s.toNat;
+  let maxN := Nat.max (minN + 2) n;
+  let stretchN := maxN + 1;
 
   -- stretch memory tree
-  let c := check (make $ UInt32.ofNat stretchN),
-  out "stretch tree" stretchN c,
+  let c := check (make $ UInt32.ofNat stretchN);
+  out "stretch tree" stretchN c;
 
   -- allocate a long lived tree
-  let long := make $ UInt32.ofNat maxN,
+  let long := make $ UInt32.ofNat maxN;
 
   -- allocate, walk, and deallocate many bottom-up binary trees
   let vs := (depth minN maxN), -- `using` (parList $ evalTuple3 r0 r0 rseq)
-  vs.mmap (λ ⟨m,d,i⟩, out (toString m ++ "\t trees") d i.get),
+  vs.mmap (λ ⟨m,d,i⟩, out (toString m ++ "\t trees") d i.get);
 
   -- confirm the the long-lived binary tree still exists
-  out "long lived tree" maxN (check long),
+  out "long lived tree" maxN (check long);
   pure 0
 | _ := pure 1
diff --git a/tests/bench/qsort.lean b/tests/bench/qsort.lean
index 2175f4d3b6..0fe34e672f 100644
--- a/tests/bench/qsort.lean
+++ b/tests/bench/qsort.lean
@@ -10,7 +10,7 @@ def mkRandomArray : Nat → Elem → Array Elem → Array Elem
 partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
 | i :=
   if i < a.size - 1 then do
-    unless (a.get i <= a.get (i+1)) $ throw (IO.userError "array is not sorted"),
+    unless (a.get i <= a.get (i+1)) $ throw (IO.userError "array is not sorted");
     checkSortedAux (i+1)
   else
     pure ()
@@ -54,10 +54,10 @@ qsortAux lt as 0 (UInt32.ofNat (as.size - 1))
 
 def main (xs : List String) : IO Unit :=
 do
-let n := xs.head.toNat,
-n.mfor $ λ _,
+let n := xs.head.toNat;
+n.mfor $ λ _;
 n.mfor $ λ i, do
-  let xs := mkRandomArray i (UInt32.ofNat i) Array.empty,
-  let xs := qsort xs (λ a b, a < b),
-  --IO.println xs,
+  let xs := mkRandomArray i (UInt32.ofNat i) Array.empty;
+  let xs := qsort xs (λ a b, a < b);
+  --IO.println xs;
   checkSortedAux xs 0
diff --git a/tests/bench/rbmap_checkpoint.lean b/tests/bench/rbmap_checkpoint.lean
index 5365678e46..c1e43050bf 100644
--- a/tests/bench/rbmap_checkpoint.lean
+++ b/tests/bench/rbmap_checkpoint.lean
@@ -81,11 +81,11 @@ def myLen : List Tree → Nat → Nat
 
 def main (xs : List String) : IO UInt32 :=
 do
-[n, freq] ← pure xs | throw "invalid input",
-let n     := n.toNat,
-let freq  := freq.toNat,
-let freq  := if freq == 0 then 1 else freq,
-let mList := mkMap n freq,
-let v     := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0,
+[n, freq] ← pure xs | throw "invalid input";
+let n     := n.toNat;
+let freq  := freq.toNat;
+let freq  := if freq == 0 then 1 else freq;
+let mList := mkMap n freq;
+let v     := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0;
 IO.println (toString (myLen mList 0) ++ " " ++ toString v) *>
 pure 0
diff --git a/tests/bench/rbmap_checkpoint2.lean b/tests/bench/rbmap_checkpoint2.lean
index 7ccfa51da0..8eeabd808a 100644
--- a/tests/bench/rbmap_checkpoint2.lean
+++ b/tests/bench/rbmap_checkpoint2.lean
@@ -81,11 +81,11 @@ def myLen : List Tree → Nat → Nat
 
 def main (xs : List String) : IO UInt32 :=
 do
-[n, freq] ← pure xs | throw "invalid input",
-let n     := n.toNat,
-let freq  := freq.toNat,
-let freq  := if freq == 0 then 1 else freq,
-let mList := mkMap n freq,
-let v     := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0,
+[n, freq] ← pure xs | throw "invalid input";
+let n     := n.toNat;
+let freq  := freq.toNat;
+let freq  := if freq == 0 then 1 else freq;
+let mList := mkMap n freq;
+let v     := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0;
 IO.println (toString (myLen mList 0) ++ " " ++ toString v) *>
 pure 0
diff --git a/tests/bench/unionfind.lean b/tests/bench/unionfind.lean
index 9415c9fe4b..44443d085a 100644
--- a/tests/bench/unionfind.lean
+++ b/tests/bench/unionfind.lean
@@ -45,32 +45,32 @@ do d ← read, pure d.size
 def findEntryAux : Nat → Node → M nodeData
 | 0     n := error "out of fuel"
 | (i+1) n :=
-  do s ← read,
+  do s ← read;
      if h : n < s.size then
-       do { let e := s.fget ⟨n, h⟩,
+       do { let e := s.fget ⟨n, h⟩;
             if e.find = n then pure e
-            else do e₁ ← findEntryAux i e.find,
-                    updt (λ s, s.set n e₁),
+            else do e₁ ← findEntryAux i e.find;
+                    updt (λ s, s.set n e₁);
                     pure e₁ }
      else error "invalid Node"
 
 def findEntry (n : Node) : M nodeData :=
-do c ← capacity,
+do c ← capacity;
    findEntryAux c n
 
 def find (n : Node) : M Node :=
 do e ← findEntry n, pure e.find
 
 def mk : M Node :=
-do n ← capacity,
-   updt $ λ s, s.push {find := n, rank := 1},
+do n ← capacity;
+   updt $ λ s, s.push {find := n, rank := 1};
    pure n
 
 def union (n₁ n₂ : Node) : M Unit :=
-do r₁ ← findEntry n₁,
-   r₂ ← findEntry n₂,
+do r₁ ← findEntry n₁;
+   r₂ ← findEntry n₂;
    if r₁.find = r₂.find then pure ()
-   else updt $ λ s,
+   else updt $ λ s;
      if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
      else if r₁.rank = r₂.rank then
         let s₁ := s.set r₁.find { find := r₂.find } in
@@ -83,13 +83,13 @@ def mkNodes : Nat → M Unit
 | (n+1) := mk *> mkNodes n
 
 def checkEq (n₁ n₂ : Node) : M Unit :=
-do r₁ ← find n₁, r₂ ← find n₂,
+do r₁ ← find n₁, r₂ ← find n₂;
    unless (r₁ = r₂) $ error "nodes are not equal"
 
 def mergePackAux : Nat → Nat → Nat → M Unit
 | 0     _ _ := pure ()
 | (i+1) n d :=
-  do c ← capacity,
+  do c ← capacity;
   if (n+d) < c
   then union n (n+d) *> mergePackAux i (n+1) d
   else pure ()
@@ -100,23 +100,23 @@ do c ← capacity, mergePackAux c 0 d
 def numEqsAux : Nat → Node → Nat → M Nat
 | 0     _ r := pure r
 | (i+1) n r :=
-  do c ← capacity,
+  do c ← capacity;
      if n < c
      then do { n₁ ← find n, numEqsAux i (n+1) (if n = n₁ then r else r+1) }
      else pure r
 
 def numEqs : M Nat :=
-do c ← capacity,
+do c ← capacity;
    numEqsAux c 0 0
 
 def test (n : Nat) : M Nat :=
 if n < 2 then error "input must be greater than 1"
 else do
-  mkNodes n,
-  mergePack 50000,
-  mergePack 10000,
-  mergePack 5000,
-  mergePack 1000,
+  mkNodes n;
+  mergePack 50000;
+  mergePack 10000;
+  mergePack 5000;
+  mergePack 1000;
   numEqs
 
 def main (xs : List String) : IO UInt32 :=
diff --git a/tests/bench/unionfind_clean.lean b/tests/bench/unionfind_clean.lean
index 35bafd6154..3d1f9eee77 100644
--- a/tests/bench/unionfind_clean.lean
+++ b/tests/bench/unionfind_clean.lean
@@ -13,32 +13,32 @@ do d ← get, pure d.size
 def findEntryAux : Nat → Node → M nodeData
 | 0     n := throw "out of fuel"
 | (i+1) n :=
-  do s ← get,
+  do s ← get;
      if h : n < s.size then
-       do { let e := s.fget ⟨n, h⟩,
+       do { let e := s.fget ⟨n, h⟩;
             if e.find = n then pure e
-            else do e₁ ← findEntryAux i e.find,
-                    modify (λ s, s.set n e₁),
+            else do e₁ ← findEntryAux i e.find;
+                    modify (λ s, s.set n e₁);
                     pure e₁ }
      else throw "invalid Node"
 
 def findEntry (n : Node) : M nodeData :=
-do c ← capacity,
+do c ← capacity;
    findEntryAux c n
 
 def find (n : Node) : M Node :=
 do e ← findEntry n, pure e.find
 
 def mk : M Node :=
-do n ← capacity,
-   modify $ λ s, s.push {find := n, rank := 1},
+do n ← capacity;
+   modify $ λ s, s.push {find := n, rank := 1};
    pure n
 
 def union (n₁ n₂ : Node) : M Unit :=
-do r₁ ← findEntry n₁,
-   r₂ ← findEntry n₂,
+do r₁ ← findEntry n₁;
+   r₂ ← findEntry n₂;
    if r₁.find = r₂.find then pure ()
-   else modify $ λ s,
+   else modify $ λ s;
      if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
      else if r₁.rank = r₂.rank then
         let s₁ := s.set r₁.find { find := r₂.find } in
@@ -51,13 +51,13 @@ def mkNodes : Nat → M Unit
 | (n+1) := mk *> mkNodes n
 
 def checkEq (n₁ n₂ : Node) : M Unit :=
-do r₁ ← find n₁, r₂ ← find n₂,
+do r₁ ← find n₁, r₂ ← find n₂;
    unless (r₁ = r₂) $ throw "nodes are not equal"
 
 def mergePackAux : Nat → Nat → Nat → M Unit
 | 0     _ _ := pure ()
 | (i+1) n d :=
-  do c ← capacity,
+  do c ← capacity;
   if (n+d) < c
   then union n (n+d) *> mergePackAux i (n+1) d
   else pure ()
@@ -68,23 +68,23 @@ do c ← capacity, mergePackAux c 0 d
 def numEqsAux : Nat → Node → Nat → M Nat
 | 0     _ r := pure r
 | (i+1) n r :=
-  do c ← capacity,
+  do c ← capacity;
      if n < c
      then do { n₁ ← find n, numEqsAux i (n+1) (if n = n₁ then r else r+1) }
      else pure r
 
 def numEqs : M Nat :=
-do c ← capacity,
+do c ← capacity;
    numEqsAux c 0 0
 
 def test (n : Nat) : M Nat :=
 if n < 2 then throw "input must be greater than 1"
 else do
-  mkNodes n,
-  mergePack 50000,
-  mergePack 10000,
-  mergePack 5000,
-  mergePack 1000,
+  mkNodes n;
+  mergePack 50000;
+  mergePack 10000;
+  mergePack 5000;
+  mergePack 1000;
   numEqs
 
 def main (xs : List String) : IO UInt32 :=
diff --git a/tests/compiler/array_test.lean b/tests/compiler/array_test.lean
index 8e0912f02a..c5a5f9a99a 100644
--- a/tests/compiler/array_test.lean
+++ b/tests/compiler/array_test.lean
@@ -7,32 +7,32 @@ a
 
 def main : IO UInt32 :=
 do
- let a : Array Nat := Array.empty,
- IO.println (toString a),
- IO.println (toString a.sz),
- let a := foo a,
- IO.println (toString a),
- let a := a.map (+10),
- IO.println (toString a),
- IO.println (toString a.sz),
- let a1 := a.pop,
- let a2 := a.push 100,
- IO.println (toString a1),
- IO.println (toString a2),
- let a2 := a.pop,
- IO.println a2,
- IO.println $ (([1, 2, 3, 4].toArray).map (+2)).map toString,
- IO.println $ ([1, 2, 3, 4].toArray.extract 1 3),
- IO.println $ ([1, 2, 3, 4].toArray.extract 0 100),
- IO.println $ ([1, 2, 3, 4].toArray.extract 1 1),
- IO.println $ ([1, 2, 3, 4].toArray.extract 2 4),
- IO.println [1,2,3,4].toArray.reverse,
- IO.println ([] : List Nat).toArray.reverse,
- IO.println [1,2,3].toArray.reverse,
- IO.println $ [1,2,3,4].toArray.filter (λ a, a % 2 == 0),
- IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 0),
- IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 1),
- IO.println $ [1,2,3,4].toArray.filter (>2),
- IO.println $ [1,2,3,4].toArray.filter (>10),
- IO.println $ [1,2,3,4].toArray.filter (>0),
+ let a : Array Nat := Array.empty;
+ IO.println (toString a);
+ IO.println (toString a.sz);
+ let a := foo a;
+ IO.println (toString a);
+ let a := a.map (+10);
+ IO.println (toString a);
+ IO.println (toString a.sz);
+ let a1 := a.pop;
+ let a2 := a.push 100;
+ IO.println (toString a1);
+ IO.println (toString a2);
+ let a2 := a.pop;
+ IO.println a2;
+ IO.println $ (([1, 2, 3, 4].toArray).map (+2)).map toString;
+ IO.println $ ([1, 2, 3, 4].toArray.extract 1 3);
+ IO.println $ ([1, 2, 3, 4].toArray.extract 0 100);
+ IO.println $ ([1, 2, 3, 4].toArray.extract 1 1);
+ IO.println $ ([1, 2, 3, 4].toArray.extract 2 4);
+ IO.println [1,2,3,4].toArray.reverse;
+ IO.println ([] : List Nat).toArray.reverse;
+ IO.println [1,2,3].toArray.reverse;
+ IO.println $ [1,2,3,4].toArray.filter (λ a, a % 2 == 0);
+ IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 0);
+ IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 1);
+ IO.println $ [1,2,3,4].toArray.filter (>2);
+ IO.println $ [1,2,3,4].toArray.filter (>10);
+ IO.println $ [1,2,3,4].toArray.filter (>0);
  pure 0
diff --git a/tests/compiler/array_test2.lean b/tests/compiler/array_test2.lean
index df9c14ee0c..1814af3b50 100644
--- a/tests/compiler/array_test2.lean
+++ b/tests/compiler/array_test2.lean
@@ -7,9 +7,9 @@ let a1 := [2, 3, 5].toArray in
 let a2 := [4, 7, 9].toArray in
 let a3 := [4, 7, 8].toArray in
 do
- check (Array.isEqv a1 a2 (λ v w, v % 2 == w % 2)),
- check (!Array.isEqv a1 a3 (λ v w, v % 2 == w % 2)),
- check (a1 ++ a2 == [2, 3, 5, 4, 7, 9].toArray),
- check (a1.any (>4)),
- check (!a1.any (>10)),
+ check (Array.isEqv a1 a2 (λ v w, v % 2 == w % 2));
+ check (!Array.isEqv a1 a3 (λ v w, v % 2 == w % 2));
+ check (a1 ++ a2 == [2, 3, 5, 4, 7, 9].toArray);
+ check (a1.any (>4));
+ check (!a1.any (>10));
  check (a1.all (<10))
diff --git a/tests/compiler/lazylist.lean b/tests/compiler/lazylist.lean
index 13bd8418c1..29dd85a98a 100644
--- a/tests/compiler/lazylist.lean
+++ b/tests/compiler/lazylist.lean
@@ -114,14 +114,14 @@ def iota (i : Nat := 0) : LazyList Nat :=
 LazyList.iterate Nat.succ i
 
 def tst : LazyList String :=
-do x ← [1, 2, 3].toLazy,
-   y ← [2, 3, 4].toLazy,
-   guard (x + y > 5),
+do x ← [1, 2, 3].toLazy;
+   y ← [2, 3, 4].toLazy;
+   guard (x + y > 5);
    pure (toString x ++ " + " ++ toString y ++ " = " ++ toString (x+y))
 
 def main : IO Unit :=
-do let n := 40,
-   IO.println $ tst.isEmpty,
-   IO.println $ tst.head,
-   IO.println $ (fib.interleave (iota.map (+100))).approx n,
+do let n := 40;
+   IO.println $ tst.isEmpty;
+   IO.println $ tst.head;
+   IO.println $ (fib.interleave (iota.map (+100))).approx n;
    IO.println $ (((iota.map (+10)).filter (λ v, v % 2 == 0)).approx n)
diff --git a/tests/compiler/rbmap.lean b/tests/compiler/rbmap.lean
index 0291043a4e..02313fbc5d 100644
--- a/tests/compiler/rbmap.lean
+++ b/tests/compiler/rbmap.lean
@@ -8,29 +8,29 @@ def depth {α β : Type} {lt : α → α → Bool} (m : RBMap α β lt) : Nat :=
 m.depth Nat.max
 
 def tst1 : IO Unit :=
-do let Map := RBMap String Nat (λ a b, a < b),
-   let m : Map := {},
-   let m := m.insert "hello" 0,
-   let m := m.insert "world" 1,
-   check (m.find "hello" == some 0),
-   check (m.find "world" == some 1),
-   let m := m.erase "hello",
-   check (m.find "hello" == none),
-   check (m.find "world" == some 1),
+do let Map := RBMap String Nat (λ a b, a < b);
+   let m : Map := {};
+   let m := m.insert "hello" 0;
+   let m := m.insert "world" 1;
+   check (m.find "hello" == some 0);
+   check (m.find "world" == some 1);
+   let m := m.erase "hello";
+   check (m.find "hello" == none);
+   check (m.find "world" == some 1);
    pure ()
 
 def tst2 : IO Unit :=
-do let Map := RBMap Nat Nat (λ a b, a < b),
-   let m : Map := {},
-   let n : Nat := 10000,
-   let m := n.fold (λ i (m : Map), m.insert i (i*10)) m,
-   check (m.all (λ k v, v == k*10)),
-   check (sz m == n),
-   IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m)),
-   let m := (n/2).fold (λ i (m : Map), m.erase (2*i)) m,
-   check (m.all (λ k v, v == k*10)),
-   check (sz m == n / 2),
-   IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m)),
+do let Map := RBMap Nat Nat (λ a b, a < b);
+   let m : Map := {};
+   let n : Nat := 10000;
+   let m := n.fold (λ i (m : Map), m.insert i (i*10)) m;
+   check (m.all (λ k v, v == k*10));
+   check (sz m == n);
+   IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m));
+   let m := (n/2).fold (λ i (m : Map), m.erase (2*i)) m;
+   check (m.all (λ k v, v == k*10));
+   check (sz m == n / 2);
+   IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m));
    pure ()
 
 abbrev Map := RBMap Nat Nat (λ a b, a < b)
@@ -38,25 +38,25 @@ abbrev Map := RBMap Nat Nat (λ a b, a < b)
 def mkRandMap (max : Nat) : Nat → Map → Array (Nat × Nat) → IO (Map × Array (Nat × Nat))
 | 0     m a := pure (m, a)
 | (n+1) m a := do
-  k ← IO.rand 0 max,
-  v ← IO.rand 0 max,
+  k ← IO.rand 0 max;
+  v ← IO.rand 0 max;
   if m.find k == none then do
-    let m := m.insert k v,
-    let a := a.push (k, v),
+    let m := m.insert k v;
+    let a := a.push (k, v);
     mkRandMap n m a
   else
     mkRandMap n m a
 
 def tst3 (seed : Nat) (n : Nat) (max : Nat) : IO Unit :=
-do IO.setRandSeed seed,
-   (m, a) ← mkRandMap max n {} Array.empty,
-   check (sz m == a.size),
-   check (a.all (λ ⟨k, v⟩, m.find k == some v)),
-   IO.println ("tst3 size: " ++ toString a.size),
-   let m := a.iterate m (λ i ⟨k, v⟩ m, if i.val % 2 == 0 then m.erase k else m),
-   check (sz m == a.size / 2),
-   a.miterate () (λ i ⟨k, v⟩ _, when (i.val % 2 == 1) (check (m.find k == some v))),
-   IO.println ("tst3 after, depth: " ++ toString (depth m) ++ ", size: " ++ toString (sz m)),
+do IO.setRandSeed seed;
+   (m, a) ← mkRandMap max n {} Array.empty;
+   check (sz m == a.size);
+   check (a.all (λ ⟨k, v⟩, m.find k == some v));
+   IO.println ("tst3 size: " ++ toString a.size);
+   let m := a.iterate m (λ i ⟨k, v⟩ m, if i.val % 2 == 0 then m.erase k else m);
+   check (sz m == a.size / 2);
+   a.miterate () (λ i ⟨k, v⟩ _, when (i.val % 2 == 1) (check (m.find k == some v)));
+   IO.println ("tst3 after, depth: " ++ toString (depth m) ++ ", size: " ++ toString (sz m));
    pure ()
 
 def main (xs : List String) : IO Unit :=
diff --git a/tests/compiler/reusebug.lean b/tests/compiler/reusebug.lean
index e7fd575923..bf4a0ddb7b 100644
--- a/tests/compiler/reusebug.lean
+++ b/tests/compiler/reusebug.lean
@@ -23,6 +23,6 @@ def add (a b : Expr) : Expr :=
 addAux a b
 
 def main (xs : List String) : IO UInt32 :=
-do let x := Var "x",
-   IO.println (add (Val 1) (Add (Mul (Val 2) x) x)),
+do let x := Var "x";
+   IO.println (add (Val 1) (Add (Mul (Val 2) x) x));
    pure 0
diff --git a/tests/compiler/t2.lean b/tests/compiler/t2.lean
index 656a2f8c03..3791e8f44c 100644
--- a/tests/compiler/t2.lean
+++ b/tests/compiler/t2.lean
@@ -85,14 +85,14 @@ nestAux n f n e
 
 def deriv (i : Nat) (f : Expr) : IO Expr :=
 do
-  let d := d "x" f,
-  IO.println (toString (i+1) ++ " count: " ++ (toString $ count d)),
+  let d := d "x" f;
+  IO.println (toString (i+1) ++ " count: " ++ (toString $ count d));
   pure d
 
 def main (xs : List String) : IO UInt32 :=
-do let x := Var "x",
-   let f := pow x x,
-   nest deriv 9 f,
+do let x := Var "x";
+   let f := pow x x;
+   nest deriv 9 f;
    pure 0
 
 -- setOption profiler True
diff --git a/tests/compiler/t4.lean b/tests/compiler/t4.lean
index e79fe5e8a2..56fcb64614 100644
--- a/tests/compiler/t4.lean
+++ b/tests/compiler/t4.lean
@@ -98,16 +98,16 @@ nestAux n f n e
 
 def deriv (i : Nat) (f : Expr) : IO Expr :=
 do
-  let d := d "x" f,
-  IO.println (toString (i+1) ++ " count: " ++ (toString $ count d)),
-  IO.println (toString d),
+  let d := d "x" f;
+  IO.println (toString (i+1) ++ " count: " ++ (toString $ count d));
+  IO.println (toString d);
   pure d
 
 def main (xs : List String) : IO UInt32 :=
-do let x := Var "x",
-   let f := add x (mul x (mul x (add x x))),
-   IO.println f,
-   nest deriv 3 f,
+do let x := Var "x";
+   let f := add x (mul x (mul x (add x x)));
+   IO.println f;
+   nest deriv 3 f;
    pure 0
 
 -- setOption profiler True
diff --git a/tests/ir/lirc.lean b/tests/ir/lirc.lean
index dc3f04c586..34b39f4e51 100644
--- a/tests/ir/lirc.lean
+++ b/tests/ir/lirc.lean
@@ -3,11 +3,11 @@ import init.Lean.Ir.lirc
 open Lean.Ir IO
 
 def main : IO Unit :=
-do args ← IO.cmdlineArgs,
+do args ← IO.cmdlineArgs;
    unless (args.length = 1) $
-     IO.fail "Error: incorrect number of arguments, expected `lirc file.Lean`",
-   let fname := args.head,
-   input ← Fs.readFile fname,
+     IO.fail "Error: incorrect number of arguments, expected `lirc file.Lean`";
+   let fname := args.head;
+   input ← Fs.readFile fname;
    match lirc input {mainProc := some "main"} with
    | Except.ok r    := Fs.writeFile (fname ++ ".cpp") r
    | Except.error e := IO.fail (toString e)
diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean
index ed0a18a4ab..549a22c395 100644
--- a/tests/lean/repr_issue.lean
+++ b/tests/lean/repr_issue.lean
@@ -1,7 +1,7 @@
 def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
-catch (do modify $ λ a : Array Nat, a.set 0 33,
+catch (do modify $ λ a : Array Nat, a.set 0 33;
           throw "error")
-      (λ _, do a ← get, pure $ a.get 0)
+      (λ _, do a ← get; pure $ a.get 0)
 
 def ex₁ : StateT (Array Nat) (ExceptT String Id) Nat :=
 foo
diff --git a/tests/lean/run/coroutine.lean b/tests/lean/run/coroutine.lean
index abfe35fe00..68cdb1a286 100644
--- a/tests/lean/run/coroutine.lean
+++ b/tests/lean/run/coroutine.lean
@@ -156,16 +156,16 @@ inductive tree (α : Type u)
 unsafe def visit {α : Type v} : tree α → coroutine Unit α Unit
 | tree.leaf         := pure ()
 | (tree.Node l a r) := do
-  visit l,
-  yield a,
+  visit l;
+  yield a;
   visit r
 
 unsafe def tst {α : Type} [HasToString α] (t : tree α) : ExceptT String IO Unit :=
-do c  ← pure $ visit t,
-   (yielded v₁ c) ← pure $ resume c (),
-   (yielded v₂ c) ← pure $ resume c (),
-   IO.println $ toString v₁,
-   IO.println $ toString v₂,
+do c  ← pure $ visit t;
+   (yielded v₁ c) ← pure $ resume c ();
+   (yielded v₂ c) ← pure $ resume c ();
+   IO.println $ toString v₁;
+   IO.println $ toString v₂;
    pure ()
 
 -- #eval tst (tree.Node (tree.Node (tree.Node tree.leaf 5 tree.leaf) 10 (tree.Node tree.leaf 20 tree.leaf)) 30 tree.leaf)
@@ -176,25 +176,25 @@ namespace ex2
 
 unsafe def ex : StateT Nat (coroutine Nat String) Unit :=
 do
-  x ← read,
-  y ← get,
-  set (y+5),
-  yield ("1) val: " ++ toString (x+y)),
-  x ← read,
-  y ← get,
-  yield ("2) val: " ++ toString (x+y)),
+  x ← read;
+  y ← get;
+  set (y+5);
+  yield ("1) val: " ++ toString (x+y));
+  x ← read;
+  y ← get;
+  yield ("2) val: " ++ toString (x+y));
   pure ()
 
 unsafe def tst2 : ExceptT String IO Unit :=
-do let c := StateT.run ex 5,
-   (yielded r c₁) ← pure $ resume c 10,
-   IO.println r,
-   (yielded r c₂) ← pure $ resume c₁ 20,
-   IO.println r,
-   (done _) ← pure $ resume c₂ 30,
-   (yielded r c₃) ← pure $ resume c₁ 100,
-   IO.println r,
-   IO.println "done",
+do let c := StateT.run ex 5;
+   (yielded r c₁) ← pure $ resume c 10;
+   IO.println r;
+   (yielded r c₂) ← pure $ resume c₁ 20;
+   IO.println r;
+   (done _) ← pure $ resume c₂ 30;
+   (yielded r c₃) ← pure $ resume c₁ 100;
+   IO.println r;
+   IO.println "done";
    pure ()
 
 -- #eval tst2
diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean
index 0ad2d97885..a504a137f7 100644
--- a/tests/lean/run/deriv.lean
+++ b/tests/lean/run/deriv.lean
@@ -84,13 +84,13 @@ unsafe def nest (f : Expr → IO Expr) : Nat → Expr → IO Expr
 
 unsafe def deriv (f : Expr) : IO Expr :=
 do
-  let d := d "x" f,
-  IO.print "count: ",
-  IO.println (count f),
+  let d := d "x" f;
+  IO.print "count: ";
+  IO.println (count f);
   pure d
 
 unsafe def main : IO Unit :=
-do let x := Var "x",
-   let f := pow x x,
-   nest deriv 9 f,
+do let x := Var "x";
+   let f := pow x x;
+   nest deriv 9 f;
    pure ()
diff --git a/tests/lean/run/ext_eff.lean b/tests/lean/run/ext_eff.lean
index 5d01bd33c6..95c0802e9d 100644
--- a/tests/lean/run/ext_eff.lean
+++ b/tests/lean/run/ext_eff.lean
@@ -120,9 +120,9 @@ inductive State (σ : Type) : Type → Type
 @[inline] def eff.get {σ effs} [member (State σ) effs] : eff effs σ := eff.send State.get
 @[inline] def eff.put {σ effs} [member (State σ) effs] (s : σ) : eff effs Unit := eff.send (State.put s)
 instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) :=
-⟨λ α x, do st ← eff.get,
-           let ⟨a, s'⟩ := x.run st,
-           eff.put s',
+⟨λ α x, do st ← eff.get;
+           let ⟨a, s'⟩ := x.run st;
+           eff.put s';
            pure a⟩
 
 @[inline] def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) :=
@@ -169,7 +169,7 @@ instance : HasRepr IO.error :=
       | IO.error.other s := "IO.error.other " ++ repr s⟩
 
 @[inline] def eff.catchIO {effs α} [member IO effs] (x : eff effs α) (catch : IO.error → eff effs α) : eff effs α :=
-x.interpose IO pure (λ β x k, do ex ← monadLift x.try,
+x.interpose IO pure (λ β x k, do ex ← monadLift x.try;
                                  match ex with
                                  | Except.ok b := k b
                                  | Except.error e := catch e)
@@ -185,12 +185,12 @@ eff.catchIO (Except.ok <$> x) (pure ∘ Except.error)
 -- handle IO exceptions before State
 def test1 :=
   let tf : Bool → eff [IO] _ := λ (x : Bool), Reader.run x $ State.run ([] : List String) $ eff.tryIo $
-  do modify (λ xs, "begin"::xs),
-     x ← read,
-     r ← monadLift $ exfn x,
-     modify (λ xs, "end"::xs),
+  do modify (λ xs, "begin"::xs);
+     x ← read;
+     r ← monadLift $ exfn x;
+     modify (λ xs, "end"::xs);
      pure r in
-  do repr <$> eff.runM (tf tt) >>= IO.println,
+  do repr <$> eff.runM (tf tt) >>= IO.println;
      repr <$> eff.runM (tf ff) >>= IO.println
 
 #eval test1
@@ -198,12 +198,12 @@ def test1 :=
 -- handle IO exceptions after State
 def test2 :=
   let tf : Bool → eff [IO] _ := λ (x : Bool), Reader.run x $ eff.tryIo $ State.run ([] : List String) $
-  do modify (λ xs, "begin"::xs),
-     x ← read,
-     r ← monadLift $ exfn x,
-     modify (λ xs, "end"::xs),
+  do modify (λ xs, "begin"::xs);
+     x ← read;
+     r ← monadLift $ exfn x;
+     modify (λ xs, "end"::xs);
      pure r in
-  do repr <$> eff.runM (tf tt) >>= IO.println,
+  do repr <$> eff.runM (tf tt) >>= IO.println;
      repr <$> eff.runM (tf ff) >>= IO.println
 
 #eval test2
diff --git a/tests/lean/run/ext_eff_linear.lean b/tests/lean/run/ext_eff_linear.lean
index 47a8b3198b..39d7f06f6e 100644
--- a/tests/lean/run/ext_eff_linear.lean
+++ b/tests/lean/run/ext_eff_linear.lean
@@ -134,9 +134,9 @@ inductive State (σ : Type) : Type → Type
 @[inline] meta def eff.get {σ effs} [member (State σ) effs] : eff effs σ := eff.send State.get
 @[inline] meta def eff.put {σ effs} [member (State σ) effs] (s : σ) : eff effs Unit := eff.send (State.put s)
 meta instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) :=
-⟨λ α x, do st ← eff.get,
-           let ⟨a, s'⟩ := x.run st,
-           eff.put s',
+⟨λ α x, do st ← eff.get;
+           let ⟨a, s'⟩ := x.run st;
+           eff.put s';
            pure a⟩
 
 meta def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) :=
diff --git a/tests/lean/run/quasi_pattern_unification_approx_issue.lean b/tests/lean/run/quasi_pattern_unification_approx_issue.lean
index 7f06870145..f993dcf15a 100644
--- a/tests/lean/run/quasi_pattern_unification_approx_issue.lean
+++ b/tests/lean/run/quasi_pattern_unification_approx_issue.lean
@@ -42,5 +42,5 @@ first-order unification.
 -/
 
 def foo2 : StateT δ (StateT σ Id) σ :=
-do s : σ  ← monadLift (get : StateT σ Id σ),
+do s : σ  ← monadLift (get : StateT σ Id σ);
    pure s