From 14a2ed44226fd1e3351c51b47847fd9d334b88ae Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 3 May 2023 17:37:06 -0600 Subject: [PATCH] Move source into `src` directory. --- README.md | 2 +- lakefile.lean | 1 + Bookshelf.lean => src/Bookshelf.lean | 0 {Bookshelf => src/Bookshelf}/List.lean | 0 {Bookshelf => src/Bookshelf}/List/Basic.lean | 0 {Bookshelf => src/Bookshelf}/Real.lean | 0 {Bookshelf => src/Bookshelf}/Real/Basic.lean | 0 {Bookshelf => src/Bookshelf}/Real/Rational.lean | 0 {Bookshelf => src/Bookshelf}/Real/Sequence.lean | 0 {Bookshelf => src/Bookshelf}/Real/Sequence.tex | 0 {Bookshelf => src/Bookshelf}/Real/Sequence/Arithmetic.lean | 0 {Bookshelf => src/Bookshelf}/Real/Sequence/Geometric.lean | 0 {Bookshelf => src/Bookshelf}/Real/Set.lean | 0 {Bookshelf => src/Bookshelf}/Real/Set/Basic.lean | 0 {Bookshelf => src/Bookshelf}/Real/Set/Interval.lean | 0 .../FirstCourseAbstractAlgebra.lean | 0 .../FirstCourseAbstractAlgebra}/Fraleigh.lean | 0 .../FirstCourseAbstractAlgebra}/Fraleigh/Chapter1.lean | 0 .../FirstCourseAbstractAlgebra}/README.md | 0 .../MathematicalIntroductionLogic.lean | 0 .../MathematicalIntroductionLogic}/Enderton.lean | 0 .../MathematicalIntroductionLogic}/Enderton/Chapter0.lean | 0 .../MathematicalIntroductionLogic}/Enderton/Chapter0.tex | 0 .../MathematicalIntroductionLogic}/README.md | 0 .../MathematicalIntroductionLogic}/Tuple.lean | 0 .../MathematicalIntroductionLogic}/Tuple/Basic.lean | 0 .../MathematicalIntroductionLogic}/Tuple/Generic.lean | 0 MockMockingbird.lean => src/MockMockingbird.lean | 0 {MockMockingbird => src/MockMockingbird}/Aviary.lean | 0 {MockMockingbird => src/MockMockingbird}/Aviary.tex | 0 OneVariableCalculus.lean => src/OneVariableCalculus.lean | 0 {OneVariableCalculus => src/OneVariableCalculus}/Apostol.lean | 0 .../OneVariableCalculus}/Apostol/Chapter_I_3.lean | 0 .../OneVariableCalculus}/Apostol/Chapter_I_3.tex | 0 .../OneVariableCalculus}/Apostol/Exercises_I_3_12.lean | 0 {OneVariableCalculus => src/OneVariableCalculus}/README.md | 0 {OneVariableCalculus => src/OneVariableCalculus}/Real.lean | 0 .../OneVariableCalculus}/Real/Function.lean | 0 .../OneVariableCalculus}/Real/Function/Step.lean | 0 .../OneVariableCalculus}/Real/Geometry.lean | 0 .../OneVariableCalculus}/Real/Geometry/Area.lean | 0 .../OneVariableCalculus}/Real/Geometry/Basic.lean | 0 .../OneVariableCalculus}/Real/Geometry/Rectangle.lean | 0 {OneVariableCalculus => src/OneVariableCalculus}/Real/Set.lean | 0 .../OneVariableCalculus}/Real/Set/Partition.lean | 0 TheoremProvingInLean.lean => src/TheoremProvingInLean.lean | 0 {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad.lean | 0 .../TheoremProvingInLean}/Avigad/Chapter2.lean | 0 .../TheoremProvingInLean}/Avigad/Chapter3.lean | 0 .../TheoremProvingInLean}/Avigad/Chapter4.lean | 0 .../TheoremProvingInLean}/Avigad/Chapter5.lean | 0 .../TheoremProvingInLean}/Avigad/Chapter7.lean | 0 .../TheoremProvingInLean}/Avigad/Chapter8.lean | 0 {TheoremProvingInLean => src/TheoremProvingInLean}/README.md | 0 54 files changed, 2 insertions(+), 1 deletion(-) rename Bookshelf.lean => src/Bookshelf.lean (100%) rename {Bookshelf => src/Bookshelf}/List.lean (100%) rename {Bookshelf => src/Bookshelf}/List/Basic.lean (100%) rename {Bookshelf => src/Bookshelf}/Real.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Basic.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Rational.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Sequence.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Sequence.tex (100%) rename {Bookshelf => src/Bookshelf}/Real/Sequence/Arithmetic.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Sequence/Geometric.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Set.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Set/Basic.lean (100%) rename {Bookshelf => src/Bookshelf}/Real/Set/Interval.lean (100%) rename FirstCourseAbstractAlgebra.lean => src/FirstCourseAbstractAlgebra.lean (100%) rename {FirstCourseAbstractAlgebra => src/FirstCourseAbstractAlgebra}/Fraleigh.lean (100%) rename {FirstCourseAbstractAlgebra => src/FirstCourseAbstractAlgebra}/Fraleigh/Chapter1.lean (100%) rename {FirstCourseAbstractAlgebra => src/FirstCourseAbstractAlgebra}/README.md (100%) rename MathematicalIntroductionLogic.lean => src/MathematicalIntroductionLogic.lean (100%) rename {MathematicalIntroductionLogic => src/MathematicalIntroductionLogic}/Enderton.lean (100%) rename {MathematicalIntroductionLogic => src/MathematicalIntroductionLogic}/Enderton/Chapter0.lean (100%) rename {MathematicalIntroductionLogic => src/MathematicalIntroductionLogic}/Enderton/Chapter0.tex (100%) rename {MathematicalIntroductionLogic => src/MathematicalIntroductionLogic}/README.md (100%) rename {MathematicalIntroductionLogic => src/MathematicalIntroductionLogic}/Tuple.lean (100%) rename {MathematicalIntroductionLogic => src/MathematicalIntroductionLogic}/Tuple/Basic.lean (100%) rename {MathematicalIntroductionLogic => src/MathematicalIntroductionLogic}/Tuple/Generic.lean (100%) rename MockMockingbird.lean => src/MockMockingbird.lean (100%) rename {MockMockingbird => src/MockMockingbird}/Aviary.lean (100%) rename {MockMockingbird => src/MockMockingbird}/Aviary.tex (100%) rename OneVariableCalculus.lean => src/OneVariableCalculus.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Apostol.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Apostol/Chapter_I_3.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Apostol/Chapter_I_3.tex (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Apostol/Exercises_I_3_12.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/README.md (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Function.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Function/Step.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Geometry.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Geometry/Area.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Geometry/Basic.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Geometry/Rectangle.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Set.lean (100%) rename {OneVariableCalculus => src/OneVariableCalculus}/Real/Set/Partition.lean (100%) rename TheoremProvingInLean.lean => src/TheoremProvingInLean.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad/Chapter2.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad/Chapter3.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad/Chapter4.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad/Chapter5.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad/Chapter7.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/Avigad/Chapter8.lean (100%) rename {TheoremProvingInLean => src/TheoremProvingInLean}/README.md (100%) diff --git a/README.md b/README.md index 4b59f05..b1116ee 100644 --- a/README.md +++ b/README.md @@ -36,5 +36,5 @@ project, first install the following: Afterward, you can generate the necessary HTML via: ```bash -> find . -name '*.tex' | grep -v preamble | xargs -I {} make4ht -e build.mk4 {} +> find . -name '*.tex' | grep -v preamble | xargs -n 1 make4ht -e build.mk4 ``` diff --git a/lakefile.lean b/lakefile.lean index c29a406..26a5182 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,6 +16,7 @@ require «doc-gen4» from git @[default_target] lean_lib «Bookshelf» { + srcDir := "src", roots := #[ `Bookshelf, `FirstCourseAbstractAlgebra, diff --git a/Bookshelf.lean b/src/Bookshelf.lean similarity index 100% rename from Bookshelf.lean rename to src/Bookshelf.lean diff --git a/Bookshelf/List.lean b/src/Bookshelf/List.lean similarity index 100% rename from Bookshelf/List.lean rename to src/Bookshelf/List.lean diff --git a/Bookshelf/List/Basic.lean b/src/Bookshelf/List/Basic.lean similarity index 100% rename from Bookshelf/List/Basic.lean rename to src/Bookshelf/List/Basic.lean diff --git a/Bookshelf/Real.lean b/src/Bookshelf/Real.lean similarity index 100% rename from Bookshelf/Real.lean rename to src/Bookshelf/Real.lean diff --git a/Bookshelf/Real/Basic.lean b/src/Bookshelf/Real/Basic.lean similarity index 100% rename from Bookshelf/Real/Basic.lean rename to src/Bookshelf/Real/Basic.lean diff --git a/Bookshelf/Real/Rational.lean b/src/Bookshelf/Real/Rational.lean similarity index 100% rename from Bookshelf/Real/Rational.lean rename to src/Bookshelf/Real/Rational.lean diff --git a/Bookshelf/Real/Sequence.lean b/src/Bookshelf/Real/Sequence.lean similarity index 100% rename from Bookshelf/Real/Sequence.lean rename to src/Bookshelf/Real/Sequence.lean diff --git a/Bookshelf/Real/Sequence.tex b/src/Bookshelf/Real/Sequence.tex similarity index 100% rename from Bookshelf/Real/Sequence.tex rename to src/Bookshelf/Real/Sequence.tex diff --git a/Bookshelf/Real/Sequence/Arithmetic.lean b/src/Bookshelf/Real/Sequence/Arithmetic.lean similarity index 100% rename from Bookshelf/Real/Sequence/Arithmetic.lean rename to src/Bookshelf/Real/Sequence/Arithmetic.lean diff --git a/Bookshelf/Real/Sequence/Geometric.lean b/src/Bookshelf/Real/Sequence/Geometric.lean similarity index 100% rename from Bookshelf/Real/Sequence/Geometric.lean rename to src/Bookshelf/Real/Sequence/Geometric.lean diff --git a/Bookshelf/Real/Set.lean b/src/Bookshelf/Real/Set.lean similarity index 100% rename from Bookshelf/Real/Set.lean rename to src/Bookshelf/Real/Set.lean diff --git a/Bookshelf/Real/Set/Basic.lean b/src/Bookshelf/Real/Set/Basic.lean similarity index 100% rename from Bookshelf/Real/Set/Basic.lean rename to src/Bookshelf/Real/Set/Basic.lean diff --git a/Bookshelf/Real/Set/Interval.lean b/src/Bookshelf/Real/Set/Interval.lean similarity index 100% rename from Bookshelf/Real/Set/Interval.lean rename to src/Bookshelf/Real/Set/Interval.lean diff --git a/FirstCourseAbstractAlgebra.lean b/src/FirstCourseAbstractAlgebra.lean similarity index 100% rename from FirstCourseAbstractAlgebra.lean rename to src/FirstCourseAbstractAlgebra.lean diff --git a/FirstCourseAbstractAlgebra/Fraleigh.lean b/src/FirstCourseAbstractAlgebra/Fraleigh.lean similarity index 100% rename from FirstCourseAbstractAlgebra/Fraleigh.lean rename to src/FirstCourseAbstractAlgebra/Fraleigh.lean diff --git a/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean b/src/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean similarity index 100% rename from FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean rename to src/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean diff --git a/FirstCourseAbstractAlgebra/README.md b/src/FirstCourseAbstractAlgebra/README.md similarity index 100% rename from FirstCourseAbstractAlgebra/README.md rename to src/FirstCourseAbstractAlgebra/README.md diff --git a/MathematicalIntroductionLogic.lean b/src/MathematicalIntroductionLogic.lean similarity index 100% rename from MathematicalIntroductionLogic.lean rename to src/MathematicalIntroductionLogic.lean diff --git a/MathematicalIntroductionLogic/Enderton.lean b/src/MathematicalIntroductionLogic/Enderton.lean similarity index 100% rename from MathematicalIntroductionLogic/Enderton.lean rename to src/MathematicalIntroductionLogic/Enderton.lean diff --git a/MathematicalIntroductionLogic/Enderton/Chapter0.lean b/src/MathematicalIntroductionLogic/Enderton/Chapter0.lean similarity index 100% rename from MathematicalIntroductionLogic/Enderton/Chapter0.lean rename to src/MathematicalIntroductionLogic/Enderton/Chapter0.lean diff --git a/MathematicalIntroductionLogic/Enderton/Chapter0.tex b/src/MathematicalIntroductionLogic/Enderton/Chapter0.tex similarity index 100% rename from MathematicalIntroductionLogic/Enderton/Chapter0.tex rename to src/MathematicalIntroductionLogic/Enderton/Chapter0.tex diff --git a/MathematicalIntroductionLogic/README.md b/src/MathematicalIntroductionLogic/README.md similarity index 100% rename from MathematicalIntroductionLogic/README.md rename to src/MathematicalIntroductionLogic/README.md diff --git a/MathematicalIntroductionLogic/Tuple.lean b/src/MathematicalIntroductionLogic/Tuple.lean similarity index 100% rename from MathematicalIntroductionLogic/Tuple.lean rename to src/MathematicalIntroductionLogic/Tuple.lean diff --git a/MathematicalIntroductionLogic/Tuple/Basic.lean b/src/MathematicalIntroductionLogic/Tuple/Basic.lean similarity index 100% rename from MathematicalIntroductionLogic/Tuple/Basic.lean rename to src/MathematicalIntroductionLogic/Tuple/Basic.lean diff --git a/MathematicalIntroductionLogic/Tuple/Generic.lean b/src/MathematicalIntroductionLogic/Tuple/Generic.lean similarity index 100% rename from MathematicalIntroductionLogic/Tuple/Generic.lean rename to src/MathematicalIntroductionLogic/Tuple/Generic.lean diff --git a/MockMockingbird.lean b/src/MockMockingbird.lean similarity index 100% rename from MockMockingbird.lean rename to src/MockMockingbird.lean diff --git a/MockMockingbird/Aviary.lean b/src/MockMockingbird/Aviary.lean similarity index 100% rename from MockMockingbird/Aviary.lean rename to src/MockMockingbird/Aviary.lean diff --git a/MockMockingbird/Aviary.tex b/src/MockMockingbird/Aviary.tex similarity index 100% rename from MockMockingbird/Aviary.tex rename to src/MockMockingbird/Aviary.tex diff --git a/OneVariableCalculus.lean b/src/OneVariableCalculus.lean similarity index 100% rename from OneVariableCalculus.lean rename to src/OneVariableCalculus.lean diff --git a/OneVariableCalculus/Apostol.lean b/src/OneVariableCalculus/Apostol.lean similarity index 100% rename from OneVariableCalculus/Apostol.lean rename to src/OneVariableCalculus/Apostol.lean diff --git a/OneVariableCalculus/Apostol/Chapter_I_3.lean b/src/OneVariableCalculus/Apostol/Chapter_I_3.lean similarity index 100% rename from OneVariableCalculus/Apostol/Chapter_I_3.lean rename to src/OneVariableCalculus/Apostol/Chapter_I_3.lean diff --git a/OneVariableCalculus/Apostol/Chapter_I_3.tex b/src/OneVariableCalculus/Apostol/Chapter_I_3.tex similarity index 100% rename from OneVariableCalculus/Apostol/Chapter_I_3.tex rename to src/OneVariableCalculus/Apostol/Chapter_I_3.tex diff --git a/OneVariableCalculus/Apostol/Exercises_I_3_12.lean b/src/OneVariableCalculus/Apostol/Exercises_I_3_12.lean similarity index 100% rename from OneVariableCalculus/Apostol/Exercises_I_3_12.lean rename to src/OneVariableCalculus/Apostol/Exercises_I_3_12.lean diff --git a/OneVariableCalculus/README.md b/src/OneVariableCalculus/README.md similarity index 100% rename from OneVariableCalculus/README.md rename to src/OneVariableCalculus/README.md diff --git a/OneVariableCalculus/Real.lean b/src/OneVariableCalculus/Real.lean similarity index 100% rename from OneVariableCalculus/Real.lean rename to src/OneVariableCalculus/Real.lean diff --git a/OneVariableCalculus/Real/Function.lean b/src/OneVariableCalculus/Real/Function.lean similarity index 100% rename from OneVariableCalculus/Real/Function.lean rename to src/OneVariableCalculus/Real/Function.lean diff --git a/OneVariableCalculus/Real/Function/Step.lean b/src/OneVariableCalculus/Real/Function/Step.lean similarity index 100% rename from OneVariableCalculus/Real/Function/Step.lean rename to src/OneVariableCalculus/Real/Function/Step.lean diff --git a/OneVariableCalculus/Real/Geometry.lean b/src/OneVariableCalculus/Real/Geometry.lean similarity index 100% rename from OneVariableCalculus/Real/Geometry.lean rename to src/OneVariableCalculus/Real/Geometry.lean diff --git a/OneVariableCalculus/Real/Geometry/Area.lean b/src/OneVariableCalculus/Real/Geometry/Area.lean similarity index 100% rename from OneVariableCalculus/Real/Geometry/Area.lean rename to src/OneVariableCalculus/Real/Geometry/Area.lean diff --git a/OneVariableCalculus/Real/Geometry/Basic.lean b/src/OneVariableCalculus/Real/Geometry/Basic.lean similarity index 100% rename from OneVariableCalculus/Real/Geometry/Basic.lean rename to src/OneVariableCalculus/Real/Geometry/Basic.lean diff --git a/OneVariableCalculus/Real/Geometry/Rectangle.lean b/src/OneVariableCalculus/Real/Geometry/Rectangle.lean similarity index 100% rename from OneVariableCalculus/Real/Geometry/Rectangle.lean rename to src/OneVariableCalculus/Real/Geometry/Rectangle.lean diff --git a/OneVariableCalculus/Real/Set.lean b/src/OneVariableCalculus/Real/Set.lean similarity index 100% rename from OneVariableCalculus/Real/Set.lean rename to src/OneVariableCalculus/Real/Set.lean diff --git a/OneVariableCalculus/Real/Set/Partition.lean b/src/OneVariableCalculus/Real/Set/Partition.lean similarity index 100% rename from OneVariableCalculus/Real/Set/Partition.lean rename to src/OneVariableCalculus/Real/Set/Partition.lean diff --git a/TheoremProvingInLean.lean b/src/TheoremProvingInLean.lean similarity index 100% rename from TheoremProvingInLean.lean rename to src/TheoremProvingInLean.lean diff --git a/TheoremProvingInLean/Avigad.lean b/src/TheoremProvingInLean/Avigad.lean similarity index 100% rename from TheoremProvingInLean/Avigad.lean rename to src/TheoremProvingInLean/Avigad.lean diff --git a/TheoremProvingInLean/Avigad/Chapter2.lean b/src/TheoremProvingInLean/Avigad/Chapter2.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter2.lean rename to src/TheoremProvingInLean/Avigad/Chapter2.lean diff --git a/TheoremProvingInLean/Avigad/Chapter3.lean b/src/TheoremProvingInLean/Avigad/Chapter3.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter3.lean rename to src/TheoremProvingInLean/Avigad/Chapter3.lean diff --git a/TheoremProvingInLean/Avigad/Chapter4.lean b/src/TheoremProvingInLean/Avigad/Chapter4.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter4.lean rename to src/TheoremProvingInLean/Avigad/Chapter4.lean diff --git a/TheoremProvingInLean/Avigad/Chapter5.lean b/src/TheoremProvingInLean/Avigad/Chapter5.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter5.lean rename to src/TheoremProvingInLean/Avigad/Chapter5.lean diff --git a/TheoremProvingInLean/Avigad/Chapter7.lean b/src/TheoremProvingInLean/Avigad/Chapter7.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter7.lean rename to src/TheoremProvingInLean/Avigad/Chapter7.lean diff --git a/TheoremProvingInLean/Avigad/Chapter8.lean b/src/TheoremProvingInLean/Avigad/Chapter8.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter8.lean rename to src/TheoremProvingInLean/Avigad/Chapter8.lean diff --git a/TheoremProvingInLean/README.md b/src/TheoremProvingInLean/README.md similarity index 100% rename from TheoremProvingInLean/README.md rename to src/TheoremProvingInLean/README.md