From f5a4aaa5afc0c9c7d97b1e4ef13d2b8656daa211 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Thu, 11 Jul 2024 13:34:20 -0700 Subject: [PATCH] Switch to a flake-based Nix build --- check | 12 ++--- default.nix | 134 +++------------------------------------------------- flake.lock | 61 ++++++++++++++++++++++++ flake.nix | 125 ++++++++++++++++++++++++++++++++++++++++++++++++ shell.nix | 2 - 5 files changed, 199 insertions(+), 135 deletions(-) create mode 100644 flake.lock create mode 100644 flake.nix delete mode 100644 shell.nix diff --git a/check b/check index ae397fb8..689a0b4f 100755 --- a/check +++ b/check @@ -2,12 +2,12 @@ git clean -dfx -nix-build --cores 4 . --argstr coqPackages coqPackages_8_14 > log_8_14.txt 2>&1 & -nix-build --cores 4 . --argstr coqPackages coqPackages_8_15 > log_8_15.txt 2>&1 & -nix-build --cores 4 . --argstr coqPackages coqPackages_8_16 > log_8_16.txt 2>&1 & -nix-build --cores 4 . --argstr coqPackages coqPackages_8_17 > log_8_17.txt 2>&1 & -nix-build --cores 4 . --argstr coqPackages coqPackages_8_18 > log_8_18.txt 2>&1 & -nix-build --cores 4 . --argstr coqPackages coqPackages_8_19 > log_8_19.txt 2>&1 & +nix build --cores 4 .\#packages.x86_64-darwin.category-theory_8_14 > log_8_14.txt 2>&1 & +nix build --cores 4 .\#packages.x86_64-darwin.category-theory_8_15 > log_8_15.txt 2>&1 & +nix build --cores 4 .\#packages.x86_64-darwin.category-theory_8_16 > log_8_16.txt 2>&1 & +nix build --cores 4 .\#packages.x86_64-darwin.category-theory_8_17 > log_8_17.txt 2>&1 & +nix build --cores 4 .\#packages.x86_64-darwin.category-theory_8_18 > log_8_18.txt 2>&1 & +nix build --cores 4 .\#packages.x86_64-darwin.category-theory_8_19 > log_8_19.txt 2>&1 & docker run -t coqorg/coq:dev bash -c ' git clone https://github.com/jwiegley/category-theory; diff --git a/default.nix b/default.nix index 50a332bb..fd1fe39d 100644 --- a/default.nix +++ b/default.nix @@ -1,127 +1,7 @@ -args@{ - rev ? "90f456026d284c22b3e3497be980b2e47d0b28ac" -, sha256 ? "164lsq7xjjvpga6l6lfi9wfsnshgfxnpa8lvb2imscdwgmajakrc" - -, pkgs ? import (builtins.fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/${rev}.tar.gz"; - inherit sha256; }) { - config.allowUnfree = true; - config.allowBroken = false; - } -}: - -let - -equations = coqPackages: - with pkgs.${coqPackages}; pkgs.stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-equations-${version}"; - version = "1.3"; - - src = pkgs.fetchFromGitHub ({ - owner = "mattam82"; - repo = "Coq-Equations"; - } // - (if coqPackages == "coqPackages_8_14" - then { - rev = "v1.3-8.14"; - sha256 = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"; - } else {}) // - (if coqPackages == "coqPackages_8_15" - then { - rev = "v1.3-8.15"; - sha256 = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k"; - } else {}) // - (if coqPackages == "coqPackages_8_16" - then { - rev = "v1.3-8.16"; - sha256 = "sha256-zyMGeRObtSGWh7n3WCqesBZL5EgLvKwmnTy09rYpxyE="; - } else {}) // - (if coqPackages == "coqPackages_8_17" - then { - rev = "v1.3-8.17"; - sha256 = "sha256-yNotSIxFkhTg3reZIchGQ7cV9WmTJ7p7hPfKGBiByDw="; - } else {}) // - (if coqPackages == "coqPackages_8_18" - then { - rev = "v1.3-8.18"; - sha256 = "sha256-8MZO9vWdr8wlAov0lBTYMnde0RuMyhaiM99zp7Zwfao="; - } else {}) // - (if coqPackages == "coqPackages_8_19" - then { - rev = "v1.3-8.19"; - sha256 = "sha256-roBCWfAHDww2Z2JbV5yMI3+EOfIsv3WvxEcUbBiZBsk="; - } else {})); - - phases = [ - "unpackPhase" "configurePhase" "buildPhase" "checkPhase" "installPhase" - ]; - - buildInputs = [ - coq coq.ocaml coq.findlib - ]; - enableParallelBuilding = true; - - configurePhase = "coq_makefile -f _CoqProject -o Makefile.coq"; - checkPhase = "make examples test-suite"; - - installFlags = [ - "COQLIB=$(out)/lib/coq/${coq.coq-version}/" - "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib" - "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" - "DOCDIR=$(out)/share/coq/${coq.coq-version}/" - "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" - ]; - - env = pkgs.buildEnv { inherit name; paths = buildInputs; }; - passthru = { - compatibleCoqVersions = v: - builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" ]; - }; - }; - -category-theory = coqPackages: - with pkgs.${coqPackages}; pkgs.stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-category-theory-${version}"; - version = "1.0"; - - src = if pkgs ? coqFilterSource - then pkgs.coqFilterSource [] ./. - else ./.; - - buildInputs = [ - coq coq.ocaml coq.findlib (equations coqPackages) - ] ++ pkgs.lib.optionals (coqPackages != "coqPackages_8_16" && - coqPackages != "coqPackages_8_17" && - coqPackages != "coqPackages_8_18" && - coqPackages != "coqPackages_8_19") [ - dpdgraph - ]; - enableParallelBuilding = true; - - configurePhase = "coq_makefile -f _CoqProject -o Makefile.coq"; - - installFlags = [ - "COQLIB=$(out)/lib/coq/${coq.coq-version}/" - "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib" - "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" - "DOCDIR=$(out)/share/coq/${coq.coq-version}/" - "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" - ]; - - env = pkgs.buildEnv { inherit name; paths = buildInputs; }; - passthru = { - compatibleCoqVersions = v: - builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" ]; - }; - }; - -in rec { - inherit category-theory; - category-theory_8_14 = category-theory "coqPackages_8_14"; - category-theory_8_15 = category-theory "coqPackages_8_15"; - category-theory_8_16 = category-theory "coqPackages_8_16"; - category-theory_8_17 = category-theory "coqPackages_8_17"; - category-theory_8_18 = category-theory "coqPackages_8_18"; - category-theory_8_19 = category-theory "coqPackages_8_19"; - category-theory_cur = category-theory_8_19; -} +(import ( + fetchTarball { + url = "https://github.com/edolstra/flake-compat/archive/35bb57c0c8d8b62bbfd284272c928ceb64ddbde9.tar.gz"; + sha256 = "1prd9b1xx8c0sfwnyzkspplh30m613j42l1k789s521f4kv4c2z2"; } +) { + src = ./.; +}).defaultNix diff --git a/flake.lock b/flake.lock new file mode 100644 index 00000000..3dbb3eef --- /dev/null +++ b/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1720657034, + "narHash": "sha256-nPhbeFdyN8yn+EXmnPcBWisoypndtQbNIhSKmAinv3E=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "212defe037698e18fc9521dfe451779a8979844c", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 00000000..478057b5 --- /dev/null +++ b/flake.nix @@ -0,0 +1,125 @@ +{ + description = "An axiom-free formalization of category theory in Coq for personal study and practical work"; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable"; + flake-utils.url = "github:numtide/flake-utils"; + }; + + outputs = { self, nixpkgs, flake-utils }: + flake-utils.lib.eachDefaultSystem (system: + let pkgs = import nixpkgs { inherit system; }; + in rec { + packages = rec { + equations = coqPackages: with pkgs.${coqPackages}; pkgs.stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-equations-${version}"; + version = "1.3"; + + src = pkgs.fetchFromGitHub ({ + owner = "mattam82"; + repo = "Coq-Equations"; + } // + (if coqPackages == "coqPackages_8_14" + then { + rev = "v1.3-8.14"; + sha256 = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"; + } else {}) // + (if coqPackages == "coqPackages_8_15" + then { + rev = "v1.3-8.15"; + sha256 = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k"; + } else {}) // + (if coqPackages == "coqPackages_8_16" + then { + rev = "v1.3-8.16"; + sha256 = "sha256-zyMGeRObtSGWh7n3WCqesBZL5EgLvKwmnTy09rYpxyE="; + } else {}) // + (if coqPackages == "coqPackages_8_17" + then { + rev = "v1.3-8.17"; + sha256 = "sha256-yNotSIxFkhTg3reZIchGQ7cV9WmTJ7p7hPfKGBiByDw="; + } else {}) // + (if coqPackages == "coqPackages_8_18" + then { + rev = "v1.3-8.18"; + sha256 = "sha256-8MZO9vWdr8wlAov0lBTYMnde0RuMyhaiM99zp7Zwfao="; + } else {}) // + (if coqPackages == "coqPackages_8_19" + then { + rev = "v1.3-8.19"; + sha256 = "sha256-roBCWfAHDww2Z2JbV5yMI3+EOfIsv3WvxEcUbBiZBsk="; + } else {})); + + phases = [ + "unpackPhase" "configurePhase" "buildPhase" "checkPhase" "installPhase" + ]; + + buildInputs = [ + coq coq.ocaml coq.findlib + ]; + enableParallelBuilding = true; + + configurePhase = "coq_makefile -f _CoqProject -o Makefile.coq"; + checkPhase = "make examples test-suite"; + + installFlags = [ + "COQLIB=$(out)/lib/coq/${coq.coq-version}/" + "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib" + "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" + "DOCDIR=$(out)/share/coq/${coq.coq-version}/" + "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" + ]; + + env = pkgs.buildEnv { inherit name; paths = buildInputs; }; + passthru = { + compatibleCoqVersions = v: + builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" ]; + }; + }; + + category-theory = coqPackages: with pkgs.${coqPackages}; pkgs.stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-category-theory-${version}"; + version = "1.0"; + + src = if pkgs ? coqFilterSource + then pkgs.coqFilterSource [] ./. + else ./.; + + buildInputs = [ + coq coq.ocaml coq.findlib (equations coqPackages) + ] ++ pkgs.lib.optionals (coqPackages == "coqPackages_8_14" || + coqPackages == "coqPackages_8_15") [ + dpdgraph + ]; + enableParallelBuilding = true; + + configurePhase = "coq_makefile -f _CoqProject -o Makefile.coq"; + + installFlags = [ + "COQLIB=$(out)/lib/coq/${coq.coq-version}/" + "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib" + "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" + "DOCDIR=$(out)/share/coq/${coq.coq-version}/" + "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" + ]; + + env = pkgs.buildEnv { inherit name; paths = buildInputs; }; + passthru = { + compatibleCoqVersions = v: + builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" ]; + }; + }; + + category-theory_8_14 = category-theory "coqPackages_8_14"; + category-theory_8_15 = category-theory "coqPackages_8_15"; + category-theory_8_16 = category-theory "coqPackages_8_16"; + category-theory_8_17 = category-theory "coqPackages_8_17"; + category-theory_8_18 = category-theory "coqPackages_8_18"; + category-theory_8_19 = category-theory "coqPackages_8_19"; + + default = category-theory_8_19; + }; + + defaultPackage = packages.default; + }); +} diff --git a/shell.nix b/shell.nix deleted file mode 100644 index 0e758cbe..00000000 --- a/shell.nix +++ /dev/null @@ -1,2 +0,0 @@ -args@{ version ? "category-theory_cur", pkgs ? null }: -(import ./default.nix (if pkgs == null then {} else { inherit pkgs; })).${version}