From 2ec35b48a615741aa4cc98e148d7e92ee1ea7c31 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 26 Oct 2024 22:20:45 -0700
Subject: [PATCH 1/2] doc: Fix minimal version, and add toolchain file

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 878cad8..8f03b66 100644
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@ nix flake new --template github:lenianiva/lean4-nix#dependency ./dependency
 ### Overlay
 
 The user must decide on a Lean version to use as overlay. The minimal supported
-version is `v4.12.0`, since it is the version when Lean's official Nix flake was
+version is `v4.11.0`, since it is the version when Lean's official Nix flake was
 deprecated. There are a couple of ways to get an overlay. Each corresponds to a
 flake output:
 
@@ -45,7 +45,7 @@ Then apply the overlay on `pkgs`:
 ```nix
 pkgs = import nixpkgs {
   inherit system;
-  overlays = [ lean4-nix.tags."v4.12.0" ];
+  overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
 };
 ```
 and `pkgs.lean` will be replaced by the chosen overlay.

From 0aa50a8ebb3f8cbb8bafd345d99abb3fdf3b8b16 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 2 Feb 2025 10:37:21 -0800
Subject: [PATCH 2/2] doc: Add `lakefile.toml` example

---
 templates/minimal/lake-manifest.json | 2 +-
 templates/minimal/lakefile.toml      | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 templates/minimal/lakefile.toml

diff --git a/templates/minimal/lake-manifest.json b/templates/minimal/lake-manifest.json
index 767660f..4af8c5f 100644
--- a/templates/minimal/lake-manifest.json
+++ b/templates/minimal/lake-manifest.json
@@ -1,5 +1,5 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
- "name": "template",
+ "name": "Minimal",
  "lakeDir": ".lake"}
diff --git a/templates/minimal/lakefile.toml b/templates/minimal/lakefile.toml
new file mode 100644
index 0000000..1ed85e4
--- /dev/null
+++ b/templates/minimal/lakefile.toml
@@ -0,0 +1,7 @@
+name = "Minimal"
+version = "0.1.0"
+defaultTargets = ["minimal"]
+
+[[lean_exe]]
+name = "minimal"
+root = "Main"