From cff6a1d11757bfeeb816421ac1e4a2cccffe2823 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Nov 2019 08:03:22 -0800 Subject: [PATCH] chore: fix tests --- tests/compiler/test_single_interpret.sh | 2 +- tests/lean/ctor_layout.lean | 2 +- tests/plugin/test_single.sh | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh index 1a6a83f1a7..2f591b8cf0 100755 --- a/tests/compiler/test_single_interpret.sh +++ b/tests/compiler/test_single_interpret.sh @@ -6,7 +6,7 @@ fi ulimit -s 8192 LEAN=$1 BIN_DIR=../../bin -export LEAN_PATH=Init=../../library/Init:Test=. +export LEAN_PATH=Init=../../src/Init:Test=. if [ $# -ne 3 ]; then INTERACTIVE=no else diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean index cabd1e478d..1ac357fc1b 100644 --- a/tests/lean/ctor_layout.lean +++ b/tests/lean/ctor_layout.lean @@ -3,7 +3,7 @@ open Lean open Lean.IR def tst : IO Unit := -do initSearchPath "Init=../../library/Init"; +do initSearchPath "Init=../../src/Init"; env ← importModules [{module := `Init.Lean.Compiler.IR.Basic}]; ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse; ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); diff --git a/tests/plugin/test_single.sh b/tests/plugin/test_single.sh index c3e0812584..6b0216220a 100755 --- a/tests/plugin/test_single.sh +++ b/tests/plugin/test_single.sh @@ -5,7 +5,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then fi ulimit -s 8192 BIN_DIR=../../bin -export LEAN_PATH=Init=../../library/Init:Test=. +export LEAN_PATH=Init=../../src/Init:Test=. if [ $# -ne 2 ]; then INTERACTIVE=no else