aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 9 Pull Requests 3 Packages Projects Releases 1 Wiki Activity

Merge branch 'dev' into goal/dependency

This commit is contained in:
Leni Aniva 2023-10-27 15:33:47 -07:00
parent 82f5494718 7dc6e4e549
commit ca7a081cac
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 241 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
README.md
View File

@ -18,6 +18,7 @@ export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATH
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
```
The provided `flake.nix` has a develop environment with Lean already setup.
## Usage

202
flake.lock Normal file
View File

@ -0,0 +1,202 @@
{
"nodes": {
"flake-parts": {
"inputs": {
"nixpkgs-lib": "nixpkgs-lib"
},
"locked": {
"lastModified": 1696343447,
"narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=",
"owner": "hercules-ci",
"repo": "flake-parts",
"rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4",
"type": "github"
},
"original": {
"owner": "hercules-ci",
"repo": "flake-parts",
"type": "github"
}
},
"flake-utils": {
"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": {
"flake-utils": "flake-utils",
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2"
},
"locked": {
"lastModified": 1695693562,
"narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
"owner": "leanprover",
"repo": "lean4",
"rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
"type": "github"
},
"original": {
"owner": "leanprover",
"ref": "v4.1.0",
"repo": "lean4",
"type": "github"
}
},
"lean4-mode": {
"flake": false,
"locked": {
"lastModified": 1676498134,
"narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
"owner": "leanprover",
"repo": "lean4-mode",
"rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4-mode",
"type": "github"
}
},
"lowdown-src": {
"flake": false,
"locked": {
"lastModified": 1633514407,
"narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
"owner": "kristapsdz",
"repo": "lowdown",
"rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
"type": "github"
},
"original": {
"owner": "kristapsdz",
"repo": "lowdown",
"type": "github"
}
},
"nix": {
"inputs": {
"lowdown-src": "lowdown-src",
"nixpkgs": "nixpkgs",
"nixpkgs-regression": "nixpkgs-regression"
},
"locked": {
"lastModified": 1657097207,
"narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
"owner": "NixOS",
"repo": "nix",
"rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nix",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1653988320,
"narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-22.05-small",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-lib": {
"locked": {
"dir": "lib",
"lastModified": 1696019113,
"narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a",
"type": "github"
},
"original": {
"dir": "lib",
"owner": "NixOS",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-regression": {
"locked": {
"lastModified": 1643052045,
"narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
}
},
"nixpkgs_2": {
"locked": {
"lastModified": 1686089707,
"narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs_3": {
"locked": {
"lastModified": 1697456312,
"narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=",
"owner": "nixos",
"repo": "nixpkgs",
"rev": "ca012a02bf8327be9e488546faecae5e05d7d749",
"type": "github"
},
"original": {
"owner": "nixos",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"flake-parts": "flake-parts",
"lean": "lean",
"nixpkgs": "nixpkgs_3"
}
}
},
"root": "root",
"version": 7
}

38
flake.nix Normal file
View File

@ -0,0 +1,38 @@
{
description = "Pantograph";
inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
flake-parts.url = "github:hercules-ci/flake-parts";
lean.url = "github:leanprover/lean4?ref=v4.1.0";
};
outputs = inputs @ {
self,
nixpkgs,
flake-parts,
lean,
...
} : flake-parts.lib.mkFlake { inherit inputs; } {
flake = {
};
systems = [
"x86_64-linux"
"x86_64-darwin"
];
perSystem = { system, pkgs, ... }: let
leanPkgs = lean.packages.${system};
project = leanPkgs.buildLeanPackage {
name = "Pantograph";
roots = [ "Main" "Pantograph" ];
src = ./.;
};
in rec {
packages = project // {
inherit (leanPkgs) lean;
default = packages.executable;
};
devShells.default = project.devShell;
};
};
}