remove import-all

.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

.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

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",

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