a nix build and testing infra

.flake8

@@ -0,0 +1,6 @@
+[flake8]
+# ignore F401 is essential until we figure out what's up with `import pycoq`
+ignore = F401
+max-line-length = 100
+exclude = .git,__pycache__,docs/source/conf.py,old,build,dist
+max-complexity = 10

.github/workflows/ci.yml

@@ -1,4 +1,4 @@
-name: CI
+name: PyCoq CI
 
 on:
   push:
@@ -17,12 +17,14 @@ jobs:
       fail-fast: false
       matrix:
         ocaml-version: [4.11.1, 4.12.0]
+        python-version: [3.6, 3.7, 3.8, 3.9, 3.10]
+        os: [ubuntu-20.04]
     env:
       OPAMJOBS: "2"
       OPAMROOTISOK: "true"
       OPAMYES: "true"
       NJOBS: "2"
-    runs-on: ubuntu-latest
+    runs-on: ${{ matrix.os }}
 
     steps:
       - uses: actions/checkout@v2
@@ -32,19 +34,25 @@ jobs:
         uses: avsm/setup-ocaml@v1
         with:
           ocaml-version: ${{ matrix.ocaml-version }}
+      - name: Set up Python ${{ matrix.python-version }}
+        uses: actions/setup-python@v2
+        with:
+          python-version: ${{ matrix.python-version }}
       - name: OPAM dependencies setup
         run: |
           opam repos add coq-released http://coq.inria.fr/opam/released
           opam config set-global jobs $NJOBS
           opam install --deps-only .
-          opam install pythonlib
           # Disabled due to vendoring
           # opam install pythonlib ppx_python
           # opam pin add ppx_python https://github.com/ejgallego/ppx_python.git#fixup
           opam list
-      - name: Build and Test PyCoq
+      - name: Build PyCoq
         run: |
           set -e
           eval $(opam env)
-          make
-          make test
+          make build_pycoq
+      - name: Validate examples
+        run: make examples
+      - name: Lint, typecheck, and test python
+        run: make pyci

.gitignore

@@ -1,3 +1,7 @@
 __pycache__
 _build
 *~
+result
+.pytype
+pycoq.egg-info/
+.hypothesis

.gitmodules

@@ -1,4 +1,3 @@
 [submodule "coq-serapi"]
 	path = coq-serapi
 	url = https://github.com/ejgallego/coq-serapi.git
-	branch = v8.13+pyml

Makefile

@@ -1,18 +1,45 @@
-.PHONY: python help
+.PHONY: build_pycoq help
 
 PYNAME=pycoq
 SERAPI=coq-serapi/coq-serapi.install
 
 # coq-serapi.install is required so plugins are in place [runtime dep]
-python:
+build_pycoq:
 	dune build $(SERAPI) pycoq/$(PYNAME).so pycoq/__init__.py setup.py
-	( cd _build/default && python3 setup.py build && pip3 install . )
+	cp requirements.txt _build/default/requirements.txt && cp README.md _build/default/README.md
+	cd _build/default && python3 setup.py build && pip3 install .
 
-test:
-	dune build examples/test.py examples/test2.py examples/error.py
-	dune exec -- python3 _build/default/examples/test.py
-	dune exec -- python3 _build/default/examples/test2.py
-	dune exec -- python3 _build/default/examples/error.py
+examples: build_pycoq
+	dune build examples/add_commutative.py examples/definitions_ast.py examples/syntax_error.py
+	dune exec -- python3 _build/default/examples/add_commutative.py
+	dune exec -- python3 _build/default/examples/definitions_ast.py
+	dune exec -- python3 _build/default/examples/syntax_error.py
+
+pyci: build_pycoq
+	pip install .[dev]
+	black .
+	flake8 .
+	pytype .
+	pytest testpy
+
+nix_build_pycoq:
+	nix-build nix/opam2nix.nix
+	./result/bin/opam2nix resolve --ocaml-version 4.12.0 ./pycoq.opam --dest nix/opam-selection.nix
+	nix-shell nix/default.nix --run "eval $(opam env)"
+	nix-shell nix/default.nix --run "dune build $(SERAPI) pycoq/$(PYNAME).so pycoq/__init__.py setup.py"
+	nix-shell nix/default.nix --run "cd _build/default && python3 setup.py build && pip3 install ."
+
+nix_examples: nix_build_pycoq
+	nix-shell nix/default.nix --run "dune build examples/add_commutative.py examples/definitions_ast.py examples/syntax_error.py"
+	nix-shell nix/default.nix --run "dune exec -- python3 _build/default/examples/add_commutative.py"
+	nix-shell nix/default.nix --run "dune exec -- python3 _build/default/examples/definitions_ast.py"
+	nix-shell nix/default.nix --run "dune exec -- python3 _build/default/examples/syntax_error.py"
+
+allpy: build_pycoq pyci examples
 
 help:
-	@echo Nothing to display
+	@echo "If you have nix installed, try 'make nix_examples'. Else, try 'make examples'."
+
+clean:
+	rm -rf _build
+	rm -r .pytype

examples/add_commutative.py

@@ -0,0 +1,42 @@
+import pycoq  # the thing breaks if this isn't imported, even tho it's not invoked
+import coq
+
+if __name__ == "__main__":
+    # Some common definitions we'll use
+    ppopts = {
+        "pp_format": ("PpSer", None),
+        "pp_depth": 1000,
+        "pp_elide": "...",
+        "pp_margin": 90,
+    }
+
+    # Add a full document chunk [mainly parsing]
+    opts = {"newtip": None, "ontop": 1, "lim": 20}
+    res = coq.add(
+        """
+        Lemma addnC n m : n + m = m + n. Proof. now induction n; simpl; auto; rewrite IHn. Qed.
+    """,
+        opts,
+    )
+
+    # Check the proof.
+    res = coq.exec(5)
+
+    # We can show the goals at the tactic point
+    opts = {"limit": 100, "preds": [], "sid": 3, "pp": ppopts, "route": 0}
+    cmd = ("Goals", None)
+    res = coq.query(opts, cmd)
+    print(res)
+
+    # We can also output the ast for example, of the main tactic in our
+    # document
+    opts = {"limit": 100, "preds": [], "sid": 3, "pp": ppopts, "route": 0}
+    cmd = ("Ast", None)
+    res_ast = coq.query(opts, cmd)
+    print(res)
+
+    # Such AST can be actually pretty-printed
+    obj = res[0][1][0][0]
+    opts = {"pp": {"pp_format": ("PpStr", None)}}
+    res = coq.print(obj, opts)
+    print(res)

examples/definitions_ast.py

@@ -0,0 +1,36 @@
+import pycoq  # the thing breaks if this isn't imported, even tho it's not invoked
+import coq
+
+if __name__ == "__main__":
+
+    print("==> Adding a sentence")
+    opts = {"newtip": 2, "ontop": 1, "lim": 10}
+    res = coq.add("Definition a := 3.", opts)
+    print(res)
+
+    print("==> Adding another sentence")
+    opts = {"newtip": 3, "ontop": 2, "lim": 10}
+    res = coq.add("Definition b := 2.", opts)
+    print(res)
+
+    print("==> Checking the second sentence")
+    res = coq.exec(3)
+    print(res)
+
+    print("==> Printing the AST")
+    ppopts = {
+        "pp_format": ("PpSer", None),
+        "pp_depth": 1000,
+        "pp_elide": "...",
+        "pp_margin": 90,
+    }
+    opts = {"limit": 100, "preds": [], "sid": 3, "pp": ppopts, "route": 0}
+    cmd = ("Ast", None)
+    res = coq.query(opts, cmd)
+    print(res)
+
+    print("==> Formatting the AST")
+    obj = res[0][1][0][0]
+    opts = {"pp": {"pp_format": ("PpStr", None)}}
+    res = coq.print(obj, opts)
+    print(res)

examples/syntax_error.py

@@ -0,0 +1,9 @@
+import pycoq  # the thing breaks if this isn't imported, even tho it's not invoked
+import coq
+
+if __name__ == "__main__":
+
+    # parsing error
+    opts = {"newtip": None, "ontop": None, "lim": 10}
+    res = coq.add("Definition a := .", opts)
+    print(res)

nix/README.md

@@ -0,0 +1,3 @@
+# Currently (11-05-2021) not working.
+
+`opam2nix` has a mysterious disappearing `coq`. that's blocking actual isolation and reproducibility. 

nix/default.nix

@@ -0,0 +1,11 @@
+{ pkgs ? import ./pkgs.nix {}
+, opam2nix ? import ./opam2nix.nix {}
+}:
+let
+  ocaml = pkgs.ocaml;
+  selection = opam2nix.build {
+    inherit ocaml;
+    selection = ./opam-selection.nix;
+    src = ../.;
+  };
+in selection.pycoq