diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5931fbd..94b3e2d 100644 --- a/.github/workflows/ci.yml +++ b/.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' diff --git a/templates/dependency/flake.lock b/templates/dependency/flake.lock index c1e0761..a706921 100644 --- a/templates/dependency/flake.lock +++ b/templates/dependency/flake.lock @@ -42,18 +42,14 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1740001283, - "narHash": "sha256-yAMMF71Mb9I/gxFSuqWB0ExAQO5I9xsL+g99LRSEAaI=", - "owner": "argumentcomputer", - "repo": "lean4-nix", - "rev": "056fc0260b4d5a66fdcc945d7ca56013cf2aee1d", - "type": "github" + "path": "../../", + "type": "path" }, "original": { - "owner": "argumentcomputer", - "repo": "lean4-nix", - "type": "github" - } + "path": "../../", + "type": "path" + }, + "parent": [] }, "nixpkgs": { "locked": { diff --git a/templates/lake-project/README.md b/templates/lake-project/README.md deleted file mode 100644 index 789c387..0000000 --- a/templates/lake-project/README.md +++ /dev/null @@ -1 +0,0 @@ -# lake-project \ No newline at end of file diff --git a/templates/lake-project/lake-manifest.json b/templates/lake-project/lake-manifest.json deleted file mode 100644 index 1cc6ce1..0000000 --- a/templates/lake-project/lake-manifest.json +++ /dev/null @@ -1,15 +0,0 @@ -{"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": "LakeProject", - "lakeDir": ".lake"} diff --git a/templates/lake-project/LakeProject.lean b/templates/lspec-project/LSpecProject.lean similarity index 69% rename from templates/lake-project/LakeProject.lean rename to templates/lspec-project/LSpecProject.lean index 20d434d..09ae5ad 100644 --- a/templates/lake-project/LakeProject.lean +++ b/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 diff --git a/templates/lake-project/LakeProject/Basic.lean b/templates/lspec-project/LSpecProject/Basic.lean similarity index 100% rename from templates/lake-project/LakeProject/Basic.lean rename to templates/lspec-project/LSpecProject/Basic.lean diff --git a/templates/lake-project/LakeProject/SubMod/Mod.lean b/templates/lspec-project/LSpecProject/SubMod/Mod.lean similarity index 100% rename from templates/lake-project/LakeProject/SubMod/Mod.lean rename to templates/lspec-project/LSpecProject/SubMod/Mod.lean diff --git a/templates/lake-project/Main.lean b/templates/lspec-project/Main.lean similarity index 74% rename from templates/lake-project/Main.lean rename to templates/lspec-project/Main.lean index 93f3cfd..0495f2a 100644 --- a/templates/lake-project/Main.lean +++ b/templates/lspec-project/Main.lean @@ -1,4 +1,4 @@ -import LakeProject +import LSpecProject def main : IO Unit := IO.println s!"{hello}, {world}!" diff --git a/templates/lake-project/Tests/Add.lean b/templates/lspec-project/Tests/Add.lean similarity index 100% rename from templates/lake-project/Tests/Add.lean rename to templates/lspec-project/Tests/Add.lean diff --git a/templates/lake-project/Tests/Sub.lean b/templates/lspec-project/Tests/Sub.lean similarity index 100% rename from templates/lake-project/Tests/Sub.lean rename to templates/lspec-project/Tests/Sub.lean diff --git a/templates/lake-project/flake.lock b/templates/lspec-project/flake.lock similarity index 59% rename from templates/lake-project/flake.lock rename to templates/lspec-project/flake.lock index c8dc3c2..4a41e4e 100644 --- a/templates/lake-project/flake.lock +++ b/templates/lspec-project/flake.lock @@ -36,36 +36,57 @@ "type": "github" } }, + "flake-parts_3": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib_3" + }, + "locked": { + "lastModified": 1738453229, + "narHash": "sha256-7H9XgNiGLKN1G1CgRh0vUL4AheZSYzPm+zmZ7vxbJdo=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "32ea77a06711b758da0ad9bd6a844c5740a87abd", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, "lean4-nix": { "inputs": { "flake-parts": "flake-parts_2", "nixpkgs": "nixpkgs" }, "locked": { - "path": "../../", + "lastModified": 1740712519, + "narHash": "sha256-K4GhK0D04fthUzR1zw4f19jdR7eVr0ufsVXv3i15mdY=", + "path": "/home/sam/repos/argument/lean4-nix", "type": "path" }, "original": { - "path": "../../", + "path": "/home/sam/repos/argument/lean4-nix", "type": "path" - }, - "parent": [] + } }, "lspec": { - "flake": false, + "inputs": { + "flake-parts": "flake-parts_3", + "lean4-nix": [ + "lean4-nix" + ], + "nixpkgs": "nixpkgs_2" + }, "locked": { - "lastModified": 1738701903, - "narHash": "sha256-nGYQbLHmO1PRgSGUiP1u43gjDa6lbDc60+AoSJZttV4=", - "owner": "argumentcomputer", - "repo": "LSpec", - "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec", - "type": "github" + "lastModified": 1740717353, + "narHash": "sha256-PrRoKSrxwFcH2Ts7UPWmpwxWH2t81Ph18aaj0T9ABQU=", + "path": "/home/sam/repos/argument/LSpec/", + "type": "path" }, "original": { - "owner": "argumentcomputer", - "ref": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec", - "repo": "LSpec", - "type": "github" + "path": "/home/sam/repos/argument/LSpec/", + "type": "path" } }, "nixpkgs": { @@ -108,13 +129,41 @@ "url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz" } }, + "nixpkgs-lib_3": { + "locked": { + "lastModified": 1738452942, + "narHash": "sha256-vJzFZGaCpnmo7I6i416HaBLpC+hvcURh/BQwROcGIp8=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz" + }, + "original": { + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz" + } + }, "nixpkgs_2": { "locked": { - "lastModified": 1739923778, - "narHash": "sha256-BqUY8tz0AQ4to2Z4+uaKczh81zsGZSYxjgvtw+fvIfM=", + "lastModified": 1740463929, + "narHash": "sha256-4Xhu/3aUdCKeLfdteEHMegx5ooKQvwPHNkOgNCXQrvc=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "5d7db4668d7a0c6cc5fc8cf6ef33b008b2b1ed8b", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-24.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_3": { + "locked": { + "lastModified": 1740603184, + "narHash": "sha256-t+VaahjQAWyA+Ctn2idyo1yxRIYpaDxMgHkgCNiMJa4=", "owner": "nixos", "repo": "nixpkgs", - "rev": "36864ed72f234b9540da4cf7a0c49e351d30d3f1", + "rev": "f44bd8ca21e026135061a0a57dcf3d0775b67a49", "type": "github" }, "original": { @@ -129,7 +178,7 @@ "flake-parts": "flake-parts", "lean4-nix": "lean4-nix", "lspec": "lspec", - "nixpkgs": "nixpkgs_2" + "nixpkgs": "nixpkgs_3" } } }, diff --git a/templates/lake-project/flake.nix b/templates/lspec-project/flake.nix similarity index 56% rename from templates/lake-project/flake.nix rename to templates/lspec-project/flake.nix index 8f0e79d..a710f2a 100644 --- a/templates/lake-project/flake.nix +++ b/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]; diff --git a/templates/lspec-project/lake-manifest.json b/templates/lspec-project/lake-manifest.json new file mode 100644 index 0000000..cfd400a --- /dev/null +++ b/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" +} diff --git a/templates/lake-project/lakefile.lean b/templates/lspec-project/lakefile.lean similarity index 76% rename from templates/lake-project/lakefile.lean rename to templates/lspec-project/lakefile.lean index 3b59c30..f1b871e 100644 --- a/templates/lake-project/lakefile.lean +++ b/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 diff --git a/templates/lake-project/lean-toolchain b/templates/lspec-project/lean-toolchain similarity index 100% rename from templates/lake-project/lean-toolchain rename to templates/lspec-project/lean-toolchain