Rename test to examples

.github/workflows/ci.yml

@@ -1,4 +1,4 @@
-name: CI
+name: PyCoq CI
 
 on:
   push:
@@ -42,9 +42,13 @@ jobs:
           # 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 install
+      - name: Validate diff checks of `examples`
+        run: |
+          set -e
+          eval $(opam env)
+          make examples

Makefile

@@ -1,20 +1,31 @@
-.PHONY: help build install test clean
+##
+# PyCoq
+#
+# @Makefile
+# @version 0.1
 
 PYNAME=pycoq
 SERAPI=coq-serapi/coq-serapi.install
+BUILDDIR=_build/default
+
+.PHONY: help build install test clean
+build: $(BUILDDIR)/pycoq/$(PYNAME).so
+
 
 help:
-	@echo targets {build,python,test,clean}
+	@echo targets {build,install,examples,clean}
 
 # coq-serapi.install is required so plugins are in place [runtime dep]
-build:
+$(BUILDDIR)/pycoq/$(PYNAME).so:
 	dune build $(SERAPI) pycoq/$(PYNAME).so
 
-install:
+install: $(BUILDDIR)/pycoq/$(PYNAME).so
 	dune build @pip-install
 
-test:
-	dune build @examples/runtest
+examples: $(BUILDDIR)/pycoq/$(PYNAME).so install
+	dune build @examples/run-examples
 
 clean:
-	@echo Nothing to display
+	dune clean
+
+# end

README.md

@@ -45,7 +45,9 @@ in the OPAM repository we have vendored it in the SerAPI branch we use.
 
 Once the right dependencies have been installed, you can do:
 ```
-$ make && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py
+$ git clone git@github.com:ejgallego/pycoq.git
+$ git submodule update 
+$ make examples
 ```
 
 If you want an interactive environment, use:

examples/dune

@@ -1,44 +1,44 @@
 (rule
  (deps
-  (:test-file test.py)
+  (:test-file definitions_ast.py)
   (package coq-serapi)
    ../build)
- (targets test.log)
+ (targets definitions_ast.log)
  (action
    (with-outputs-to %{targets}
     (setenv PYTHONPATH ../build/lib
      (run python3 %{test-file})))))
 
 (rule
  (deps
-  (:test-file test2.py)
+  (:test-file add_commutative.py)
   (package coq-serapi)
    ../build)
- (targets test2.log)
+ (targets add_commutative.log)
  (action
    (with-outputs-to %{targets}
     (setenv PYTHONPATH ../build/lib
      (run python3 %{test-file})))))
 
 (rule
  (deps
-  (:test-file error.py)
+  (:test-file syntax_error.py)
   (package coq-serapi)
    ../build)
- (targets error.log)
+ (targets syntax_error.log)
  (action
    (with-outputs-to %{targets}
     (setenv PYTHONPATH ../build/lib
      (run python3 %{test-file})))))
 
 (rule
- (alias runtest)
- (action (diff out/test.out test.log)))
+ (alias run-examples)
+ (action (diff out/definitions_ast.out definitions_ast.log)))
 
 (rule
- (alias runtest)
- (action (diff out/test2.out test2.log)))
+ (alias run-examples)
+ (action (diff out/add_commutative.out add_commutative.log)))
 
 (rule
- (alias runtest)
- (action (diff out/error.out error.log)))
+ (alias run-examples)
+ (action (diff out/syntax_error.out syntax_error.log)))

examples/out/test2.out → examples/out/add_commutative.out

@@ -1,32 +1,31 @@
-file_loaded: Coq.Init.Prelude, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Prelude.vo
-file_loaded: Coq.Init.Notations, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Notations.vo
-file_loaded: Coq.Init.Ltac, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Ltac.vo
-file_loaded: Coq.Init.Logic, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Logic.vo
-file_loaded: Coq.Init.Datatypes, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Datatypes.vo
-file_loaded: Coq.Init.Logic_Type, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Logic_Type.vo
-file_loaded: Coq.Init.Specif, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Specif.vo
-file_loaded: Coq.Init.Decimal, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Decimal.vo
-file_loaded: Coq.Init.Hexadecimal, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Hexadecimal.vo
-file_loaded: Coq.Init.Number, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Number.vo
-file_loaded: Coq.Init.Nat, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Nat.vo
-file_loaded: Coq.Init.Byte, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Byte.vo
-file_loaded: Coq.Init.Numeral, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Numeral.vo
-file_loaded: Coq.Init.Peano, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Peano.vo
-file_loaded: Coq.Init.Wf, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Wf.vo
-file_loaded: Coq.Init.Tactics, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Tactics.vo
-file_loaded: Coq.Init.Tauto, /home/egallego/.opam/dev-coq-pycoq/lib/coq/theories/Init/Tauto.vo
+file_loaded: Coq.Init.Prelude, /home/quinn/.opam/default/lib/coq/theories/Init/Prelude.vo
+file_loaded: Coq.Init.Notations, /home/quinn/.opam/default/lib/coq/theories/Init/Notations.vo
+file_loaded: Coq.Init.Ltac, /home/quinn/.opam/default/lib/coq/theories/Init/Ltac.vo
+file_loaded: Coq.Init.Logic, /home/quinn/.opam/default/lib/coq/theories/Init/Logic.vo
+file_loaded: Coq.Init.Datatypes, /home/quinn/.opam/default/lib/coq/theories/Init/Datatypes.vo
+file_loaded: Coq.Init.Logic_Type, /home/quinn/.opam/default/lib/coq/theories/Init/Logic_Type.vo
+file_loaded: Coq.Init.Specif, /home/quinn/.opam/default/lib/coq/theories/Init/Specif.vo
+file_loaded: Coq.Init.Decimal, /home/quinn/.opam/default/lib/coq/theories/Init/Decimal.vo
+file_loaded: Coq.Init.Hexadecimal, /home/quinn/.opam/default/lib/coq/theories/Init/Hexadecimal.vo
+file_loaded: Coq.Init.Number, /home/quinn/.opam/default/lib/coq/theories/Init/Number.vo
+file_loaded: Coq.Init.Nat, /home/quinn/.opam/default/lib/coq/theories/Init/Nat.vo
+file_loaded: Coq.Init.Byte, /home/quinn/.opam/default/lib/coq/theories/Init/Byte.vo
+file_loaded: Coq.Init.Numeral, /home/quinn/.opam/default/lib/coq/theories/Init/Numeral.vo
+file_loaded: Coq.Init.Peano, /home/quinn/.opam/default/lib/coq/theories/Init/Peano.vo
+file_loaded: Coq.Init.Wf, /home/quinn/.opam/default/lib/coq/theories/Init/Wf.vo
+file_loaded: Coq.Init.Tactics, /home/quinn/.opam/default/lib/coq/theories/Init/Tactics.vo
+file_loaded: Coq.Init.Tauto, /home/quinn/.opam/default/lib/coq/theories/Init/Tauto.vo
 Processing in master
 Processed
 🐓🐍🐓🐍 Coq's initialization complete 🐍🐓🐍🐓
 Processing in master
-575357:master:0] STM: 5: proof addnC: synch (cause: policy)
+34784:master:0] STM: 5: proof addnC: synch (cause: policy)
 Processing in master
 Processing in master
 Processing in master
 Processed
 Processed
 Processed
-sh: 1: dot: not found
 Processed
 Processed
 Processed

examples/out/definitions_ast.out

@@ -0,0 +1,35 @@
+file_loaded: Coq.Init.Prelude, /home/quinn/.opam/default/lib/coq/theories/Init/Prelude.vo
+file_loaded: Coq.Init.Notations, /home/quinn/.opam/default/lib/coq/theories/Init/Notations.vo
+file_loaded: Coq.Init.Ltac, /home/quinn/.opam/default/lib/coq/theories/Init/Ltac.vo
+file_loaded: Coq.Init.Logic, /home/quinn/.opam/default/lib/coq/theories/Init/Logic.vo
+file_loaded: Coq.Init.Datatypes, /home/quinn/.opam/default/lib/coq/theories/Init/Datatypes.vo
+file_loaded: Coq.Init.Logic_Type, /home/quinn/.opam/default/lib/coq/theories/Init/Logic_Type.vo
+file_loaded: Coq.Init.Specif, /home/quinn/.opam/default/lib/coq/theories/Init/Specif.vo
+file_loaded: Coq.Init.Decimal, /home/quinn/.opam/default/lib/coq/theories/Init/Decimal.vo
+file_loaded: Coq.Init.Hexadecimal, /home/quinn/.opam/default/lib/coq/theories/Init/Hexadecimal.vo
+file_loaded: Coq.Init.Number, /home/quinn/.opam/default/lib/coq/theories/Init/Number.vo
+file_loaded: Coq.Init.Nat, /home/quinn/.opam/default/lib/coq/theories/Init/Nat.vo
+file_loaded: Coq.Init.Byte, /home/quinn/.opam/default/lib/coq/theories/Init/Byte.vo
+file_loaded: Coq.Init.Numeral, /home/quinn/.opam/default/lib/coq/theories/Init/Numeral.vo
+file_loaded: Coq.Init.Peano, /home/quinn/.opam/default/lib/coq/theories/Init/Peano.vo
+file_loaded: Coq.Init.Wf, /home/quinn/.opam/default/lib/coq/theories/Init/Wf.vo
+file_loaded: Coq.Init.Tactics, /home/quinn/.opam/default/lib/coq/theories/Init/Tactics.vo
+file_loaded: Coq.Init.Tauto, /home/quinn/.opam/default/lib/coq/theories/Init/Tauto.vo
+Processing in master
+Processed
+🐓🐍🐓🐍 Coq's initialization complete 🐍🐓🐍🐓
+Processing in master
+Processing in master
+Processed
+Processed
+Processed
+==> Adding a sentence
+[('Added', (2, {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 0, 'ep': 18}, ('NewTip', None))), ('Completed', None)]
+==> Adding another sentence
+[('Added', (3, {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 0, 'ep': 18}, ('NewTip', None))), ('Completed', None)]
+==> Checking the second sentence
+[('Completed', None)]
+==> Printing the AST
+[('ObjList', ([('CoqAst', ({'v': {'control': [], 'attrs': [], 'expr': ('VernacDefinition', ((('NoDischarge', None), ('Definition', None)), ({'v': ('Name', (('Id', ('b',)),)), 'loc': {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 11, 'ep': 12}}, None), ('DefineBody', ([], None, {'v': ('CPrim', (('Number', ((('SPlus', None), {'int': '2', 'frac': '', 'exp': ''}),)),)), 'loc': {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 16, 'ep': 17}}, None))))}, 'loc': {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 0, 'ep': 18}},))],)), ('Completed', None)]
+==> Formatting the AST
+[('ObjList', ([('CoqString', ('Definition b := 2.',))],)), ('Completed', None)]

examples/out/syntax_error.out

@@ -0,0 +1,21 @@
+file_loaded: Coq.Init.Prelude, /home/quinn/.opam/default/lib/coq/theories/Init/Prelude.vo
+file_loaded: Coq.Init.Notations, /home/quinn/.opam/default/lib/coq/theories/Init/Notations.vo
+file_loaded: Coq.Init.Ltac, /home/quinn/.opam/default/lib/coq/theories/Init/Ltac.vo
+file_loaded: Coq.Init.Logic, /home/quinn/.opam/default/lib/coq/theories/Init/Logic.vo
+file_loaded: Coq.Init.Datatypes, /home/quinn/.opam/default/lib/coq/theories/Init/Datatypes.vo
+file_loaded: Coq.Init.Logic_Type, /home/quinn/.opam/default/lib/coq/theories/Init/Logic_Type.vo
+file_loaded: Coq.Init.Specif, /home/quinn/.opam/default/lib/coq/theories/Init/Specif.vo
+file_loaded: Coq.Init.Decimal, /home/quinn/.opam/default/lib/coq/theories/Init/Decimal.vo
+file_loaded: Coq.Init.Hexadecimal, /home/quinn/.opam/default/lib/coq/theories/Init/Hexadecimal.vo
+file_loaded: Coq.Init.Number, /home/quinn/.opam/default/lib/coq/theories/Init/Number.vo
+file_loaded: Coq.Init.Nat, /home/quinn/.opam/default/lib/coq/theories/Init/Nat.vo
+file_loaded: Coq.Init.Byte, /home/quinn/.opam/default/lib/coq/theories/Init/Byte.vo
+file_loaded: Coq.Init.Numeral, /home/quinn/.opam/default/lib/coq/theories/Init/Numeral.vo
+file_loaded: Coq.Init.Peano, /home/quinn/.opam/default/lib/coq/theories/Init/Peano.vo
+file_loaded: Coq.Init.Wf, /home/quinn/.opam/default/lib/coq/theories/Init/Wf.vo
+file_loaded: Coq.Init.Tactics, /home/quinn/.opam/default/lib/coq/theories/Init/Tactics.vo
+file_loaded: Coq.Init.Tauto, /home/quinn/.opam/default/lib/coq/theories/Init/Tauto.vo
+Processing in master
+Processed
+🐓🐍🐓🐍 Coq's initialization complete 🐍🐓🐍🐓
+[('CoqExn', ({'loc': {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 16, 'ep': 17}, 'stm_ids': None, 'backtrace': False, 'exn': None, 'pp': ('Pp_glue', ([('Pp_glue', ([],)), ('Pp_box', (('Pp_hovbox', (0,)), ('Pp_glue', ([('Pp_string', ('Syntax error: ',)), ('Pp_string', ("[reduce] expected after ':=' (in [def_body])",)), ('Pp_string', ('.',))],))))],)), 'str': "Syntax error: [reduce] expected after ':=' (in [def_body])."},)), ('Completed', None)]