aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/workflows/nix-action.yml74
-rw-r--r--.github/workflows/nix.yml32
-rw-r--r--.nix/config.nix34
-rw-r--r--.nix/coq-nix-toolbox.nix1
-rw-r--r--.nix/coq-overlays/mathcomp-single/default.nix2
-rw-r--r--config.nix3
-rw-r--r--default.nix155
-rw-r--r--package.nix1
8 files changed, 179 insertions, 123 deletions
diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
deleted file mode 100644
index f31495f..0000000
--- a/.github/workflows/nix-action.yml
+++ /dev/null
@@ -1,74 +0,0 @@
-name: Nix CI
-
-on:
- push:
- branches:
- - master
- pull_request:
- branches:
- - '**'
-
-jobs:
- dependencies:
- runs-on: ubuntu-latest
- outputs:
- matrix: ${{ steps.set-matrix.outputs.matrix }}
- steps:
- - name: Cachix install
- uses: cachix/install-nix-action@v12
- with:
- nix_path: nixpkgs=channel:nixpkgs-unstable
- - name: Cachix setup coq
- uses: cachix/cachix-action@v8
- with:
- # Name of a cachix cache to pull/substitute
- name: coq
- - name: Cachix setup math-comp
- uses: cachix/cachix-action@v8
- with:
- # Name of a cachix cache to pull/substitute
- name: math-comp
- authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
- - name: Git checkout
- uses: actions/checkout@v2
- with:
- fetch-depth: 0
- - name: Building/fetching dependencies
- run: nix-build --argstr ci-job dependencies
- - name: Setup build matrix
- id: set-matrix
- run: |
- matrix=$(nix-shell --arg do-nothing true --run nixTasks)
- echo ::set-output name=matrix::{\"task\":$(echo $matrix)}\"
-
- main:
- runs-on: ubuntu-latest
- needs:
- - dependencies
- strategy:
- matrix: ${{fromJson(needs.dependencies.outputs.matrix)}}
- steps:
- - name: Cachix install
- uses: cachix/install-nix-action@v12
- with:
- nix_path: nixpkgs=channel:nixpkgs-unstable
- - name: Cachix setup coq
- uses: cachix/cachix-action@v8
- with:
- # Name of a cachix cache to pull/substitute
- name: coq
- - name: Cachix setup math-comp
- uses: cachix/cachix-action@v8
- with:
- # Name of a cachix cache to pull/substitute
- name: math-comp
- authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
- - name: Git checkout
- uses: actions/checkout@v2
- with:
- fetch-depth: 0
- - name: Building/fetching dependencies
- run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies
- - name: Building/fetching current project
- run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job main
-
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
new file mode 100644
index 0000000..6a34426
--- /dev/null
+++ b/.github/workflows/nix.yml
@@ -0,0 +1,32 @@
+name: Cachix
+on:
+ push:
+jobs:
+ cachix:
+ name: Cachix branch
+ runs-on: ubuntu-latest
+ strategy:
+ fail-fast: false
+ matrix:
+ coq: [ "8.11", "8.12" ]
+ steps:
+ - name: Get branch shortname
+ run: echo "##[set-output name=name;]$(echo ${GITHUB_REF#refs/heads/})"
+ id: branch-short
+ - name: Get owner name
+ run: echo "##[set-output name=name;]$(echo $GITHUB_REPOSITORY | cut -d/ -f1)"
+ id: owner
+ - name: Get owner lowercase name
+ run: echo "##[set-output name=name;]$(echo $GITHUB_REPOSITORY | cut -d/ -f1 | tr '[:upper:]' '[:lower:]')"
+ id: owner-lowercase
+ - uses: cachix/install-nix-action@v12
+ - uses: cachix/cachix-action@v8
+ if: steps.owner.outputs.name == 'math-comp' || steps.owner.outputs.name == 'CohenCyril'
+ with:
+ # Name of a cachix cache to push and pull/substitute
+ name: ${{ steps.owner-lowercase.outputs.name }}
+ extraPullNames: coq
+ # Authentication token for Cachix, needed only for private cache access
+ authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+ # building fake mathcomp-fast target
+ - run: nix-build https://github.com/math-comp/math-comp-nix/archive/master.tar.gz --arg config '{coq = "${{ matrix.coq }}"; mathcomp = "${{ steps.owner.outputs.name }}/${{ steps.branch-short.outputs.name }}";}' --argstr package mathcomp
diff --git a/.nix/config.nix b/.nix/config.nix
deleted file mode 100644
index dde76b9..0000000
--- a/.nix/config.nix
+++ /dev/null
@@ -1,34 +0,0 @@
-{
- ## DO NOT CHANGE THIS
- format = "1.0.0";
- ## unless you made an automated or manual update
- ## to another supported format.
-
- ## The attribute to build, either from nixpkgs
- ## of from the overlays located in `.nix/coq-overlays`
- coq-attribute = "mathcomp";
-
- ## If you want to select a different attribute
- ## to serve as a basis for nix-shell edit this
- coq-shell-attribute = "mathcomp-single";
-
- ## Indicate the relative location of your _CoqProject
- ## If not specified, it defaults to "_CoqProject"
- coqproject = "mathcomp/_CoqProject";
-
- ## select an entry to build in the following `tasks` set
- ## defaults to "default"
- select = "coq-8.13";
-
- ## write one `tasks.name` attribute set per
- ## alternative configuration, the can be used to
- ## compute several ci jobs as well
-
- ## You can override Coq and other Coq coqPackages
- ## through the following attribute
-
- tasks."coq-8.13".coqPackages.coq.override.version = "8.13";
- tasks."coq-8.12".coqPackages.coq.override.version = "8.12";
- tasks."coq-8.11".coqPackages.coq.override.version = "8.11";
- tasks."coq-8.10".coqPackages.coq.override.version = "8.10";
-}
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
deleted file mode 100644
index ba2d943..0000000
--- a/.nix/coq-nix-toolbox.nix
+++ /dev/null
@@ -1 +0,0 @@
-"e54b920493f0494ede95b5f7d083cc8b20b1f5a6"
diff --git a/.nix/coq-overlays/mathcomp-single/default.nix b/.nix/coq-overlays/mathcomp-single/default.nix
deleted file mode 100644
index 65be1c4..0000000
--- a/.nix/coq-overlays/mathcomp-single/default.nix
+++ /dev/null
@@ -1,2 +0,0 @@
-{ mathcomp, version ? null }:
-mathcomp.override {single = true; version = null;}
diff --git a/config.nix b/config.nix
new file mode 100644
index 0000000..bb1ecee
--- /dev/null
+++ b/config.nix
@@ -0,0 +1,3 @@
+{
+ coq = "8.11";
+}
diff --git a/default.nix b/default.nix
index a588f43..195a47e 100644
--- a/default.nix
+++ b/default.nix
@@ -1,13 +1,144 @@
-{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
- update-nixpkgs ? false, ci-matrix ? false, ci-job ? null,
- override ? {}, ocaml-override ? {}, global-override ? {},
- ci ? (!isNull ci-job), inNixShell ? null, src ? ./.,
-}@args:
-let auto = fetchGit {
- url = "https://github.com/coq-community/coq-nix-toolbox.git";
- ref = "master";
-# putting a ref here is strongly advised
- rev = import .nix/coq-nix-toolbox.nix;
-};
+{
+ nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix
+ else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/502845c3e31ef3de0e424f3fcb09217df2ce6df6.tar.gz),
+ config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}),
+ withEmacs ? false,
+ print-env ? false,
+ do-nothing ? false,
+ package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"),
+ src ? (if builtins.pathExists ./package.nix then ./. else false)
+}:
+with builtins;
+let
+ cfg-fun = if isFunction config then config else (pkgs: config);
+ pkg-src = if src == false then {}
+ else { ${if package == "mathcomp.single" then "mathcomp" else package} = src; };
+ pkgs = if isAttrs nixpkgs then nixpkgs else import nixpkgs {
+ overlays = [ (pkgs: super-pkgs: with pkgs.lib;
+ let coqPackages = with pkgs; {
+ "8.7" = coqPackages_8_7;
+ "8.8" = coqPackages_8_8;
+ "8.9" = coqPackages_8_9;
+ "8.10" = coqPackages_8_10;
+ "8.11" = coqPackages_8_11;
+ "8.12" = coqPackages_8_12;
+ "default" = coqPackages_8_10;
+ }.${(cfg-fun pkgs).coq or "default"}.overrideScope'
+ (coqPackages: super-coqPackages:
+ let
+ all-pkgs = pkgs // { inherit coqPackages; };
+ cfg = pkg-src // {
+ mathcomp-fast = {
+ src = ./.;
+ propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast);
+ };
+ mathcomp-full = {
+ src = ./.;
+ propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all);
+ };
+ } // (cfg-fun all-pkgs);
+ in {
+ mathcomp-extra-config =
+ let mec = super-coqPackages.mathcomp-extra-config; in
+ lib.recursiveUpdate mec {
+ initial = {
+ # fixing mathcomp analysis to depend on real-closed
+ mathcomp-analysis = {version, coqPackages} @ args:
+ let mca = mec.initial.mathcomp-analysis args; in
+ mca // {
+ propagatedBuildInputs = mca.propagatedBuildInputs ++
+ (if builtins.elem coq.version ["8.10" "8.11" "8.12"] then (with coqPackages; [ coq-elpi hierarchy-builder ]) else []);
+ };
+ };
+ for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} =
+ (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) //
+ (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]);
+ };
+ mathcomp = if cfg?mathcomp then coqPackages.mathcomp_ cfg.mathcomp else super-coqPackages.mathcomp;
+ } // mapAttrs
+ (package: version: coqPackages.mathcomp-extra package version)
+ (removeAttrs cfg ["mathcomp" "coq"])
+ ); in {
+ coqPackages = coqPackages.filterPackages coqPackages.coq coqPackages;
+ coq = coqPackages.coq;
+ mc-clean = src: {
+ version = baseNameOf src;
+ src = cleanSourceWith {
+ src = cleanSource src;
+ filter = path: type: let baseName = baseNameOf (toString path); in ! (
+ hasSuffix ".aux" baseName ||
+ hasSuffix ".d" baseName ||
+ hasSuffix ".vo" baseName ||
+ hasSuffix ".glob" baseName ||
+ elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"]
+ );
+ };
+ };
+ })];
+ };
+
+ mathcompnix = ./.;
+
+ shellHook = ''
+ nixEnv () {
+ echo "Here is your work environement"
+ echo "buildInputs:"
+ for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done
+ echo "propagatedBuildInputs:"
+ for x in $propagatedBuildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done
+ echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions"
+ }
+
+ printEnv () {
+ for x in $buildInputs; do echo $x; done
+ for x in $propagatedBuildInputs; do echo $x; done
+ }
+
+ cachixEnv () {
+ echo "Pushing environement to cachix"
+ printEnv | cachix push math-comp
+ }
+
+ nixDefault () {
+ cat $mathcompnix/default.nix
+ } > default.nix
+
+ updateNixPkgs (){
+ HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1);
+ URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz
+ SHA256=$(nix-prefetch-url --unpack $URL)
+ echo "fetchTarball {
+ url = $URL;
+ sha256 = \"$SHA256\";
+ }" > nixpkgs.nix
+ }
+ updateNixPkgsMaster (){
+ HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1);
+ URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz
+ SHA256=$(nix-prefetch-url --unpack $URL)
+ echo "fetchTarball {
+ url = $URL;
+ sha256 = \"$SHA256\";
+ }" > nixpkgs.nix
+ }
+ ''
+ + pkgs.lib.optionalString print-env "nixEnv";
+
+ emacs = with pkgs; emacsWithPackages
+ (epkgs: with epkgs.melpaStablePackages; [proof-general]);
+
+ pkg = with pkgs;
+ if package == "mathcomp.single" then coqPackages.mathcomp.single
+ else coqPackages.${package} or (coqPackages.current-mathcomp-extra package);
in
-(import auto ({inherit src;} // args)).nix-auto
+if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: {
+ inherit shellHook mathcompnix;
+
+ buildInputs = if do-nothing then []
+ else (old.buildInputs ++
+ (if pkgs.lib.trivial.inNixShell then pkgs.lib.optional withEmacs pkgs.emacs
+ else [])) ++ [ pkgs.lua pkgs.sedutil ];
+
+ propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs;
+
+}) else pkg
diff --git a/package.nix b/package.nix
new file mode 100644
index 0000000..661824d
--- /dev/null
+++ b/package.nix
@@ -0,0 +1 @@
+"mathcomp.single"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:11:21 +0000