pycoq

pycoq copied to clipboard

We should provide a method for users to install the PyCoq package seamlessly.

It is not clear to me how the install flow should go, as I'm 100% unfamiliar with Python. As of now, PyCoq has to components:

• a .so library, built with a standard OCaml toolchain, which contains Coq + the PyCoq interface
• the setup.py and Python utility libraries [that build a Python package using pip3

I dunno if a pycoq opam package would be able to actually do the pip3 setup, and if that's "allowed" [note local OPAM switches, etc...]

On the other hand, I'm not sure how "external" deps are handled in the Python world.

On the other hand, I'm not sure how "external" deps are handled in the Python world.

External depedencies are usually written in a setup.py file and install automagically with pip install or conda install. e.g. https://github.com/brando90/ultimate-utils/blob/master/setup.py e.g. you can install my library by only doing pip install ultimate-utils (or in dev mode add the -e option pip install -e .` in the location of the setup.py file).

I don't know what the "official"/best way to do thins but my recommendation is that single pip install does everything -- including the installation of opam and that makefiles are not used. I bet most python ppl that are not super old have no idea what a makefile is.

The setup.py file a normal python file so it's turning complete and can execute all code. One could write all the opam commands needed to be executed there with the subprocess module and install absolutely everything from there -- including installing opam.

That's what I recommend.

How long would that thing take?

I'm OK with having a normal install, but I'd much prefer if when developing make was as fast as is in OCaml now (and cache friendly)

I assume it would take longer since you're running commands from python (but at least it would feel pythonic, to me at least) but honestly I don't know. I've personally never seen make being used with python. I've only learned about them recently because Ocaml and Coq use them. This is the challenge when combining awesome tools that weren't meant to be used together (?).

Do you have a pointer on what's the recommended Python + C stubs developer workflow?

When python is developed alone, do people compile anything at all?

I will ask one of my full time software developer friends (not just researcher) and see what he thinks and share it here. When I develop, I never compile anything (and if I do pip does it on it's own, I have seen bytecode stuff around but I never touch it or consciously create it). I personally fully embrace the interpreted nature of python and spend as much time developing & running code as a way to develop (e.g. I rarely insert code into my files that I've not already run in a debugger or console). To the extent that I abandoned TensorFlow which is compiled (from within python), and switched to PyTorch for ML/ANN development.

btw, with my suggested approach in compiling from the setup file, you can run the make if you want -- or any other terminal command. Though Idk if this is recommended, I admit.

I don't know either. Thanks for all the help.

Here the thing is that we def need to compile the OCaml parts, and they are output in _build/default , so hence the need to tell python that, I guess setting that in some variable of config would avoid you having to do the chdir.

I don't know either. Thanks for all the help.

Here the thing is that we def need to compile the OCaml parts, and they are output in _build/default , so hence the need to tell python that, I guess setting that in some variable of config would avoid you having to do the chdir.

hmmm...are you doing any of this in a python env? e.g. conda or pyenv? wondering if that is the issue. If that is set up properly you don't need to do hacky things in python to edit it's path or things like that. This is what it sounds is going on here...perhaps.