summaryrefslogtreecommitdiff
path: root/tests/lean/misc-external
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/misc-external')
-rw-r--r--tests/lean/misc-external/External.lean1
-rw-r--r--tests/lean/misc-external/External/Types.lean4
-rw-r--r--tests/lean/misc-external/lake-manifest.json27
-rw-r--r--tests/lean/misc-external/lakefile.lean14
-rw-r--r--tests/lean/misc-external/lean-toolchain1
5 files changed, 36 insertions, 11 deletions
diff --git a/tests/lean/misc-external/External.lean b/tests/lean/misc-external/External.lean
new file mode 100644
index 00000000..b95db309
--- /dev/null
+++ b/tests/lean/misc-external/External.lean
@@ -0,0 +1 @@
+import External.Funs
diff --git a/tests/lean/misc-external/External/Types.lean b/tests/lean/misc-external/External/Types.lean
index 386832f4..ed1842be 100644
--- a/tests/lean/misc-external/External/Types.lean
+++ b/tests/lean/misc-external/External/Types.lean
@@ -4,5 +4,7 @@ import Base.Primitives
/- [core::num::nonzero::NonZeroU32] -/
axiom core_num_nonzero_non_zero_u32_t : Type
-/- The state type used in the state-error monad -/ axiom State : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
diff --git a/tests/lean/misc-external/lake-manifest.json b/tests/lean/misc-external/lake-manifest.json
new file mode 100644
index 00000000..57b071ca
--- /dev/null
+++ b/tests/lean/misc-external/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece",
+ "name": "mathlib",
+ "inputRev?": null}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "name": "std",
+ "inputRev?": "main"}}]}
diff --git a/tests/lean/misc-external/lakefile.lean b/tests/lean/misc-external/lakefile.lean
index b883f4b9..6cc4aae4 100644
--- a/tests/lean/misc-external/lakefile.lean
+++ b/tests/lean/misc-external/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «external» {
- -- add package configuration options here
-}
+package «external» {}
-lean_lib «Base» {
- -- add library configuration options here
-}
-
-lean_lib «External» {
- -- add library configuration options here
-}
+lean_lib «Base» {}
+@[default_target]
+lean_lib «External» {}
diff --git a/tests/lean/misc-external/lean-toolchain b/tests/lean/misc-external/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/misc-external/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21