Test the new docker-coq-action feature allowing "opam_file" folders

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

@@ -38,9 +38,10 @@ jobs:
     steps:
       # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
       - uses: actions/checkout@v2
-      - uses: coq-community/docker-coq-action@v1
+      - uses: coq-community/docker-coq-action@optional-opam-file
         with:
-          opam_file: 'coq-demo.opam'
+          # opam_file: 'coq-demo.opam'
+          opam_file: '.'
           coq_version: ${{ matrix.coq_version }}
           ocaml_version: ${{ matrix.ocaml_version }}
 
@@ -51,7 +52,6 @@ jobs:
         image:
           - mathcomp/mathcomp:1.10.0-coq-8.10
           - mathcomp/mathcomp:1.10.0-coq-8.11
-          - mathcomp/mathcomp:1.11.0-coq-dev
           - mathcomp/mathcomp-dev:coq-dev
       max-parallel: 4
       fail-fast: false

coq-test.opam

@@ -0,0 +1,30 @@
+opam-version: "2.0"
+maintainer: "erik@martin-dorel.org"
+version: "dev"
+
+homepage: "https://github.com/erikmd/docker-coq-github-action-demo"
+dev-repo: "git+https://github.com/erikmd/docker-coq-github-action-demo.git"
+bug-reports: "https://github.com/erikmd/docker-coq-github-action-demo/issues"
+license: "MIT"
+
+synopsis: "Demo of docker-coq-action"
+description: """
+Demo of docker-coq-action.
+"""
+
+build: [
+  ["sh" "-c" "coq_makefile src/test.v -o Makefile2"]
+  [make "-j%{jobs}%" "-f" "Makefile2"]
+]
+install: [make "install" "-f" "Makefile2"]
+
+depends: [
+  "ocaml" {>= "4.05.0"}
+  "coq" {(>= "8.6") | (= "dev")}
+]
+
+tags: [
+]
+authors: [
+  "Erik Martin-Dorel"
+]

src/test.v

@@ -0,0 +1,6 @@
+Lemma id : forall A : Type, A -> A.
+Proof.
+exact (fun A (x : A) => x).
+Defined.
+
+Print id.