Wooooooo
This commit is contained in:
commit
d79410bbf5
4
.gitignore
vendored
Normal file
4
.gitignore
vendored
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
/.lake
|
||||||
|
.direnv
|
||||||
|
.envrc
|
||||||
|
.github
|
||||||
4
Example.lean
Normal file
4
Example.lean
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
import Aesop
|
||||||
|
|
||||||
|
def main : IO Unit :=
|
||||||
|
IO.println "Cirno's Perfect Arithmetics Class has begun!"
|
||||||
124
flake.lock
Normal file
124
flake.lock
Normal file
@ -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
|
||||||
|
}
|
||||||
46
flake.nix
Normal file
46
flake.nix
Normal file
@ -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 ];
|
||||||
|
};
|
||||||
|
};
|
||||||
|
};
|
||||||
|
}
|
||||||
95
lake-manifest.json
Normal file
95
lake-manifest.json
Normal file
@ -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"}
|
||||||
10
lakefile.toml
Normal file
10
lakefile.toml
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
name = "Example"
|
||||||
|
version = "0.1.0"
|
||||||
|
|
||||||
|
[leanOptions]
|
||||||
|
autoImplicit = false
|
||||||
|
|
||||||
|
[[require]]
|
||||||
|
name = "mathlib"
|
||||||
|
scope = "leanprover-community"
|
||||||
|
rev = "v4.15.0"
|
||||||
1
lean-toolchain
Normal file
1
lean-toolchain
Normal file
@ -0,0 +1 @@
|
|||||||
|
leanprover/lean4:v4.15.0
|
||||||
9
readme.org
Normal file
9
readme.org
Normal file
@ -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
|
||||||
Loading…
Reference in New Issue
Block a user