diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index db8f06b..ae4e595 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,9 +25,6 @@ jobs: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain) echo "$HOME/.elan/bin" >> $GITHUB_PATH - - name: Check lib completeness - run: lake exe import_check Src - - name: Cache dependencies uses: actions/cache@v3 with: @@ -36,9 +33,5 @@ jobs: restore-keys: | deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }} - # If you use mathlib, uncomment it out. - # - name: get mathlib cache - # run: lake exe cache get - - name: run 'lake build' run: lake build \ No newline at end of file diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index ed8d19b..b9cfa77 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -38,14 +38,8 @@ jobs: with: mdbook-version: '0.4.32' - - name: run mk-exercise - run: lake exe mk_exercise Src build - - - name: run mdgen - run: lake exe mdgen build md/build - - - name: build by mdbook - run: mdbook build + - name: build + run: lake run build - name: Upload artifact uses: actions/upload-pages-artifact@v2 diff --git a/Src.lean b/Src.lean deleted file mode 100644 index 95f844c..0000000 --- a/Src.lean +++ /dev/null @@ -1,27 +0,0 @@ -import Src.Problem1 -import Src.Problem10 -import Src.Problem11 -import Src.Problem12 -import Src.Problem13 -import Src.Problem14 -import Src.Problem15 -import Src.Problem16 -import Src.Problem17 -import Src.Problem18 -import Src.Problem19 -import Src.Problem2 -import Src.Problem20 -import Src.Problem21 -import Src.Problem22 -import Src.Problem23 -import Src.Problem24 -import Src.Problem3 -import Src.Problem31 -import Src.Problem32 -import Src.Problem4 -import Src.Problem5 -import Src.Problem6 -import Src.Problem7 -import Src.Problem8 -import Src.Problem9 -import Src.README diff --git a/lake-manifest.json b/lake-manifest.json index 68e1862..51e6d29 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,19 +1,10 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/Seasawher/import-all", + [{"url": "https://github.com/Seasawher/mk-exercise", "type": "git", "subDir": null, - "rev": "1fe598ba49253721c558c3ddc85e820c36e876f3", - "name": "«import-all»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/Seasawher/mk-exercise", - "type": "git", - "subDir": null, - "rev": "bbdb1f33a7b132a4dd97deb8ba668705e9555854", + "rev": "4c1fe9cd1874092131861948d2d87bee0741ff91", "name": "«mk-exercise»", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +13,7 @@ {"url": "https://github.com/Seasawher/mdgen", "type": "git", "subDir": null, - "rev": "8f5e2c1145085ac2532d3744696cb1b39582802f", + "rev": "9abb32df39f210d63e164d2fccc106fe96896e0d", "name": "mdgen", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index a749b29..0325e72 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -10,11 +10,9 @@ package «Src» where @[default_target] lean_lib «Src» where + globs := #[.submodules `Src] -- add library configuration options here -require «import-all» from git - "https://github.com/Seasawher/import-all" @ "main" - require «mk-exercise» from git "https://github.com/Seasawher/mk-exercise" @ "main" @@ -34,6 +32,5 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do script build do if ← runCmd "lake" #["exe", "mk_exercise", "Src", "build"] then return 1 if ← runCmd "lake" #["exe", "mdgen", "build", "md/build"] then return 1 - if ← runCmd "lake" #["exe", "import_all", "Src"] then return 1 if ← runCmd "mdbook" #["build"] then return 1 return 0