-
Notifications
You must be signed in to change notification settings - Fork 375
Commit
- Loading branch information
There are no files selected for viewing
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,5 @@ | ||
File Exists | ||
False | ||
True | ||
Just "__PWD__testdir" | ||
Just "__TEST_DIR__/testdir" | ||
hello |
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,6 +1,6 @@ | ||
. ../../testutils.sh | ||
|
||
./gen_expected.sh | ||
run dir.idr | ||
run dir.idr | filter_test_dir | ||
|
||
cat testdir/test.txt | ||
rm -rf testdir |
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
1/1: Building Main (Main.idr) | ||
Installing __TEST_DIR__/build/ttc/Main.ttc to __TEST_DIR__/currently/nonexistent/dir/idris2-0.6.0/testpkg-0 | ||
Installing __TEST_DIR__/build/ttc/Main.ttm to __TEST_DIR__/currently/nonexistent/dir/idris2-0.6.0/testpkg-0 | ||
Installing __TEST_DIR__/build/ttc/Main.ttc to __TEST_DIR__/currently/nonexistent/dir/idris2-0.6.0/testpkg-0 | ||
Installing __TEST_DIR__/build/ttc/Main.ttm to __TEST_DIR__/currently/nonexistent/dir/idris2-0.6.0/testpkg-0 | ||
Installing package file for testpkg to __TEST_DIR__/currently/nonexistent/dir/idris2-0.6.0/testpkg-0 |
This file was deleted.
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,19 +1,10 @@ | ||
. ../../testutils.sh | ||
|
||
if [ "$OS" = "windows" ]; then | ||
MY_PWD="$(cygpath -m "$(pwd)")\\\\" | ||
else | ||
MY_PWD="$(pwd)/" | ||
fi | ||
|
||
MY_PWD="${MY_PWD}" ./gen_expected.sh | ||
|
||
export IDRIS2_PACKAGE_PATH=$IDRIS2_PREFIX/$NAME_VERSION | ||
export IDRIS2_PREFIX=${MY_PWD}currently/nonexistent/dir/ | ||
export IDRIS2_PREFIX=$test_dir/currently/nonexistent/dir/ | ||
|
||
export IDRIS2_INC_CGS= | ||
|
||
idris2 --install ./testpkg.ipkg | sed -r "s/.([0-9]){10}//g" | ||
idris2 --install ./testpkg.ipkg | sed -r "s/.([0-9]){10}//g" | filter_test_dir | ||
|
||
# ../ is there for some extra safety for using rm -rf | ||
rm -rf ../pkg010/build ../pkg010/currently | ||
rm -rf currently |
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
LOG package.depends:10: all depends: ["__TEST_DIR__/depends/bar-0.7.2", "__TEST_DIR__/depends/foo-0.1.0"] |
This file was deleted.
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,11 +1,3 @@ | ||
. ../../testutils.sh | ||
|
||
if [ "$OS" = "windows" ]; then | ||
MY_PWD="$(cygpath -m "$(pwd)")\\\\" | ||
else | ||
MY_PWD="$(pwd)/" | ||
fi | ||
|
||
MY_PWD="${MY_PWD}" ./gen_expected.sh | ||
|
||
idris2 --build test.ipkg --log package.depends:10 | ||
idris2 --build test.ipkg --log package.depends:10 | filter_test_dir |
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
LOG package.depends:10: all depends: ["__TEST_DIR__/depends/bar-0.1.0", "__TEST_DIR__/depends/baz-0.2.0", "__TEST_DIR__/depends/foo-0.2.0"] |
This file was deleted.
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,11 +1,3 @@ | ||
. ../../testutils.sh | ||
|
||
if [ "$OS" = "windows" ]; then | ||
MY_PWD="$(cygpath -m "$(pwd)")\\\\" | ||
else | ||
MY_PWD="$(pwd)/" | ||
fi | ||
|
||
MY_PWD="${MY_PWD}" ./gen_expected.sh | ||
|
||
idris2 --build test.ipkg --log package.depends:10 | ||
idris2 --build test.ipkg --log package.depends:10 | filter_test_dir |
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
(:protocol-version 2 1) | ||
(:return (:ok "Current working directory is \"__TEST_DIR__/b1\"") 1) | ||
(:write-string "1/1: Building B1 (src/B1.idr)" 2) | ||
(:return (:ok ()) 2) | ||
(:return (:ok "1" ((0 1 ((:decor :data))))) 4) | ||
(:return (:ok (("A.i" (:filename "__TEST_DIR__/prefix/idris2-0.6.0/a1-0/A.idr") (:start 2 0) (:end 3 7)))) 5) | ||
(:return (:ok "Current working directory is \"__TEST_DIR__/b2\"") 6) | ||
(:write-string "1/1: Building B2 (src/B2.idr)" 7) | ||
(:return (:ok ()) 7) | ||
(:return (:ok "2" ((0 1 ((:decor :data))))) 8) | ||
(:return (:ok (("A.i" (:filename "__TEST_DIR__/prefix/idris2-0.6.0/a2-0/A.idr") (:start 2 0) (:end 3 7)))) 9) | ||
he file is done, aborting | ||
(:protocol-version 2 1) | ||
(:return (:ok "Current working directory is \"__TEST_DIR__/b2\"") 1) | ||
(:return (:ok ()) 2) | ||
(:return (:ok "2" ((0 1 ((:decor :data))))) 4) | ||
(:return (:ok (("A.i" (:filename "__TEST_DIR__/prefix/idris2-0.6.0/a2-0/A.idr") (:start 2 0) (:end 3 7)))) 5) | ||
(:return (:ok "Current working directory is \"__TEST_DIR__/b1\"") 6) | ||
(:return (:ok ()) 7) | ||
(:return (:ok "1" ((0 1 ((:decor :data))))) 8) | ||
(:return (:ok (("A.i" (:filename "__TEST_DIR__/prefix/idris2-0.6.0/a1-0/A.idr") (:start 2 0) (:end 3 7)))) 9) | ||
he file is done, aborting |
This file was deleted.
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,20 +1,12 @@ | ||
. ../../testutils.sh | ||
|
||
if [ "$OS" = "windows" ]; then | ||
MY_PWD="$(cygpath -m "$(pwd)")\\\\" | ||
else | ||
MY_PWD="$(pwd)/" | ||
fi | ||
|
||
MY_PWD="${MY_PWD}" ./gen_expected.sh | ||
|
||
mkdir prefix | ||
|
||
IDRIS2_PREFIX="${MY_PWD}/prefix" idris2 --install-with-src a1/a1.ipkg > /dev/null | ||
IDRIS2_PREFIX="${MY_PWD}/prefix" idris2 --install-with-src a2/a2.ipkg > /dev/null | ||
IDRIS2_PREFIX="$test_dir/prefix" idris2 --install-with-src a1/a1.ipkg > /dev/null | ||
IDRIS2_PREFIX="$test_dir/prefix" idris2 --install-with-src a2/a2.ipkg > /dev/null | ||
|
||
IDRIS2_PREFIX="${MY_PWD}/prefix" idris2 --no-prelude --ide-mode < input1 | grep -v ":highlight-source" | cut -c 7- | ||
IDRIS2_PREFIX="${MY_PWD}/prefix" idris2 --no-prelude --ide-mode < input2 | grep -v ":highlight-source" | cut -c 7- | ||
IDRIS2_PREFIX="$test_dir/prefix" idris2 --no-prelude --ide-mode < input1 | grep -v ":highlight-source" | cut -c 7- | filter_test_dir | ||
IDRIS2_PREFIX="$test_dir/prefix" idris2 --no-prelude --ide-mode < input2 | grep -v ":highlight-source" | cut -c 7- | filter_test_dir | ||
|
||
rm -r a1/build a2/build b1/build b2/build | ||
rm -rf prefix |
This file was deleted.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,5 @@ | ||
File Exists | ||
False | ||
True | ||
Just "__PWD__testdir" | ||
Just "__TEST_DIR__/testdir" | ||
hello |
This file was deleted.