From 8fa943d24d7dc7a42064bd43c65e0b686ebc8a53 Mon Sep 17 00:00:00 2001
From: Mathew Polzin <matt.polzin@gmail.com>
Date: Sun, 2 Jun 2024 16:20:20 -0500
Subject: [PATCH] Add a test for ipkg json dump

---
 tests/idris2/pkg/pkg019/expected              |  1 +
 tests/idris2/pkg/pkg019/run                   |  4 ++
 tests/idris2/pkg/pkg019/src/And/A/Proof.idr   |  8 +++
 tests/idris2/pkg/pkg019/src/Main.idr          |  4 ++
 .../pkg/pkg019/src/Yet/Another/Path.idr       |  7 +++
 tests/idris2/pkg/pkg019/test.ipkg             | 49 +++++++++++++++++++
 6 files changed, 73 insertions(+)
 create mode 100644 tests/idris2/pkg/pkg019/expected
 create mode 100755 tests/idris2/pkg/pkg019/run
 create mode 100644 tests/idris2/pkg/pkg019/src/And/A/Proof.idr
 create mode 100644 tests/idris2/pkg/pkg019/src/Main.idr
 create mode 100644 tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr
 create mode 100644 tests/idris2/pkg/pkg019/test.ipkg

diff --git a/tests/idris2/pkg/pkg019/expected b/tests/idris2/pkg/pkg019/expected
new file mode 100644
index 0000000000..71aa7c0efd
--- /dev/null
+++ b/tests/idris2/pkg/pkg019/expected
@@ -0,0 +1 @@
+{"name": "test","depends": [{"contrib": {"lowerInclusive": true,"lowerBound": "*","upperInclusive": true,"upperBound": "*"}},{"idris2": {"lowerInclusive": true,"lowerBound": "0.7.0","upperInclusive": true,"upperBound": "*"}}],"modules": ["And.A.Proof","Yet.Another.Path"],"version": "0.1.0","langversion": {"lowerInclusive": true,"lowerBound": "0.7.0","upperInclusive": true,"upperBound": "*"},"authors": "Average Joe","maintainers": "Average Joe","license": "MIT","brief": "A basic test","readme": "https://github.com/idris-lang/Idris2/README.md","homepage": "https://github.com/idris-lang/Idris2","sourceloc": "https://github.com/idris-lang/Idris2","bugtracker": "https://github.com/idris-lang/Idris2/issues","main": "Main","executable": "test-exec","opts": "--codegen node","sourcedir": "src","builddir": "build","outputdir": "out","prebuild": "make pre","postbuild": "make post","preinstall": "make pre-install","postinstall": "make post-install","preclean": "make pre-clean","postclean": "make post-clean"}
diff --git a/tests/idris2/pkg/pkg019/run b/tests/idris2/pkg/pkg019/run
new file mode 100755
index 0000000000..0c2bed7773
--- /dev/null
+++ b/tests/idris2/pkg/pkg019/run
@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+idris2 --dump-ipkg-json test.ipkg
+
diff --git a/tests/idris2/pkg/pkg019/src/And/A/Proof.idr b/tests/idris2/pkg/pkg019/src/And/A/Proof.idr
new file mode 100644
index 0000000000..744af6dc4d
--- /dev/null
+++ b/tests/idris2/pkg/pkg019/src/And/A/Proof.idr
@@ -0,0 +1,8 @@
+module And.A.Proof
+
+import Yet.Another.Path as Val
+
+%default total
+
+equality : Val.val === 2+3
+equality = Refl
diff --git a/tests/idris2/pkg/pkg019/src/Main.idr b/tests/idris2/pkg/pkg019/src/Main.idr
new file mode 100644
index 0000000000..09b50ac49b
--- /dev/null
+++ b/tests/idris2/pkg/pkg019/src/Main.idr
@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = pure ()
diff --git a/tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr b/tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr
new file mode 100644
index 0000000000..9973d76be2
--- /dev/null
+++ b/tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr
@@ -0,0 +1,7 @@
+module Yet.Another.Path
+
+%default total
+
+public export
+val : Nat
+val = 5
diff --git a/tests/idris2/pkg/pkg019/test.ipkg b/tests/idris2/pkg/pkg019/test.ipkg
new file mode 100644
index 0000000000..7ac761576b
--- /dev/null
+++ b/tests/idris2/pkg/pkg019/test.ipkg
@@ -0,0 +1,49 @@
+package test
+version = 0.1.0
+authors = "Average Joe"
+maintainers = "Average Joe"
+license = "MIT"
+brief = "A basic test"
+readme = "https://github.com/idris-lang/Idris2/README.md"
+homepage = "https://github.com/idris-lang/Idris2"
+sourceloc = "https://github.com/idris-lang/Idris2"
+bugtracker = "https://github.com/idris-lang/Idris2/issues"
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+langversion >= 0.7.0
+
+-- packages to add to search path
+depends = contrib,
+          idris2 >= 0.7.0
+
+-- modules to install
+modules = And.A.Proof,
+          Yet.Another.Path
+
+-- main file (i.e. file to load at REPL)
+main = Main
+
+-- name of executable
+executable = test-exec
+opts = "--codegen node"
+sourcedir = "src"
+builddir = "build"
+outputdir = "out"
+
+-- script to run before building
+prebuild = "make pre"
+
+-- script to run after building
+postbuild = "make post"
+
+-- script to run after building, before installing
+preinstall = "make pre-install"
+
+-- script to run after installing
+postinstall = "make post-install"
+
+-- script to run before cleaning
+preclean = "make pre-clean"
+
+-- script to run after cleaning
+postclean = "make post-clean"