Use LSpec Nix flake

.github/workflows/ci.yml

@@ -22,14 +22,14 @@ jobs:
         with:
           name: argumentcomputer
           authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-      - name: Patch flake.nix with current commit
+      - name: Patch flake.nix with current commit in template
         run: |
           sed -i 's|github:argumentcomputer/lean4-nix|path:../../|g' flake.nix
-        working-directory : ${{ github.workspace }}/templates/lake-project
+        working-directory : ${{ github.workspace }}/templates/lspec-project
       - run: nix build .#default .#lspec
-        working-directory : ${{ github.workspace }}/templates/lake-project
+        working-directory : ${{ github.workspace }}/templates/lspec-project
       - run: nix run .#lspec
-        working-directory : ${{ github.workspace }}/templates/lake-project
+        working-directory : ${{ github.workspace }}/templates/lspec-project
 
   cache:
     if: github.event_name == 'push' && github.ref == 'refs/heads/main'

templates/lake-project/LakeProject.lean → templates/lspec-project/LSpecProject.lean

@@ -1,4 +1,4 @@
 -- This module serves as the root of the `LakeProject` library.
 -- Import modules here that should be built as part of the library.
-import LakeProject.Basic
-import LakeProject.SubMod.Mod
+import LSpecProject.Basic
+import LSpecProject.SubMod.Mod

templates/lake-project/Main.lean → templates/lspec-project/Main.lean

@@ -1,4 +1,4 @@
-import LakeProject
+import LSpecProject
 
 def main : IO Unit :=
   IO.println s!"{hello}, {world}!"

templates/lake-project/flake.nix → templates/lspec-project/flake.nix

@@ -1,14 +1,14 @@
 {
-  description = "Lean 4 Example Project";
+  description = "Example LSpec Project";
 
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean4-nix.url = "github:argumentcomputer/lean4-nix";
-    # TODO: Add a Nix flake for LSpec so it doesn't have to be rebuilt in each caller
     lspec = {
-      url = "github:argumentcomputer/LSpec?ref=ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec";
-      flake = false;
+      url = "github:argumentcomputer/LSpec";
+      inputs.lean4-nix.follows = "lean4-nix";
+      #rev = "";
     };
   };
 
@@ -30,24 +30,26 @@
       perSystem = {
         system,
         pkgs,
+        self',
         ...
-      }: {
+      }:
+        let
+          lspecLib = (lspec.lib {inherit pkgs lean4-nix;}).lib;
+        in
+      {
         _module.args.pkgs = import nixpkgs {
           inherit system;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
         };
 
-        packages.default = ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-            name = "LakeProject";
-            src = ./.;
-            roots = ["Main" "LakeProject"]; # Add each `lean_lib` as a root
-          }).executable;
-
-        packages.lspec = ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-          name = "LSpec";
-          src = "${lspec}";
-          roots = ["Main" "LSpec"];
+        packages = lspecLib.mkTests ./. // {
+          default = ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+          name = "LSpecProject";
+          src = ./.;
+          roots = ["Main" "LSpecProject"]; # Add each `lean_lib` as a root
         }).executable;
+          lspec = lspecLib.allTests ./.;
+        };
 
         devShells.default = pkgs.mkShell {
           packages = with pkgs.lean; [lean lean-all];

templates/lspec-project/lake-manifest.json

@@ -0,0 +1,20 @@
+{
+  "version": "1.1.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/argumentcomputer/LSpec",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+      "name": "LSpec",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+      "inherited": false,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "LSpecProject",
+  "lakeDir": ".lake"
+}

templates/lake-project/lakefile.lean → templates/lspec-project/lakefile.lean

@@ -13,14 +13,14 @@ lean_exe Tests.Sub
 end Tests
 
 -- NOTE: kebab-case in the package name isn't supported with Nix due to `«»` parsing
-package LakeProject where
+package LSpecProject where
   version := v!"0.1.0"
 
 @[default_target]
-lean_lib «LakeProject» where
+lean_lib «LSpecProject» where
   -- add library configuration options here
 
--- Run with `lake exe lake-project` or `nix run`
+-- Run with `lake exe lspec-project` or `nix run`
 @[default_target]
-lean_exe "lake-project" where
+lean_exe "lspec-project" where
   root := `Main