Merge pull request #5 from erikmd/warn-error

Demo for coq-problem-matcher (warn/error)

Author: erikmd

.github/workflows/build-coq-demo.yml

@@ -1,9 +1,8 @@
-# This is a basic workflow to help you get started with Actions
-
+# This is a workflow example relying on docker-coq-action
 name: CI
 
-# Controls when the action will run.
-# cf. https://help.github.com/en/actions/configuring-and-managing-workflows/configuring-a-workflow#filtering-for-specific-branches-tags-and-paths
+# Controls when the action will run:
+# https://help.github.com/en/actions/configuring-and-managing-workflows/configuring-a-workflow#filtering-for-specific-branches-tags-and-paths
 # Triggers the workflow on push events or pull request events for the
 # master branch only:
 on:
@@ -15,59 +14,31 @@ on:
       - master
 
 # A workflow run is made up of one or more jobs that can run sequentially or in parallel
+# This workflow contains two jobs, build and mathcomp:
 jobs:
-  # This workflow contains a single job called "build"
   build:
     # The type of runner that the job will run on;
     # the OS must be GNU/Linux to be able to use the docker-coq-action
     runs-on: ubuntu-latest
-
     strategy:
       matrix:
         coq_version:
           - 8.11
           - dev
         ocaml_version: ['4.07-flambda']
-      # at most 20 concurrent jobs per free account
-      # cf. https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#usage-limits
+      # at most 20 concurrent jobs per free account:
+      # https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#usage-limits
       max-parallel: 4
 
     # Steps represent a sequence of tasks that will be executed as part of the job
     steps:
     # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
     - uses: actions/checkout@v2
-
     - uses: erikmd/docker-coq-action@master
-      id: docker-coq-action
       with:
         opam_file: 'coq-demo.opam'
         coq_version: ${{ matrix.coq_version }}
         ocaml_version: ${{ matrix.ocaml_version }}
-        custom_script: |
-          startGroup Test UID+GID
-            pwd
-            ls -hal
-            touch test || true
-            id
-            sudo chown -R coq:coq .
-            touch test
-            ls -hal
-            stat -c "UID=%u,GID=%g %n" $WORKDIR/$PACKAGE.opam
-          endGroup
-          startGroup Print opam config
-            opam config list; opam repo list; opam list
-          endGroup
-          startGroup Fetch dependencies
-            opam pin add -n -y -k path $PACKAGE $WORKDIR
-            opam update -y
-          endGroup
-          startGroup Build
-            opam install -y -v -j 2 $PACKAGE
-            opam list
-          endGroup
-          startGroup Uninstallation test
-            opam remove $PACKAGE
-          endGroup
 
   mathcomp:
     runs-on: ubuntu-latest
@@ -82,7 +53,12 @@ jobs:
     steps:
     - uses: actions/checkout@v2
     - uses: erikmd/docker-coq-action@master
-      id: docker-mathcomp-action
       with:
         opam_file: './coq-demo.opam'
         custom_image: ${{ matrix.image }}
+
+# Remark:
+# you may want to add the following badge to your README.md:
+# [![CI](https://github.com/$USER/$REPO/workflows/CI/badge.svg?branch=master)](https://github.com/$USER/$REPO/actions?query=workflow%3ACI)
+# after replacing $USER/$REPO to use your project namespace; note also
+# that CI is the workflow name, defined at the beginning of this file.

.github/workflows/misc-test.yml

@@ -0,0 +1,33 @@
+# a few tests, not intended for demo purposes
+name: misc-test
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  uid-test:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+    - run: id
+    - uses: erikmd/docker-coq-action@master
+      with:
+        opam_file: './coq-demo.opam'
+        coq_version: 'latest'
+        ocaml_version: '4.07-flambda'
+        custom_script: |
+          # small test, not intended for demo purposes
+          startGroup Test UID+GID
+            id
+            pwd
+            ls -hal
+            stat -c "UID=%u,GID=%g %n" $WORKDIR/$PACKAGE.opam
+          endGroup
+          startGroup Print opam config
+            opam config list; opam repo list; opam list
+          endGroup

README.md

@@ -5,6 +5,17 @@
 Demo of:
 
 * [docker-coq-action](https://github.com/erikmd/docker-coq-action),
-* [Docker-Coq](https://hub.docker.com/r/coqorg/coq) images,
+* [docker-coq](https://hub.docker.com/r/coqorg/coq) and
+  [docker-mathcomp](https://hub.docker.com/r/mathcomp/mathcomp) images,
 * and a workflow named [build-coq-demo.yml](./.github/workflows/build-coq-demo.yml),
 * relying on [coq-demo.opam](./coq-demo.opam)
+
+Note: you can add a badge in your `README.md`, like that of this demo:
+
+```
+[![CI](https://github.com/$USER/$REPO/workflows/CI/badge.svg?branch=master)](https://github.com/$USER/$REPO/actions?query=workflow%3ACI)
+```
+
+after replacing `$USER/$REPO` to use your project namespace; note also
+that CI is the workflow name, defined at the beginning of [this file](
+./.github/workflows/build-coq-demo.yml).

src/demo.v

@@ -10,3 +10,16 @@ Proof.
 idtac "proof in progress...".
 now intros P [H1 H2]; apply H1; apply H2; intros HP; apply H1.
 Qed.
+
+Variable A : Prop. (* raise a warning *)
+Lemma identity : A -> A.
+Proof.
+easy.
+Qed.
+
+Lemma eqs : forall a b c : nat, (a, b) = (b, a) -> b = c -> a = c.
+move=> a b c Hab Hc.
+case: Hab=>->_.
+case: Hc=>->. (* raise a warning *)
+done.
+Qed.