pycoq

pycoq copied to clipboard

why do we need os.chdir('_build/default')?

1

brando90

Data set for machine learning compatible with PyCoq

1

Hi everyone! I'm interested in trying out this Python-Coq interface. Thus I was curious -- what are coq data sets one can use with this PyCoq? Any recommendations? Ref: -...

brando90

Can CoqGym's data be used with PyCoq?

1

Can CoqGym's data be used with PyCoq? cross: https://github.com/princeton-vl/CoqGym/discussions/70

brando90

Stop using the protocol interpreter interface

1

As of now, PyCoq uses SerAPI interpreter interface; we should stop using it, and instead, generate the Coq object directly from a ML-style direct API. The reason SerAPI used an...

ejgallego

nixify

4

one take on this is in https://github.com/ejgallego/pycoq/pull/10 - However, @ejgallego said > I think also that opam2nix should not be used, but start from the coq-serapi derivation which is not...

quinn-dougherty

a `nix` build and testing infra

12

TODO: - fix everything so I can get the thing to run - implement some basic `pytest` stuff.

quinn-dougherty

Give the caller `namedtuple`; factor out the need for dictionaries

1

passing `dict`s is good enough for the machine learning in python community, so it's good enough for us. However, since we don't need _quite_ the flexibility in configs the machine...

quinn-dougherty

return objects should probably be dicts instead of nested 2-tuples

2

```python res = coq.add(some_command, opts) print(dict(res)) ``` ```shell {'Added': (6, {'fname': ('ToplevelInput', None), 'line_nb': 2, 'bol_pos': 1, 'line_nb_last': 2, 'bol_pos_last': 1, 'bp': 66, 'ep': 70}, ('NewTip', None)), 'Completed': None} {'CoqExn':...

quinn-dougherty

let `pytest` and `pytype` know about `pycoq.so` somehow, probably by doing some kind of `dune exec -- pytest`

1

In https://github.com/ejgallego/pycoq/pull/10 I decided to put `if __name__ == "__main__":` blocks in the test suite, instead of using test harness `pytest`, because I couldn't make `pytest` aware of the `pycoq`...

quinn-dougherty

Test suite

2

We need a test-suite, which will serve as a first form of documentation.

ejgallego