-
Notifications
You must be signed in to change notification settings - Fork 375
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into default-implicits-in-named-implementations
- Loading branch information
Showing
15 changed files
with
427 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
src/*xistent* | ||
src/..a-dot-named-file | ||
src/another-fancy-record.json |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,61 @@ | ||
--- Print dirs with ipkg --- | ||
1/1: Building Inside.PrintDirs (src/Inside/PrintDirs.idr) | ||
LOG elab:0: project dir: __TEST_DIR__ | ||
LOG elab:0: source dir: __TEST_DIR__/src | ||
LOG elab:0: current module dir: __TEST_DIR__/src/Inside | ||
LOG elab:0: submodules dir: __TEST_DIR__/src/Inside/PrintDirs | ||
LOG elab:0: build dir: __TEST_DIR__/build | ||
|
||
--- Print dirs with ipkg (with changed pwd) --- | ||
1/1: Building Inside.PrintDirs (src/Inside/PrintDirs.idr) | ||
LOG elab:0: project dir: __TEST_DIR__ | ||
LOG elab:0: source dir: __TEST_DIR__/src | ||
LOG elab:0: current module dir: __TEST_DIR__/src/Inside | ||
LOG elab:0: submodules dir: __TEST_DIR__/src/Inside/PrintDirs | ||
LOG elab:0: build dir: __TEST_DIR__/build | ||
|
||
--- Print dirs without ipkg (with changed pwd) --- | ||
1/1: Building Inside.PrintDirs (Inside/PrintDirs.idr) | ||
LOG elab:0: project dir: __TEST_DIR__ | ||
LOG elab:0: source dir: __TEST_DIR__ | ||
LOG elab:0: current module dir: __TEST_DIR__/Inside | ||
LOG elab:0: submodules dir: __TEST_DIR__/Inside/PrintDirs | ||
LOG elab:0: build dir: __TEST_DIR__/build | ||
|
||
--- Simple reads and writes --- | ||
1/1: Building SimpleRW (src/SimpleRW.idr) | ||
LOG elab:0: reading existentToRead: | ||
LOG elab:0: contents: | ||
existent to read | ||
second line | ||
|
||
LOG elab:0: reading nonExistentToRead: | ||
LOG elab:0: FILE DOES NOT EXIST | ||
LOG elab:0: written to existentToWrite | ||
LOG elab:0: written to nonExistentToWrite | ||
existent to read | ||
second line | ||
cat: src/nonExistentToRead: No such file or directory | ||
WRITTEN CONTENTS | ||
LA-LA-LA | ||
WRITTEN CONTENTS | ||
LA-LA-LA | ||
|
||
--- A little but less simple reads and writes --- | ||
1/1: Building LessSimpleRW (src/LessSimpleRW.idr) | ||
LOG elab:0: written to nonExistentOriginally/a-generated-file | ||
LOG elab:0: reading nonExistentOriginally/../nonExistentOriginally/a-generated-file: | ||
LOG elab:0: contents: | ||
WRITTEN CONTENTS | ||
LA-LA-LA | ||
|
||
LOG elab:0: written to ..a-dot-named-file | ||
WRITTEN CONTENTS | ||
LA-LA-LA | ||
WRITTEN CONTENTS | ||
LA-LA-LA | ||
|
||
--- Type providers --- | ||
1/1: Building TypeProviders (src/TypeProviders.idr) | ||
Derived: | ||
{"veryStringField":"String","veryIntegerField":"Integer","varyNatField":"Prelude.Types.Nat"} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,77 @@ | ||
. ../../../testutils.sh | ||
|
||
echo "--- Print dirs with ipkg ---" | ||
check --find-ipkg src/Inside/PrintDirs.idr | filter_test_dir | ||
|
||
############################## | ||
|
||
echo | ||
. ../../../testutils.sh | ||
|
||
( | ||
cd src | ||
echo "--- Print dirs with ipkg (with changed pwd) ---" | ||
check --find-ipkg Inside/PrintDirs.idr | filter_test_dir | ||
) | ||
|
||
############################## | ||
|
||
echo | ||
|
||
( | ||
cd src | ||
. ../../../../testutils.sh # this is here because we will pollute with `build` dir here | ||
echo "--- Print dirs without ipkg (with changed pwd) ---" | ||
check Inside/PrintDirs.idr | filter_test_dir | ||
) | ||
|
||
############################## | ||
|
||
echo | ||
. ../../../testutils.sh | ||
|
||
echo "--- Simple reads and writes ---" | ||
|
||
rm -rf src/nonExistent* | ||
echo "non-overwritten existent to write" > src/existentToWrite | ||
|
||
check --find-ipkg src/SimpleRW.idr | ||
|
||
cat src/existentToRead | ||
cat src/nonExistentToRead 2>&1 | ||
cat src/existentToWrite | ||
cat src/nonExistentToWrite 2>&1 | ||
|
||
rm -rf src/nonExistent* | ||
echo "non-overwritten existent to write" > src/existentToWrite | ||
|
||
############################## | ||
|
||
echo | ||
. ../../../testutils.sh | ||
|
||
echo "--- A little but less simple reads and writes ---" | ||
|
||
rm -rf src/nonExistent* | ||
rm -f src/..a-dot-named-file | ||
|
||
check --find-ipkg src/LessSimpleRW.idr | ||
|
||
cat src/nonExistentOriginally/a-generated-file 2>&1 | ||
cat src/..a-dot-named-file 2>&1 | ||
|
||
rm -rf src/nonExistent* | ||
rm -f src/..a-dot-named-file | ||
|
||
############################## | ||
|
||
echo | ||
. ../../../testutils.sh | ||
|
||
echo "--- Type providers ---" | ||
rm -rf src/another-fancy-record.json | ||
check --find-ipkg src/TypeProviders.idr | ||
|
||
echo "Derived:" | ||
cat src/another-fancy-record.json | ||
echo |
19 changes: 19 additions & 0 deletions
19
tests/idris2/reflection/reflection024/src/Inside/PrintDirs.idr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
module Inside.PrintDirs | ||
|
||
import Language.Reflection | ||
|
||
dirs : List (String, LookupDir) | ||
dirs = | ||
[ ("project dir" , ProjectDir ) | ||
, ("source dir" , SourceDir ) | ||
, ("current module dir", CurrentModuleDir) | ||
, ("submodules dir" , SubmodulesDir ) | ||
, ("build dir" , BuildDir ) | ||
] | ||
|
||
logAllDirs : Elab () | ||
logAllDirs = for_ dirs $ \(msg, lk) => logMsg "elab" 0 "\{msg}: \{!(idrisDir lk)}" | ||
|
||
%language ElabReflection | ||
|
||
%runElab logAllDirs |
Oops, something went wrong.