Merge branch 'dev' into goal/dependency
This commit is contained in:
commit
41e1f64d44
|
@ -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 $@
|
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
|
||||||
```
|
```
|
||||||
|
The provided `flake.nix` has a develop environment with Lean already setup.
|
||||||
|
|
||||||
## Usage
|
## Usage
|
||||||
|
|
||||||
|
|
|
@ -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
|
||||||
|
}
|
|
@ -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;
|
||||||
|
};
|
||||||
|
};
|
||||||
|
}
|
Loading…
Reference in New Issue