Add CI

.github/workflows/coq.yml

@@ -0,0 +1,34 @@
+name: Coq
+
+on:
+  push:
+    branches: ["main"]
+  pull_request:
+    branches: ["main"]
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+      - name: Download Git submodules
+        run: git submodule update --init --recursive
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: coqorg/coq:8.17-ocaml-4.14-flambda
+          custom_script: |
+            startGroup "Install dependencies"
+              opam install -y --deps-only CoqOfPython/coq-of-python.opam
+            endGroup
+            startGroup "Set the rights"
+              sudo chown -R $(whoami) .
+            endGroup
+            startGroup "Compile Coq translations"
+              cd CoqOfPython
+              make
+              cd ..
+            endGroup

CoqOfPython/coq-of-python.opam

@@ -0,0 +1,23 @@
+opam-version: "2.0"
+name: "coq-of-python"
+version: "0.1"
+synopsis: "Coq of Python"
+description: """
+Formal verification for Python by translation to the proof system Coq
+"""
+maintainer: "Guillaume Claret <[email protected]>"
+authors: [
+  "Formal Land <[email protected]>"
+]
+license: "MIT"
+homepage: "https://github.com/formal-land/coq-of-python"
+bug-reports: "https://github.com/formal-land/coq-of-python/issues"
+dev-repo: "git+https://github.com/formal-land/coq-of-python.git"
+depends: [
+  "ocaml" {>= "4.08"}
+  "coq" {>= "8.17.1" & < "8.18"}
+  "coq-hammer" {>= "1.3.2+8.17" & < "1.3.2+8.18"}
+]
+build: [
+  [make]
+]