max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-22 17:46:15 -07:00
parent a0b8f13094
commit 474f9a3695
4 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/Reformat.lean
View file

@ -13,7 +13,7 @@ let (debug, f) : Bool × String := match args with
| _ => panic! "usage: file [-d]"
let env ← mkEmptyEnvironment
let stx ← Lean.Parser.parseFile env args.head!
let (f, _) ← («finally» (PrettyPrinter.ppModule stx) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.format debug } { env := env }
let (f, _) ← (tryFinally (PrettyPrinter.ppModule stx) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.format debug } { env := env }
IO.print f
let stx' ← Lean.Parser.parseModule env args.head! (toString f)
if stx' != stx then

2
tests/lean/run/Reparen.lean
View file

@ -30,7 +30,7 @@ IO.print s;
let cmds := (stx.getArg 1).getArgs;
cmds.forM $ fun cmd => do
let cmd := unparen cmd;
let (cmd, _) ← («finally» (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
let (cmd, _) ← (tryFinally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
let some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
IO.print s

14
tests/lean/run/finally.lean
View file

@ -29,7 +29,7 @@ match r with
def tst2 : M Nat :=
tryCatchThe IO.Error
(«finally» f2 (do set 100; IO.println "finisher executed"))
(tryFinally f2 (do set 100; IO.println "finisher executed"))
(fun _ => get)
#eval (tst2.run).run' 0
@ -38,8 +38,8 @@ tryCatchThe IO.Error
def tst3 : M Nat :=
tryCatchThe IO.Error
(«finally»
(«finally» f1 (do set 100; IO.println "inner finisher executed"; f2; pure ()))
(tryFinally
(tryFinally f1 (do set 100; IO.println "inner finisher executed"; f2; pure ()))
(do modify Nat.succ; IO.println "outer finisher executed"))
(fun _ => get)
@ -48,8 +48,8 @@ tryCatchThe IO.Error
#eval checkE ((tst3.run).run' 0) 101
def tst4 : M Nat := do
let a ← «finally»
(«finally» (pure 42) (do set 100; IO.println "inner finisher executed"; pure ()))
let a ← tryFinally
(tryFinally (pure 42) (do set 100; IO.println "inner finisher executed"; pure ()))
(do modify Nat.succ; IO.println "outer finisher executed");
let s ← get;
pure (a + s)
@ -59,13 +59,13 @@ pure (a + s)
#eval checkE ((tst4.run).run' 0) 143
def tst5 : M Nat := do
let (a, _) ← finally' (pure 42) (fun a? => do IO.println ("finalizer received: " ++ toString a?));
let (a, _) ← tryFinally' (pure 42) (fun a? => do IO.println ("finalizer received: " ++ toString a?));
pure a
#eval (tst5.run).run' 0
def tst6 : M Nat := do
let (a, _) ← finally' f2 (fun a? => do IO.println ("finalizer received: " ++ toString a?));
let (a, _) ← tryFinally' f2 (fun a? => do IO.println ("finalizer received: " ++ toString a?));
pure a
def tst7 : IO Unit :=

2
tests/lean/run/trace.lean
View file

@ -49,7 +49,7 @@ withReader
let opts := opts.setBool `trace.bughunt true;
-- let opts := opts.setBool `trace.slow true;
{ ctx with options := opts })
(tryCatch («finally» x printTraces) (fun _ => IO.println "ERROR"))
(tryCatch (tryFinally x printTraces) (fun _ => IO.println "ERROR"))
#eval run (tst3 true)
#eval run (tst3 false)