-
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.
- Loading branch information
1 parent
875fb65
commit 8fa943d
Showing
6 changed files
with
73 additions
and
0 deletions.
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"} |
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,4 @@ | ||
. ../../../testutils.sh | ||
|
||
idris2 --dump-ipkg-json test.ipkg | ||
|
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,8 @@ | ||
module And.A.Proof | ||
|
||
import Yet.Another.Path as Val | ||
|
||
%default total | ||
|
||
equality : Val.val === 2+3 | ||
equality = Refl |
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,4 @@ | ||
module Main | ||
|
||
main : IO () | ||
main = pure () |
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,7 @@ | ||
module Yet.Another.Path | ||
|
||
%default total | ||
|
||
public export | ||
val : Nat | ||
val = 5 |
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,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" |