diff --git a/doc/flake.nix b/doc/flake.nix
index ccf543d48e..70f14cb087 100644
--- a/doc/flake.nix
+++ b/doc/flake.nix
@@ -78,22 +78,27 @@
           (with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
         doCheck = false;
       };
-      renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } ''
-        mkdir -p $(basename $out/${name})
-        alectryon --frontend lean4+markup ${file} --backend webpage -o $out/${name}.md
-      '';
-      listFilesRecursiveRel = root: dir: lib.flatten (lib.mapAttrsToList (name: type:
-        if type == "directory" then
-          listFilesRecursiveRel root ("${dir}/${name}")
-        else
-          dir + "/${name}"
-      ) (builtins.readDir "${root}/${dir}"));
-      renderDir = dir: let
-        inputs = builtins.filter (n: builtins.match ".*\.lean" n != null) (listFilesRecursiveRel dir ".");
-        outputs = lib.genAttrs inputs (n: renderLean n "${dir}/${n}");
-      in
-        outputs // symlinkJoin { inherit name; paths = lib.attrValues outputs; };
-      inked = renderDir ./.;
+      renderLeanMod = mod: mod.overrideAttrs (final: prev: {
+        name = "${prev.name}.md";
+        buildInputs = prev.buildInputs ++ [ alectryon ];
+        outputs = [ "out" ];
+        buildCommand = ''
+          dir=$(dirname $relpath)
+          mkdir -p $dir out/$dir
+          if [ -d $src ]; then cp -r $src/. $dir/; else cp $src $leanPath; fi
+          alectryon --frontend lean4+markup $leanPath --backend webpage -o $out/$leanPath.md
+        '';
+      });
+      renderPackage = pkg: symlinkJoin {
+        name = "${pkg.name}-mds";
+        paths = map renderLeanMod (lib.attrValues pkg.mods);
+      };
+      examples = (buildLeanPackage {
+        name = "examples";
+        src = ./.;
+        roots = [ { mod = "examples"; glob = "submodules"; } ];
+      });
+      inked = renderPackage examples;
       doc = book;
     };
     defaultPackage = self.packages.${system}.doc;
diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index f6ecff0fa7..e72431c70f 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -49,7 +49,7 @@ with builtins; let
       set -u
       ${args.buildCommand}
     '' ];
-  });
+  }) // { overrideAttrs = f: mkBareDerivation (lib.fix (lib.extends f (_: args))); };
   runBareCommand = name: args: buildCommand: mkBareDerivation (args // { inherit name buildCommand; });
   runBareCommandLocal = name: args: buildCommand: runBareCommand name (args // {
     preferLocalBuild = true;
@@ -134,10 +134,10 @@ with builtins; let
     # the only possible references to store paths in the JSON should be inside errors, so no chance of missed dependencies from this
     unsafeDiscardStringContext (readFile "${modDepsFile}/${modDepsFile.name}"));
   modDepsMap = listToAttrs (lib.zipListsWith lib.nameValuePair candidateMods modDeps.imports);
-  maybeOverride = f: x: if f != null then lib.fix (lib.extends f (_: x)) else x;
+  maybeOverrideAttrs = f: x: if f != null then x.overrideAttrs f else x;
   # build module (.olean and .c) given derivations of all (immediate) dependencies
   # TODO: make `rec` parts override-compatible?
-  buildMod = mod: deps: mkBareDerivation (maybeOverride overrideBuildModAttrs rec {
+  buildMod = mod: deps: maybeOverrideAttrs overrideBuildModAttrs (mkBareDerivation rec {
     name = "${mod}";
     LEAN_PATH = depRoot mod deps;
     LEAN_ABORT_ON_PANIC = "1";