From e18b705ad3a903f62262a04bee2a18ce5eb8198d Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Fri, 10 Feb 2023 09:12:25 -0700
Subject: [PATCH] Setup to transition to lean 4.

---
 .gitignore     |  5 ++---
 Bookshelf.lean |  1 +
 Main.lean      |  4 ++++
 lakefile.lean  | 15 +++++++++++++++
 lean-toolchain |  1 +
 leanpkg.toml   |  8 --------
 6 files changed, 23 insertions(+), 11 deletions(-)
 create mode 100644 Bookshelf.lean
 create mode 100644 Main.lean
 create mode 100644 lakefile.lean
 create mode 100644 lean-toolchain
 delete mode 100644 leanpkg.toml

diff --git a/.gitignore b/.gitignore
index 1cb9f3c..20c60d7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,2 @@
-*.olean
-/_target
-/leanpkg.path
+/build
+/lake-packages/*
diff --git a/Bookshelf.lean b/Bookshelf.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/Bookshelf.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..e60cc2b
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,4 @@
+import «Bookshelf»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..86589d0
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+package «bookshelf» {
+  -- add package configuration options here
+}
+
+lean_lib «Bookshelf» {
+  -- add library configuration options here
+}
+
+@[default_target]
+lean_exe «bookshelf» {
+  root := `Main
+}
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..5bf01da
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-02-10
diff --git a/leanpkg.toml b/leanpkg.toml
deleted file mode 100644
index 17b4e4c..0000000
--- a/leanpkg.toml
+++ /dev/null
@@ -1,8 +0,0 @@
-[package]
-name = "bookshelf"
-version = "0.1"
-lean_version = "leanprover-community/lean:3.50.3"
-path = "src"
-
-[dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "4c19a16e4b705bf135cf9a80ac18fcc99c438514"}