Merge pull request #16 from coq-community/dune-nix-ci

use Dune in repo opam packages, use Nix CI

Author: palmskog

.github/workflows/nix-action.yml

@@ -0,0 +1,47 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Nix CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    paths:
+    - .github/workflows/**
+  pull_request_target:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        overrides:
+          - 'coq = "master"'
+      fail-fast: false
+    steps:
+      - name: Determine which commit to test
+        run: |
+          if [[ ${{ github.event_name }} =~ "pull_request" ]]; then
+            merge_commit=$(git ls-remote ${{ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge | cut -f1)
+            if [ -z "$merge_commit" ]; then
+              echo "tested_commit=${{ github.event.pull_request.head.sha }}" >> $GITHUB_ENV
+            else
+              echo "tested_commit=$merge_commit" >> $GITHUB_ENV
+            fi
+          else
+            echo "tested_commit=${{ github.sha }}" >> $GITHUB_ENV
+          fi
+      - uses: cachix/install-nix-action@v14
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - uses: cachix/cachix-action@v10
+        with:
+          name: coq-community
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+          extraPullNames: coq, math-comp
+      - uses: actions/checkout@v2
+        with:
+          ref: ${{ env.tested_ref }}
+      - run: >
+          nix-build https://coq.inria.fr/nix/toolbox --argstr job qarith-stern-brocot --arg override '{ ${{ matrix.overrides }}; qarith-stern-brocot = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }'

README.md

@@ -5,6 +5,7 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 # Binary Rational Numbers
 
 [![Docker CI][docker-action-shield]][docker-action-link]
+[![Nix CI][nix-action-shield]][nix-action-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
@@ -13,6 +14,9 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [docker-action-shield]: https://github.com/coq-community/qarith-stern-brocot/workflows/Docker%20CI/badge.svg?branch=master
 [docker-action-link]: https://github.com/coq-community/qarith-stern-brocot/actions?query=workflow:"Docker%20CI"
 
+[nix-action-shield]: https://github.com/coq-community/qarith-stern-brocot/workflows/Nix%20CI/badge.svg?branch=master
+[nix-action-link]: https://github.com/coq-community/qarith-stern-brocot/actions?query=workflow:"Nix%20CI"
+
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
 
@@ -26,7 +30,7 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [doi-shield]: https://zenodo.org/badge/DOI/10.1007/978-3-540-24849-1_20.svg
 [doi-link]: https://doi.org/10.1007/978-3-540-24849-1_20
 
-Development of rational numbers as finite binary lists and defining
+Development of rational numbers in Coq as finite binary lists and defining
 field operations on them in two different ways: strict and lazy.
 
 
@@ -66,8 +70,7 @@ make install
 
 ## Documentation
 
-This package contains a rational arithmetic library for Coq.
-This includes:
+This project contains a rational arithmetic library for Coq. This includes:
 
 - A binary representation for positive rational numbers `Qpositive` and its
   extension to `Q` by adding sign bit (also known as Stern-Brocot

coq-qarith-stern-brocot.opam

@@ -1,6 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
 maintainer: "[email protected]"
 version: "dev"
@@ -10,15 +7,15 @@ dev-repo: "git+https://github.com/coq-community/qarith-stern-brocot.git"
 bug-reports: "https://github.com/coq-community/qarith-stern-brocot/issues"
 license: "LGPL-2.1-or-later"
 
-synopsis: "Binary rational numbers"
+synopsis: "Binary rational numbers in Coq"
 description: """
-Development of rational numbers as finite binary lists and defining
+Development of rational numbers in Coq as finite binary lists and defining
 field operations on them in two different ways: strict and lazy.
 """
 
-build: [make "-j%{jobs}%" ]
-install: [make "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
+  "dune" {>= "2.5"}
   "coq" {(>= "8.14" & < "8.15~") | (= "dev")}
 ]
 

meta.yml

@@ -4,11 +4,12 @@ shortname: qarith-stern-brocot
 organization: coq-community
 community: true
 action: true
+nix: true
 
-synopsis: Binary rational numbers
+synopsis: Binary rational numbers in Coq
 
 description: |
-  Development of rational numbers as finite binary lists and defining
+  Development of rational numbers in Coq as finite binary lists and defining
   field operations on them in two different ways: strict and lazy.
 
 doi: 10.1007/978-3-540-24849-1_20
@@ -40,6 +41,9 @@ tested_coq_opam_versions:
 - version: dev
 - version: '8.14'
 
+tested_coq_nix_versions:
+- coq_version: 'master'
+
 namespace: QArithSternBrocot
 
 keywords:
@@ -56,8 +60,7 @@ categories:
 documentation: |
   ## Documentation
 
-  This package contains a rational arithmetic library for Coq.
-  This includes:
+  This project contains a rational arithmetic library for Coq. This includes:
 
   - A binary representation for positive rational numbers `Qpositive` and its
     extension to `Q` by adding sign bit (also known as Stern-Brocot

theories/dune

@@ -2,4 +2,4 @@
  (name QArithSternBrocot)
  (package coq-qarith-stern-brocot)
  (synopsis "Binary rational numbers")
- (flags -w -notation-overridden))
+ (flags :standard -w -notation-overridden))