feat: Output shared library in Nix flake #48

Merged
aniva merged 16 commits from feature/lib into dev 2024-03-16 19:01:04 -07:00
6 changed files with 24 additions and 22 deletions
Showing only changes of commit b7542b4749 - Show all commits

View File

@ -1,8 +1,8 @@
LIB := build/lib/Pantograph.olean LIB := ./.lake/build/lib/Pantograph.olean
EXE := build/bin/pantograph EXE := ./.lake/build/bin/pantograph
SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
TEST_EXE := build/bin/test TEST_EXE := ./.lake/build/bin/test
TEST_SOURCE := $(wildcard Test/*.lean) TEST_SOURCE := $(wildcard Test/*.lean)
$(LIB) $(EXE): $(SOURCE) $(LIB) $(EXE): $(SOURCE)
@ -12,7 +12,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
lake build test lake build test
test: $(TEST_EXE) test: $(TEST_EXE)
lake env $(TEST_EXE) $(TEST_EXE)
clean: clean:
lake clean lake clean

View File

@ -41,16 +41,16 @@
"nixpkgs": "nixpkgs_2" "nixpkgs": "nixpkgs_2"
}, },
"locked": { "locked": {
"lastModified": 1695693562, "lastModified": 1709691092,
"narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=", "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=",
"owner": "leanprover", "owner": "leanprover",
"repo": "lean4", "repo": "lean4",
"rev": "a832f398b80a5ebb820d27b9e55ec949759043ff", "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "leanprover", "owner": "leanprover",
"ref": "v4.1.0", "ref": "v4.7.0-rc2",
"repo": "lean4", "repo": "lean4",
"type": "github" "type": "github"
} }

View File

@ -4,7 +4,7 @@
inputs = { inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
flake-parts.url = "github:hercules-ci/flake-parts"; flake-parts.url = "github:hercules-ci/flake-parts";
lean.url = "github:leanprover/lean4?ref=v4.1.0"; lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2";
}; };
outputs = inputs @ { outputs = inputs @ {

View File

@ -1,12 +1,14 @@
{"version": 6, {"version": 7,
"packagesDir": "lake-packages", "packagesDir": ".lake/packages",
"packages": "packages":
[{"git": [{"url": "https://github.com/lurk-lab/LSpec.git",
{"url": "https://github.com/lurk-lab/LSpec.git", "type": "git",
"subDir?": null, "subDir": null,
"rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41", "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"opts": {},
"name": "LSpec", "name": "LSpec",
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41", "manifestFile": "lake-manifest.json",
"inherited": false}}], "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"name": "pantograph"} "inherited": false,
"configFile": "lakefile.lean"}],
"name": "pantograph",
"lakeDir": ".lake"}

View File

@ -15,7 +15,7 @@ lean_exe pantograph {
} }
require LSpec from git require LSpec from git
"https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41" "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
lean_lib Test { lean_lib Test {
} }
lean_exe test { lean_exe test {

View File

@ -1 +1 @@
leanprover/lean4:4.1.0 leanprover/lean4:4.7.0-rc2