commit d79410bbf5ccfefbfa3356c733ad41ec61135881 Author: pingu Date: Wed Jan 29 23:07:02 2025 +0100 Wooooooo diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..07b65bd --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +/.lake +.direnv +.envrc +.github diff --git a/Example.lean b/Example.lean new file mode 100644 index 0000000..03155d3 --- /dev/null +++ b/Example.lean @@ -0,0 +1,4 @@ +import Aesop + +def main : IO Unit := + IO.println "Cirno's Perfect Arithmetics Class has begun!" diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..2cabf1b --- /dev/null +++ b/flake.lock @@ -0,0 +1,124 @@ +{ + "nodes": { + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1736143030, + "narHash": "sha256-+hu54pAoLDEZT9pjHlqL9DNzWz0NbUn8NEAHP7PQPzU=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "b905f6fc23a9051a6e1b741e1438dbfc0634c6de", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "flake-parts_2": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib_2" + }, + "locked": { + "lastModified": 1727826117, + "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "lean4-nix": { + "inputs": { + "flake-parts": "flake-parts_2", + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1736388194, + "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=", + "owner": "lenianiva", + "repo": "lean4-nix", + "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2", + "type": "github" + }, + "original": { + "owner": "lenianiva", + "repo": "lean4-nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1728500571, + "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-24.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "lastModified": 1735774519, + "narHash": "sha256-CewEm1o2eVAnoqb6Ml+Qi9Gg/EfNAxbRx1lANGVyoLI=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/e9b51731911566bbf7e4895475a87fe06961de0b.tar.gz" + }, + "original": { + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/e9b51731911566bbf7e4895475a87fe06961de0b.tar.gz" + } + }, + "nixpkgs-lib_2": { + "locked": { + "lastModified": 1727825735, + "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" + }, + "original": { + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1737885589, + "narHash": "sha256-Zf0hSrtzaM1DEz8//+Xs51k/wdSajticVrATqDrfQjg=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "852ff1d9e153d8875a83602e03fdef8a63f0ecf8", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-parts": "flake-parts", + "lean4-nix": "lean4-nix", + "nixpkgs": "nixpkgs_2" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..8c5e823 --- /dev/null +++ b/flake.nix @@ -0,0 +1,46 @@ +{ + description = "Lean 4 Example Project"; + + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; + flake-parts.url = "github:hercules-ci/flake-parts"; + lean4-nix.url = "github:lenianiva/lean4-nix"; + }; + + outputs = inputs @ { + nixpkgs, + flake-parts, + lean4-nix, + ... + }: + flake-parts.lib.mkFlake {inherit inputs;} { + systems = [ + "aarch64-darwin" + "aarch64-linux" + "x86_64-darwin" + "x86_64-linux" + ]; + + perSystem = { + system, + pkgs, + ... + }: { + _module.args.pkgs = import nixpkgs { + inherit system; + overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; + }; + + packages.default = + ((lean4-nix.lake {inherit pkgs;}).mkPackage { + src = ./.; + roots = ["Example"]; + }) + .executable; + + devShells.default = pkgs.mkShell { + packages = with pkgs; [ lean4 ]; + }; + }; + }; +} diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..66717e7 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.48", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "Example", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..fc5fcd5 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "Example" +version = "0.1.0" + +[leanOptions] +autoImplicit = false + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.15.0" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..d0eb99f --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.15.0 diff --git a/readme.org b/readme.org new file mode 100644 index 0000000..597af03 --- /dev/null +++ b/readme.org @@ -0,0 +1,9 @@ +#+title: Readme + +To ensure that the lsp in emacs work, one needs to run +#+begin_src sh +lake exec cache get +lake build +#+end_src + +The build step could be done in emacs via just loading a file, however, if the dependency is large (for example mathlib), it will crash due to size issues