From 0ac92e9ee0f8337a79044709c3fd5582cdabc61f Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 20 Sep 2020 16:28:41 +0200 Subject: [PATCH 1/2] feat: Add another .v and .opam file --- coq-test.opam | 30 ++++++++++++++++++++++++++++++ src/test.v | 6 ++++++ 2 files changed, 36 insertions(+) create mode 100644 coq-test.opam create mode 100644 src/test.v diff --git a/coq-test.opam b/coq-test.opam new file mode 100644 index 0000000..1776147 --- /dev/null +++ b/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" +] diff --git a/src/test.v b/src/test.v new file mode 100644 index 0000000..d262023 --- /dev/null +++ b/src/test.v @@ -0,0 +1,6 @@ +Lemma id : forall A : Type, A -> A. +Proof. +exact (fun A (x : A) => x). +Defined. + +Print id. From 8dbd478bc3d5360cd8cc66b77781efb076b1b4b8 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 20 Sep 2020 16:29:55 +0200 Subject: [PATCH 2/2] Test the new docker-coq-action feature allowing "opam_file" folders --- .github/workflows/build-coq-demo.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/build-coq-demo.yml b/.github/workflows/build-coq-demo.yml index 284ceb9..bf0eaa2 100644 --- a/.github/workflows/build-coq-demo.yml +++ b/.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