From e607a0efb049c9a67d4d7a710105c11741a01743 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 20 Feb 2023 13:26:18 -0700 Subject: [PATCH] Break books into separate Lean projects. --- .gitignore | 9 +++++---- Bookshelf.lean | 2 -- .../TheoremProvingInLean.lean | 6 ++++++ .../TheoremProvingInLean/Exercises2.lean | 0 .../TheoremProvingInLean/Exercises3.lean | 0 .../TheoremProvingInLean/Exercises4.lean | 0 .../TheoremProvingInLean/Exercises5.lean | 0 .../TheoremProvingInLean/Exercises7.lean | 0 .../TheoremProvingInLean/Exercises8.lean | 0 .../theorem-proving-in-lean/lake-manifest.json | 1 + bookshelf/theorem-proving-in-lean/lakefile.lean | 7 +++++++ .../theorem-proving-in-lean/lean-toolchain | 0 common/Sequence.lean | 2 ++ {Bookshelf => common}/Sequence/Arithmetic.lean | 0 {Bookshelf => common}/Sequence/Geometric.lean | 0 lake-manifest.json => common/lake-manifest.json | 2 +- common/lakefile.lean | 12 ++++++++++++ common/lean-toolchain | 1 + lakefile.lean | 14 -------------- 19 files changed, 35 insertions(+), 21 deletions(-) delete mode 100644 Bookshelf.lean create mode 100644 bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean rename exercises/theorem-proving-in-lean/exercises-2.lean => bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean (100%) rename exercises/theorem-proving-in-lean/exercises-3.lean => bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean (100%) rename exercises/theorem-proving-in-lean/exercises-4.lean => bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean (100%) rename exercises/theorem-proving-in-lean/exercises-5.lean => bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean (100%) rename exercises/theorem-proving-in-lean/exercises-7.lean => bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean (100%) rename exercises/theorem-proving-in-lean/exercises-8.lean => bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean (100%) create mode 100644 bookshelf/theorem-proving-in-lean/lake-manifest.json create mode 100644 bookshelf/theorem-proving-in-lean/lakefile.lean rename lean-toolchain => bookshelf/theorem-proving-in-lean/lean-toolchain (100%) create mode 100644 common/Sequence.lean rename {Bookshelf => common}/Sequence/Arithmetic.lean (100%) rename {Bookshelf => common}/Sequence/Geometric.lean (100%) rename lake-manifest.json => common/lake-manifest.json (93%) create mode 100644 common/lakefile.lean create mode 100644 common/lean-toolchain delete mode 100644 lakefile.lean diff --git a/.gitignore b/.gitignore index 30bf676..6e543ec 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ -/build -/lake-packages/* -/_target -/leanpkg.path +# Lean +**/build +**/lake-packages/* +**/_target +**/leanpkg.path diff --git a/Bookshelf.lean b/Bookshelf.lean deleted file mode 100644 index 037efd7..0000000 --- a/Bookshelf.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Bookshelf.Sequence.Arithmetic -import Bookshelf.Sequence.Geometric diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean new file mode 100644 index 0000000..277ec5e --- /dev/null +++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean @@ -0,0 +1,6 @@ +import TheoremProvingInLean.Exercises2 +import TheoremProvingInLean.Exercises3 +import TheoremProvingInLean.Exercises4 +import TheoremProvingInLean.Exercises5 +import TheoremProvingInLean.Exercises7 +import TheoremProvingInLean.Exercises8 \ No newline at end of file diff --git a/exercises/theorem-proving-in-lean/exercises-2.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-2.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean diff --git a/exercises/theorem-proving-in-lean/exercises-3.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-3.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean diff --git a/exercises/theorem-proving-in-lean/exercises-4.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-4.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean diff --git a/exercises/theorem-proving-in-lean/exercises-5.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-5.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean diff --git a/exercises/theorem-proving-in-lean/exercises-7.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-7.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean diff --git a/exercises/theorem-proving-in-lean/exercises-8.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-8.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean diff --git a/bookshelf/theorem-proving-in-lean/lake-manifest.json b/bookshelf/theorem-proving-in-lean/lake-manifest.json new file mode 100644 index 0000000..1e31dae --- /dev/null +++ b/bookshelf/theorem-proving-in-lean/lake-manifest.json @@ -0,0 +1 @@ +{"version": 4, "packagesDir": "lake-packages", "packages": []} diff --git a/bookshelf/theorem-proving-in-lean/lakefile.lean b/bookshelf/theorem-proving-in-lean/lakefile.lean new file mode 100644 index 0000000..d989b0a --- /dev/null +++ b/bookshelf/theorem-proving-in-lean/lakefile.lean @@ -0,0 +1,7 @@ +import Lake +open Lake DSL + +package «theorem-proving-in-lean» + +@[default_target] +lean_lib «TheoremProvingInLean» diff --git a/lean-toolchain b/bookshelf/theorem-proving-in-lean/lean-toolchain similarity index 100% rename from lean-toolchain rename to bookshelf/theorem-proving-in-lean/lean-toolchain diff --git a/common/Sequence.lean b/common/Sequence.lean new file mode 100644 index 0000000..a56ac94 --- /dev/null +++ b/common/Sequence.lean @@ -0,0 +1,2 @@ +import Sequence.Arithmetic +import Sequence.Geometric \ No newline at end of file diff --git a/Bookshelf/Sequence/Arithmetic.lean b/common/Sequence/Arithmetic.lean similarity index 100% rename from Bookshelf/Sequence/Arithmetic.lean rename to common/Sequence/Arithmetic.lean diff --git a/Bookshelf/Sequence/Geometric.lean b/common/Sequence/Geometric.lean similarity index 100% rename from Bookshelf/Sequence/Geometric.lean rename to common/Sequence/Geometric.lean diff --git a/lake-manifest.json b/common/lake-manifest.json similarity index 93% rename from lake-manifest.json rename to common/lake-manifest.json index fe3e9de..d02be76 100644 --- a/lake-manifest.json +++ b/common/lake-manifest.json @@ -4,7 +4,7 @@ [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "065e9956724008d1059577700fd676eaf25f35d5", + "rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87", "name": "mathlib", "inputRev?": null}}, {"git": diff --git a/common/lakefile.lean b/common/lakefile.lean new file mode 100644 index 0000000..b27615a --- /dev/null +++ b/common/lakefile.lean @@ -0,0 +1,12 @@ +import Lake +open Lake DSL + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" + +package «Common» + +@[default_target] +lean_lib «Common» { + roots := #["Sequence"] +} diff --git a/common/lean-toolchain b/common/lean-toolchain new file mode 100644 index 0000000..5bf01da --- /dev/null +++ b/common/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-02-10 diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 index 3d0e994..0000000 --- a/lakefile.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Lake -open Lake DSL - -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" - -package «bookshelf» { - -- add package configuration options here -} - -@[default_target] -lean_lib «Bookshelf» { - -- add library configuration options here -}