From 642cf2e172b2eeab4725d4266d808a2a9fb9bf88 Mon Sep 17 00:00:00 2001 From: Fabian Kunze Date: Mon, 16 Nov 2020 13:18:31 +0100 Subject: [PATCH 1/2] added ci & opam files --- .github/workflows/build.yml | 32 ++++++++++++++++++++++++++++++++ .gitignore | 8 ++++++-- opam | 26 ++++++++++++++++++++++++++ 3 files changed, 64 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/build.yml create mode 100644 opam diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..f4fa975 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,32 @@ +name: Test compilation + +on: [push, pull_request] + +jobs: + build: + runs-on: ubuntu-latest + steps: + + - name: Try to restore opam cache + id: opam-cache + uses: actions/cache@v2 + with: + path: "~/.opam" + key: opam-${{github.base_ref}}-${{github.ref}} + restore-keys: | + opam--refs/heads/${{github.base_ref}} + + - name: Install OCaml + uses: avsm/setup-ocaml@v1 + with: + ocaml-version: 4.07.1 + + - name: Checkout code + uses: actions/checkout@v2 + with: + fetch-depth: 1 + + - run: opam repo add coq-released https://coq.inria.fr/opam/released + - run: opam install . --deps-only --with-doc --with-test + + - run: opam exec -- make -j 2 all diff --git a/.gitignore b/.gitignore index 6c7e7d2..1850cb9 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,8 @@ Makefile.coq Makefile.coq.conf *.vo +*.vok +*.vos *.glob *~ *.v.d @@ -22,6 +24,8 @@ Makefile.coq.conf .merlin *.cmt *.cmti + src/smpl.ml -*.vok -*.vos \ No newline at end of file +.merlin +Makefile.coq +Makefile.coq.conf diff --git a/opam b/opam new file mode 100644 index 0000000..8821e5f --- /dev/null +++ b/opam @@ -0,0 +1,26 @@ +opam-version: "2.0" +version: "dev" +maintainer: "Yannick Forster " +authors: ["Sigurd Schneider " + "Yannick Forster " + "Fabian Kunze "] +homepage: "https://github.com/uds-psl/smpl" +bug-reports: "https://github.com/uds-psl/smpl/issues" +license: "MIT" +dev-repo: "git+https://github.com/uds-psl/smpl" +build: [make "-j%{jobs}%"] +install: [make "install"] +depends: [ + "ocaml" + "coq" { >= "8.12" & < "8.13~" } +] +synopsis: "Smpl: An Extensible Tactic for Coq" +description: """ +Smpl is useful for proof automation in Coq. Smpl provides named lists +of tactics to which tactics can be added with Coq commands. A special +tactic called 'smpl foo' executes the tactics in the lists named foo +in order, until one of them succeeds. Smpl works across modules by +merging tactics from all imports according to a priority number that +can be provided upon addition. Smpl thus allows to modify the behavior +of a tactic after it is defined in a convenient and modular way. +""" From 696d2e3a5790b54b03dd3629c32620884e547f6c Mon Sep 17 00:00:00 2001 From: Fabian Kunze Date: Mon, 16 Nov 2020 13:23:09 +0100 Subject: [PATCH 2/2] Updated readme --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index c2334ae..ac82fdf 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ # Coq Plugin smpl +![Test compilation](https://github.com/uds-psl/smpl/workflows/Test%20compilation/badge.svg) Smpl is useful for proof automation in Coq. Smpl provides named lists of tactics to which tactics can be added with Coq commands. A special @@ -26,7 +27,7 @@ The plugin is available for various versions of Coq in the different branches of ## Installation We provide an opam repository from which smpl can be installed. -To install from the opam repository for Coq 8.10.2 use the following +To install from the opam repository for Coq 8.10.2 and onwards use the following commands: opam repo add psl-opam-repository https://github.com/uds-psl/psl-opam-repository.git