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 2019-11-22 08:03:22 -08:00
parent e4cc56a6ad
commit cff6a1d117
3 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/compiler/test_single_interpret.sh
View file

@ -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

2
tests/lean/ctor_layout.lean
View file

@ -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);

2
tests/plugin/test_single.sh
View file

@ -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