File tree Expand file tree Collapse file tree 4 files changed +35
-117
lines changed
Expand file tree Collapse file tree 4 files changed +35
-117
lines changed Original file line number Diff line number Diff line change 3333 with :
3434 name : argumentcomputer
3535 authToken : ' ${{ secrets.CACHIX_AUTH_TOKEN }}'
36- - run : nix run .#test
36+ - run : nix build
Original file line number Diff line number Diff line change 11{
2- description = "Lean 4 Example Project " ;
2+ description = "LSpec Nix Flake " ;
33
44 inputs = {
5- nixpkgs . url = "github:nixos/nixpkgs/nixos-24.11 " ;
5+ nixpkgs . url = "github:nixos/nixpkgs/nixos-unstable " ;
66 flake-parts . url = "github:hercules-ci/flake-parts" ;
77 lean4-nix = {
88 url = "github:argumentcomputer/lean4-nix" ;
99 inputs . nixpkgs . follows = "nixpkgs" ;
10- #rev = "";
1110 } ;
1211 } ;
1312
2524 "x86_64-linux"
2625 ] ;
2726
28- flake = {
29- lib = import ./lspec.nix ;
30- } ;
31-
3227 perSystem = {
3328 system ,
3429 pkgs ,
3530 self' ,
3631 config ,
3732 ...
3833 } :
39- let
40- lib = ( import ./lspec.nix { inherit pkgs lean4-nix ; } ) . lib ;
41- lspecBin = lib . lspecLib . executable ;
42- in
4334 {
4435 _module . args . pkgs = import nixpkgs {
4536 inherit system ;
4637 overlays = [ ( lean4-nix . readToolchainFile ./lean-toolchain ) ] ;
4738 } ;
48- # TODO: Replace with a Nix-compatible binary
49- # Running `lspecBin` will cause an error due to calling `lake` explicitly and only parsing `lakefile.lean` files
50- # It is included for completeness only
51- #packages.default = lspecBin;
39+
40+ # Build the library with `nix build`
41+ packages . default = ( ( lean4-nix . lake { inherit pkgs ; } ) . mkPackage {
42+ src = ./. ;
43+ roots = [ "LSpec" ] ;
44+ } ) . modRoot ;
5245
5346 devShells . default = pkgs . mkShell {
5447 packages = with pkgs . lean ; [ lean lean-all ] ;
Load Diff This file was deleted.
You can’t perform that action at this time.
0 commit comments