aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 8 Pull Requests 2 Packages Projects Releases 1 Wiki Activity

chore: Update Lean4 upstream to unofficial flake #115

Open
aniva wants to merge 3 commits from misc/build into dev
pull from: misc/build
merge into: aniva:dev
Conversation 1 Commits 3 Files Changed 2 +71 -97
2 changed files with 71 additions and 97 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

137
flake.lock
View File

@ -5,11 +5,11 @@
"nixpkgs-lib": "nixpkgs-lib" "nixpkgs-lib": "nixpkgs-lib"
}, },
"locked": { "locked": {
"lastModified": 1709336216, "lastModified": 1727826117,
"narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=", "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
"owner": "hercules-ci", "owner": "hercules-ci",
"repo": "flake-parts", "repo": "flake-parts",
"rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2", "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -18,40 +18,40 @@
"type": "github" "type": "github"
} }
}, },
"flake-utils": { "flake-parts_2": {
"locked": {
"lastModified": 1656928814,
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"lean": {
"inputs": { "inputs": {
"flake-utils": "flake-utils", "nixpkgs-lib": "nixpkgs-lib_2"
"nixpkgs": "nixpkgs",
"nixpkgs-cadical": "nixpkgs-cadical",
"nixpkgs-old": "nixpkgs-old"
}, },
"locked": { "locked": {
"lastModified": 1727749878, "lastModified": 1727826117,
"narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=", "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
"owner": "leanprover", "owner": "hercules-ci",
"repo": "lean4", "repo": "flake-parts",
"rev": "dc2533473114eb8656439ff2b9335209784aa640", "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "leanprover", "owner": "hercules-ci",
"ref": "v4.12.0", "repo": "flake-parts",
"repo": "lean4", "type": "github"
}
},
"lean4-nix": {
"inputs": {
"flake-parts": "flake-parts_2",
"nixpkgs": "nixpkgs"
},
"locked": {
"lastModified": 1729990097,
"narHash": "sha256-3RUciZy/VMbyp9v1f8oba/oQ8bWWVh2+1wsuUah3ryE=",
"owner": "lenianiva",
"repo": "lean4-nix",
"rev": "6919763f186c7b0d39907203a649078ff3a4eb71",
"type": "github"
},
"original": {
"owner": "lenianiva",
"repo": "lean4-nix",
"type": "github" "type": "github"
} }
}, },
@ -74,83 +74,56 @@
}, },
"nixpkgs": { "nixpkgs": {
"locked": { "locked": {
"lastModified": 1686089707, "lastModified": 1728500571,
"narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=", "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=",
"owner": "NixOS", "owner": "nixos",
"repo": "nixpkgs", "repo": "nixpkgs",
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397", "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "NixOS", "owner": "nixos",
"ref": "nixpkgs-unstable", "ref": "nixos-24.05",
"repo": "nixpkgs", "repo": "nixpkgs",
"type": "github" "type": "github"
} }
}, },
"nixpkgs-cadical": {
"locked": {
"lastModified": 1722221733,
"narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
}
},
"nixpkgs-lib": { "nixpkgs-lib": {
"locked": { "locked": {
"dir": "lib", "lastModified": 1727825735,
"lastModified": 1709237383, "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
"narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=", "type": "tarball",
"owner": "NixOS", "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
"repo": "nixpkgs",
"rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
"type": "github"
}, },
"original": { "original": {
"dir": "lib", "type": "tarball",
"owner": "NixOS", "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
} }
}, },
"nixpkgs-old": { "nixpkgs-lib_2": {
"flake": false,
"locked": { "locked": {
"lastModified": 1581379743, "lastModified": 1727825735,
"narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=", "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
"owner": "NixOS", "type": "tarball",
"repo": "nixpkgs", "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
"rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
"type": "github"
}, },
"original": { "original": {
"owner": "NixOS", "type": "tarball",
"ref": "nixos-19.03", "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
"repo": "nixpkgs",
"type": "github"
} }
}, },
"nixpkgs_2": { "nixpkgs_2": {
"locked": { "locked": {
"lastModified": 1711703276, "lastModified": 1729691686,
"narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=", "narHash": "sha256-BAuPWW+9fa1moZTU+jFh+1cUtmsuF8asgzFwejM4wac=",
"owner": "nixos", "owner": "nixos",
"repo": "nixpkgs", "repo": "nixpkgs",
"rev": "d8fe5e6c92d0d190646fb9f1056741a229980089", "rev": "32e940c7c420600ef0d1ef396dc63b04ee9cad37",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "nixos", "owner": "nixos",
"ref": "nixos-unstable", "ref": "nixos-24.05",
"repo": "nixpkgs", "repo": "nixpkgs",
"type": "github" "type": "github"
} }
@ -158,7 +131,7 @@
"root": { "root": {
"inputs": { "inputs": {
"flake-parts": "flake-parts", "flake-parts": "flake-parts",
"lean": "lean", "lean4-nix": "lean4-nix",
"lspec": "lspec", "lspec": "lspec",
"nixpkgs": "nixpkgs_2" "nixpkgs": "nixpkgs_2"
} }

31
flake.nix
View File

@ -2,12 +2,9 @@
description = "Pantograph"; description = "Pantograph";
inputs = { inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
flake-parts.url = "github:hercules-ci/flake-parts"; flake-parts.url = "github:hercules-ci/flake-parts";
lean = { lean4-nix.url = "github:lenianiva/lean4-nix";
# Do not follow input's nixpkgs since it could cause build failures
url = "github:leanprover/lean4?ref=v4.12.0";
};
lspec = { lspec = {
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab"; url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
flake = false; flake = false;
@ -18,7 +15,7 @@
self, self,
nixpkgs, nixpkgs,
flake-parts, flake-parts,
lean, lean4-nix,
lspec, lspec,
... ...
} : flake-parts.lib.mkFlake { inherit inputs; } { } : flake-parts.lib.mkFlake { inherit inputs; } {
@ -29,13 +26,16 @@
"x86_64-darwin" "x86_64-darwin"
]; ];
perSystem = { system, pkgs, ... }: let perSystem = { system, pkgs, ... }: let
leanPkgs = lean.packages.${system}.deprecated; pkgs = import nixpkgs {
lspecLib = leanPkgs.buildLeanPackage { inherit system;
overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
};
lspecLib = pkgs.lean.buildLeanPackage {
name = "LSpec"; name = "LSpec";
roots = [ "Main" "LSpec" ]; roots = [ "Main" "LSpec" ];
src = "${lspec}"; src = "${lspec}";
}; };
project = leanPkgs.buildLeanPackage { project = pkgs.lean.buildLeanPackage {
name = "Pantograph"; name = "Pantograph";
roots = [ "Pantograph" ]; roots = [ "Pantograph" ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
@ -46,7 +46,7 @@
!(pkgs.lib.hasSuffix "Repl.lean" path); !(pkgs.lib.hasSuffix "Repl.lean" path);
}); });
}; };
repl = leanPkgs.buildLeanPackage { repl = pkgs.lean.buildLeanPackage {
name = "Repl"; name = "Repl";
roots = [ "Main" "Repl" ]; roots = [ "Main" "Repl" ];
deps = [ project ]; deps = [ project ];
@ -57,7 +57,7 @@
!(pkgs.lib.hasSuffix ".md" path); !(pkgs.lib.hasSuffix ".md" path);
}); });
}; };
test = leanPkgs.buildLeanPackage { test = pkgs.lean.buildLeanPackage {
name = "Test"; name = "Test";
# NOTE: The src directory must be ./. since that is where the import # NOTE: The src directory must be ./. since that is where the import
# root begins (e.g. `import Test.Environment` and not `import # root begins (e.g. `import Test.Environment` and not `import
@ -72,24 +72,25 @@
}; };
in rec { in rec {
packages = { packages = {
inherit (leanPkgs) lean lean-all; inherit (pkgs.lean) lean lean-all;
inherit (project) sharedLib; inherit (project) sharedLib;
inherit (repl) executable; inherit (repl) executable;
default = repl.executable; default = repl.executable;
}; };
legacyPackages = { legacyPackages = {
inherit project leanPkgs; inherit project;
leanPkgs = pkgs.lean;
}; };
checks = { checks = {
test = pkgs.runCommand "test" { test = pkgs.runCommand "test" {
buildInputs = [ test.executable leanPkgs.lean-all ]; buildInputs = [ test.executable pkgs.lean.lean-all ];
} '' } ''
#export LEAN_SRC_PATH="${./.}" #export LEAN_SRC_PATH="${./.}"
${test.executable}/bin/test > $out ${test.executable}/bin/test > $out
''; '';
}; };
devShells.default = pkgs.mkShell { devShells.default = pkgs.mkShell {
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ]; buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
}; };
}; };
}; };