.github/workflows/nix-action.yml

@@ -11,39 +11,26 @@ on:
       - '**'
 
 jobs:
-  setup:
-    runs-on: ubuntu-latest
-    steps:
-    - name: Do nothing
-      run: echo "No setup, using meta.yml bundles"
-  "aac-tactics":
-    name: Main build
+  build:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        bundle:
-          - default
+        coq_version:
+          - 'master'
+      fail-fast: false
     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 coq-community
-      uses: cachix/cachix-action@v8
-      with:
-        # Name of a cachix cache to pull/substitute
-        name: coq-community
-        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-    - name: Git checkout
-      uses: actions/checkout@v2
-      with:
-        fetch-depth: 0
-    - name: Building/fetching dependencies
-      run: nix-build --no-out-link --argstr bundle "${{ matrix.bundle }}" --argstr job "_deps"
-    - name: Building/fetching current project
-      run: nix-build --no-out-link --argstr bundle "${{ matrix.bundle }}" --argstr job "aac-tactics"
+      - uses: cachix/install-nix-action@v12
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - uses: cachix/cachix-action@v8
+        with:
+          name: coq
+      - uses: cachix/cachix-action@v8
+        with:
+          name: coq-community
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+      - uses: cachix/cachix-action@v8
+        with:
+          name: math-comp
+      - uses: actions/checkout@v2
+      - run: nix-build https://coq.inria.fr/nix/toolbox --argstr job "aac-tactics" --arg override "{coq = \"${{ matrix.coq_version }}\";}"

.travis.yml

@@ -0,0 +1,67 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+os: linux
+dist: bionic
+language: shell
+
+.opam: &OPAM
+  language: shell
+  services: docker
+  install: |
+    # Prepare the COQ container
+    docker pull ${COQ_IMAGE}
+    docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${PACKAGE} -w /home/coq/${PACKAGE} ${COQ_IMAGE}
+    docker exec COQ /bin/bash --login -c "
+      # This bash script is double-quoted to interpolate Travis CI env vars:
+      echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
+      export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
+      set -ex  # -e = exit on failure; -x = trace for debug
+      opam update -y
+      opam pin add ${PACKAGE} . -y -n -k path
+      opam install ${PACKAGE} -y -j ${NJOBS} --deps-only
+      opam config list
+      opam repo list
+      opam list
+      "
+  script:
+  - echo -e "${ANSI_YELLOW}Building ${PACKAGE}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
+  - |
+    docker exec COQ /bin/bash --login -c "
+      export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
+      set -ex
+      sudo chown -R coq:coq /home/coq/${PACKAGE}
+      opam install ${PACKAGE} -v -y -j ${NJOBS}
+      "
+  - docker stop COQ  # optional
+  - echo -en 'travis_fold:end:script\\r'
+
+.nix: &NIX
+  language: nix
+  nix: 2.3.7
+  sudo: false
+  install:
+  # for cachix we need travis to be a trusted nix user
+  - echo "trusted-users = $USER" | sudo tee -a /etc/nix/nix.conf
+  - sudo systemctl restart nix-daemon
+  - nix-env -iA nixpkgs.cachix
+  - cachix use coq
+  - cachix use coq-community
+  - cachix use math-comp
+  script:
+  - nix-build https://coq.inria.fr/nix/toolbox --argstr job "aac-tactics" --arg override "{coq = \"$COQ\";}"
+jobs:
+  include:
+
+  # Test supported versions of Coq via Nix
+  - env:
+    - COQ=master
+    <<: *NIX
+
+  # Test supported versions of Coq via OPAM
+  - env:
+    - COQ_IMAGE=coqorg/coq:dev
+    - PACKAGE=coq-aac-tactics.dev
+    - NJOBS=2
+    <<: *OPAM
+

coq-aac-tactics.opam

@@ -1,3 +1,6 @@
+# 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: "palmskog@gmail.com"
 version: "dev"
@@ -19,7 +22,7 @@ provided with the plugin."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "ocaml" {>= "4.05.0"}
-  "dune" {>= "2.4"}
+  "dune" {>= "2.5"}
   "coq" {= "dev"}
 ]
 

dune-project

@@ -1,3 +1,3 @@
-(lang dune 2.4)
-(using coq 0.1)
-(name coq-aac-tactics)
+(lang dune 2.5)
+(using coq 0.2)
+(name aac-tactics)

meta.yml

@@ -4,9 +4,12 @@ shortname: aac-tactics
 organization: coq-community
 community: true
 action: true
+travis: true
 nix: true
 plugin: true
 doi: 10.1007/978-3-642-25379-9_14
+branch: master
+dune: true
 
 synopsis: >-
   Coq plugin providing tactics for rewriting universally quantified
@@ -56,17 +59,6 @@ supported_ocaml_versions:
 tested_coq_opam_versions:
 - version: dev
 
-cachix:
-- name: coq
-- name: coq-community
-  token: CACHIX_AUTH_TOKEN
-
-nix-bundles:
-- bundle: default
-  packages:
-  - name: coq
-    version: master
-
 namespace: AAC_tactics
 
 keywords:

src/aac_rewrite.ml

@@ -346,7 +346,7 @@ let aac_rewrite_wrap  ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
       let check_type x =
         Tacmach.New.pf_conv_x goal x rlt.Coq.Relation.carrier
       in
-      let hypinfo = Coq.Rewrite.get_hypinfo env sigma rew ~l2r ?check_type:(Some check_type) in      
+      let hypinfo = Coq.Rewrite.get_hypinfo env sigma ?check_type:(Some check_type) rew ~l2r in
       let sigma,rewinfo = dispatch env sigma in_left concl hypinfo in
       let sigma =
         match extra with

src/coq.ml

@@ -352,7 +352,7 @@ type hypinfo =
       l2r : bool; 			(** rewriting from left to right  *)
     }
 
-let get_hypinfo env sigma c ?check_type ~l2r  : hypinfo =
+let get_hypinfo env sigma ?check_type c ~l2r : hypinfo =
   let ctype = Typing.unsafe_type_of env sigma c in
   let (rel_context, body_type) = decompose_prod_assum sigma ctype in
   let rec check f e =

src/coq.mli

@@ -174,11 +174,11 @@ type hypinfo =
       l2r : bool; 			(** rewriting from left to right  *)
     }
 
-(** [get_hypinfo H ?check_type l2r] analyse the hypothesis H, and
+(** [get_hypinfo ?check_type H l2r] analyse the hypothesis H, and
     build the related hypinfo. Moreover, an optionnal
     function can be provided to check the type of every free
     variable of the body of the hypothesis.  *)
-val get_hypinfo : Environ.env -> Evd.evar_map ->  EConstr.constr -> ?check_type:(EConstr.types -> bool) -> l2r:bool -> hypinfo
+val get_hypinfo : Environ.env -> Evd.evar_map -> ?check_type:(EConstr.types -> bool) -> EConstr.constr -> l2r:bool -> hypinfo
 
 (** {2 Rewriting with bindings}