Merge pull request #3 from uds-psl/ci

Added ci

.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

.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
+.merlin
+Makefile.coq
+Makefile.coq.conf

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

opam

@@ -0,0 +1,26 @@
+opam-version: "2.0"
+version: "dev"
+maintainer: "Yannick Forster <[email protected]>"
+authors: ["Sigurd Schneider <[email protected]>"
+          "Yannick Forster <[email protected]>"
+          "Fabian Kunze <[email protected]>"]
+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.
+"""