Fix unit tests for Windows

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/tests/frontends/lean/lean_pp.cpp

@@ -74,6 +74,8 @@ static void tst5() {
     frontend f;
     std::shared_ptr<string_output_channel> out(new string_output_channel());
     f.set_regular_channel(out);
+    f.set_option(name{"pp", "unicode"}, true);
+    f.set_option(name{"lean", "pp", "notation"}, true);
     regular(f) << And(Const("a"), Const("b"));
     lean_assert(out->str() == "a ∧ b");
     f.set_option(name{"lean", "pp", "notation"}, false);
@@ -95,8 +97,9 @@ static void tst6() {
     expr t = mk_deep(10);
     f.set_option(name{"lean", "pp", "max_depth"}, 5);
     f.set_option(name{"pp", "colors"}, false);
+    f.set_option(name{"pp", "unicode"}, false);
     regular(f) << t;
-    lean_assert(out->str() == "f (f (f (f (f (…)))))");
+    lean_assert(out->str() == "f (f (f (f (f (...)))))");
 }
 
 int main() {

tests/lean/arith1.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Check 10 + 20
 Check 10
 Check 10 - 20

tests/lean/arith1.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
 Nat
 Nat
 Int

tests/lean/arith2.lean.expected.out

@@ -1,3 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
 1 / 2
 2/3
 3 div 2

tests/lean/arith3.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Eval 8 mod 3
 Eval 8 div 4
 Eval 7 div 3

tests/lean/arith3.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
 2
 2
 2

tests/lean/arith4.lean.expected.out

@@ -1,3 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
   Assumed: x
 sin x
 sin (x + -1 * (π / 2))

tests/lean/arith5.lean.expected.out

@@ -1,3 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
   Assumed: x
 (1 + -1 * (exp (-2 * x))) / (2 * (exp (-1 * x)))
 (1 + (exp (-2 * x))) / (2 * (exp (-1 * x)))

tests/lean/coercion1.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable T : Type
 Variable R : Type
 Variable f : T -> R

tests/lean/coercion1.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: T
   Assumed: R
   Assumed: f
@@ -6,12 +7,12 @@
 Variable f : T → R
 Coercion f
   Assumed: g
-Error (line: 9, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types
+Error (line: 8, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types
   Assumed: h
-Error (line: 11, pos: 0) invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)
+Error (line: 10, pos: 0) invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)
   Defined: T2
   Defined: R2
   Assumed: f2
-Error (line: 15, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types
+Error (line: 14, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types
   Assumed: id
-Error (line: 17, pos: 0) invalid coercion declaration, 'from' and 'to' types are the same
+Error (line: 16, pos: 0) invalid coercion declaration, 'from' and 'to' types are the same

tests/lean/coercion2.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable T : Type
 Variable R : Type
 Variable t2r : T -> R

tests/lean/coercion2.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: T
   Assumed: R
   Assumed: t2r

tests/lean/config.lean

@@ -0,0 +1,3 @@
+(* Set default configuration for tests *)
+Set pp::colors  false
+Set pp::unicode true

tests/lean/config.lean.expected.out

@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Set: pp::colors
+  Set: pp::unicode

tests/lean/ex1.lean.expected.out

@@ -1 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
 test

tests/lean/ex2.lean

@@ -1,6 +1,5 @@
 (* comment *)
 (* (* nested comment *) *)
-Set pp::colors false
 Show true
 Set lean::pp::notation false
 Show true && false

tests/lean/ex2.lean.expected.out

@@ -1,15 +1,16 @@
   Set: pp::colors
+  Set: pp::unicode
 ⊤
   Set: lean::pp::notation
 and ⊤ ⊥
   Set: pp::unicode
 and true false
   Assumed: a
-Error (line: 10, pos: 0) invalid object declaration, environment already has an object named 'a'
+Error (line: 9, pos: 0) invalid object declaration, environment already has an object named 'a'
   Assumed: b
 and a b
   Assumed: A
-Error (line: 14, pos: 11) type mismatch at application
+Error (line: 13, pos: 11) type mismatch at application
     and a A
 Function type:
     Bool -> Bool -> Bool
@@ -17,8 +18,8 @@ Arguments types:
     Bool
     Type
 Variable A : Type
-(pp::unicode := false, lean::pp::notation := false, pp::colors := false)
-Error (line: 17, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
-Error (line: 18, pos: 23) invalid option value, given option is not an integer
+(lean::pp::notation := false, pp::unicode := false, pp::colors := false)
+Error (line: 16, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
+Error (line: 17, pos: 23) invalid option value, given option is not an integer
   Set: lean::pp::notation
 a /\ b

tests/lean/ex3.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable myeq : Pi (A : Type), A -> A -> Bool
 Show myeq _ true false
 Variable T : Type

tests/lean/ex3.lean.expected.out

@@ -1,9 +1,10 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: myeq
 myeq Bool ⊤ ⊥
   Assumed: T
   Assumed: a
-Error (line: 6, pos: 6) type mismatch at application
+Error (line: 5, pos: 6) type mismatch at application
     myeq Bool ⊤ a
 Function type:
     Π (A : Type) (_ _ : A), Bool
@@ -13,7 +14,7 @@ Arguments types:
     T
   Assumed: myeq2
   Set: lean::pp::implicit
-Error (line: 10, pos: 15) type mismatch at application
+Error (line: 9, pos: 15) type mismatch at application
     myeq2::explicit Bool ⊤ a
 Function type:
     Π (A : Type) (a b : A), Bool

tests/lean/overload1.lean.expected.out

@@ -1,3 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
   Assumed: N
   Assumed: f
   Assumed: g

tests/lean/overload2.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Show 1 + true
 Variable R : Type
 Variable T : Type

tests/lean/overload2.lean.expected.out

@@ -1,5 +1,6 @@
   Set: pp::colors
-Error (line: 2, pos: 9) application type mismatch, none of the overloads can be used
+  Set: pp::unicode
+Error (line: 1, pos: 10) application type mismatch, none of the overloads can be used
 Candidates:
     Real::add : Real → Real → Real
     Int::add : Int → Int → Int
@@ -22,7 +23,7 @@ f a b
 f (r2t b) (t2r a)
   Assumed: g
 f a b
-Error (line: 20, pos: 10) ambiguous overloads
+Error (line: 19, pos: 10) ambiguous overloads
 Candidates:
     g : R → T → R
     f : T → R → T

tests/lean/test.sh

@@ -13,7 +13,7 @@ fi
 NUM_ERRORS=0
 for f in `ls *.lean`; do
     echo "-- testing $f"
-    $LEAN $f > $f.produced.out
+    $LEAN config.lean $f > $f.produced.out
     if test -f $f.expected.out; then
         if diff $f.produced.out $f.expected.out; then
             echo "-- checked"

tests/lean/tst1.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 (* Define a "fake" type to simulate the natural numbers. This is just a test. *)
 Variable N : Type
 Variable lt : N -> N -> Bool

tests/lean/tst1.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: N
   Assumed: lt
   Assumed: zero

tests/lean/tst10.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable a : Bool
 Variable b : Bool
 (* Conjunctions *)

tests/lean/tst10.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: a
   Assumed: b
 a ∧ b

tests/lean/tst11.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Definition xor (x y : Bool) : Bool := (not x) = y
 Infixr 50 ⊕ : xor
 Show xor true false

tests/lean/tst11.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Defined: xor
 ⊤ ⊕ ⊥
 ⊥

tests/lean/tst12.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Show (fun x : Bool, (fun y : Bool, x /\ y))
 Show let x := true,
          y := true

tests/lean/tst12.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
 λ x y : Bool, x ∧ y
 let x := ⊤,
     y := ⊤,

tests/lean/tst13.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Show fun x : Bool, (fun x : Bool, x).
 Show let x := true,
          y := true

tests/lean/tst13.lean.expected.out

@@ -1,3 +1,4 @@
   Set: pp::colors
+  Set: pp::unicode
 λ x x : Bool, x
 let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z

tests/lean/tst14.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Show Int -> Int -> Int
 Variable f : Int -> Int -> Int
 Eval f 0

tests/lean/tst14.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
 Int → Int → Int
   Assumed: f
 f 0

tests/lean/tst15.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable x : Type max U+1+2 M+1 M+2 3
 Check x
 Variable f : Type U+10 -> Type

tests/lean/tst15.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: x
 Type U+3 ⊔ M+2 ⊔ 3
   Assumed: f

tests/lean/tst16.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable f : Type -> Bool
 Show forall a b : Type, (f a) = (f b)
 Variable g : Bool -> Bool -> Bool

tests/lean/tst16.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: f
 ∀ a b : Type, (f a) = (f b)
   Assumed: g

tests/lean/tst17.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable f : Type -> Bool
 Variable g : Type -> Type -> Bool
 Show forall (a b : Type), exists (c : Type), (g a b) = (f c)

tests/lean/tst17.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: f
   Assumed: g
 ∀ a b : Type, ∃ c : Type, (g a b) = (f c)

tests/lean/tst2.lean.expected.out

@@ -1,12 +1,14 @@
-⟨⟩
+  Set: pp::colors
+  Set: pp::unicode
+⟨pp::unicode ↦ true, pp::colors ↦ false⟩
   Assumed: a
   Assumed: b
 a ∧ b
   Set: lean::pp::notation
-⟨lean::pp::notation ↦ false⟩
+⟨lean::pp::notation ↦ false, pp::unicode ↦ true, pp::colors ↦ false⟩
 and a b
-Variable a : Bool
-Variable b : Bool
+Variable a : Bool
+Variable b : Bool
   Set: lean::pp::notation
-⟨lean::pp::notation ↦ true⟩
+⟨lean::pp::notation ↦ true, pp::unicode ↦ true, pp::colors ↦ false⟩
 a ∧ b

tests/lean/tst3.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Set lean::parser::verbose false.
 Notation 10 if _ then _ : implies.
 Show Environment 1.

tests/lean/tst3.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
 Notation 10 if _ then _ : implies
 if ⊤ then ⊥
 if ⊤ then (if a then ⊥)

tests/lean/tst4.lean

@@ -7,7 +7,6 @@ Show f n1 n2
 Show f (fun x : N -> N, x) (fun y : _, y)
 Variable EqNice {A : Type} (lhs rhs : A) : Bool
 Infix 50 === : EqNice
-Set pp::colors false
 Show n1 === n2
 Check f n1 n2
 Check Congr::explicit

tests/lean/tst4.lean.expected.out

@@ -1,12 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
   Assumed: f
   Assumed: N
   Assumed: n1
   Assumed: n2
   Set: lean::pp::implicit
 f::explicit N n1 n2
-f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
+f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
   Assumed: EqNice
-  Set: pp::colors
 EqNice::explicit N n1 n2
 N
 Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b)

tests/lean/tst5.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable N : Type
 Variable a : N
 Variable b : N

tests/lean/tst5.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: N
   Assumed: a
   Assumed: b

tests/lean/tst6.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable N : Type
 Variable h : N -> N -> N
 

tests/lean/tst6.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: N
   Assumed: h
   Proved: CongrH

tests/lean/tst7.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable f : Pi (A : Type), A -> Bool
 Show fun (A B : Type) (a : _), f B a
 (* The following one should produce an error *)

tests/lean/tst7.lean.expected.out

@@ -1,7 +1,8 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: f
 λ (A B : Type) (a : B), f B a
-Error (line: 5, pos: 40) application type mismatch during term elaboration at term
+Error (line: 4, pos: 40) application type mismatch during term elaboration at term
     f B a
 Elaborator state
     #0 ≈ lift:0:2 ?M0

tests/lean/tst8.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Check fun (A : Type) (a : A),
           let b := a
           in b

tests/lean/tst8.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
 Π (A : Type) (a : A), A
   Assumed: g
   Defined: f

tests/lean/tst9.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Variable f : Pi A : Type, A -> A -> A
 Variable N : Type
 Variable g : N -> N -> Bool

tests/lean/tst9.lean.expected.out

@@ -1,9 +1,10 @@
   Set: pp::colors
+  Set: pp::unicode
   Assumed: f
   Assumed: N
   Assumed: g
   Assumed: a
-Error (line: 6, pos: 6) type mismatch at application
+Error (line: 5, pos: 6) type mismatch at application
     g ⊤ (f _ a a)
 Function type:
     N → N → Bool

tests/lean/unicode.lean

@@ -1,4 +1,3 @@
-Set pp::colors false
 Show true /\ false
 Set pp::unicode false
 Show true /\ false

tests/lean/unicode.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
+  Set: pp::unicode
 ⊤ ∧ ⊥
   Set: pp::unicode
 true /\ false