Stream: PyCoq

Topic: how can i help


view this post on Zulip Quinn (Nov 04 2021 at 21:47):

For a start, we need handle errors correctly and to adhere to Python conventions. A large amount of feedback is required from Python experts as I am not familiar with Python myself at all.

I have some battle-forged python opinions, and can certainly throw do some devops and throw pytype, pytest, hypothesis, flake8 into any codebase. but can you point me to some code that you want a python expert to look at? a scenario where you suspect the error handling isn't ideal?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:50):

Hi @Quinn , that's amazing, thanks a lot for your help!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:50):

Actually we have fixed the error handling problem

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:51):

so I think the main point now is how to package PyCoq correctly so it can be submitted to PIP etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:51):

I am not very familiar with Python packaging

view this post on Zulip Quinn (Nov 04 2021 at 21:52):

ok

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:52):

The way PyCoq works is as follows:

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:53):

so I wonder how can we have a Python package to depend on an OCaml one

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:53):

The way we are working is that we specify the "coq" object as an OCaml module, then we add the methods for those

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:53):

so in a sense, the canonical API is defined in OCaml, this is a bit more convenient

view this post on Zulip Quinn (Nov 04 2021 at 21:53):

I wonder that too. I have some packaging experience with pypi but zilch with the opam ecosystem.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:54):

opam will just install the .so in the corresponding root

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:54):

opam root I mean, that can be in $home/.opam/$switch

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:54):

or also local to a directory in _opam

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:55):

opam supports several "switches" so you can have different ocaml installations with different versions etc...

view this post on Zulip Quinn (Nov 04 2021 at 21:55):

The thing is, my gut tells me (I haven't set up an environment to check) the IBM/pycoq pypi listing is something where if you pip install pycoq without the underlying ocaml situation under control, you might get into a scenario where the pip install works and code doesn't crash until runtime.

view this post on Zulip Quinn (Nov 04 2021 at 21:55):

That's an outcome that IMO is worse than not being on pypi at all.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:55):

ibm/pycoq has the same problem

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:55):

needs to have sertop installed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:56):

that is to say, both python bindings need to install Coq before they can be used

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:56):

ibm/pycoq needs sertop which gives access to Coq via an RPC protocol

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:56):

ejgallego/pycoq skips the RPC and provides access to Coq via Python's FFI [using a .so]

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:57):

So I dunno what's the best way here, but in a sense this is the same that for example depending on gtk

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:57):

or any C library that will be used by the Python code

view this post on Zulip Quinn (Nov 04 2021 at 22:01):

in the c or c++ dependency case, python will happily put you in a situation where a caller finds out by surprise that the dependency isn't there. So without experimenting I can guess a misconfigured opam, ocaml, sertop etc. will do the same for pycoq. An ideal solution would not have this property. Let me do some research into setup.py files real quick and see if we can dodge this property at that level.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:02):

Great thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:02):

If that's the case that's not too bad, we can just require that Coq is installed, and if it is not, we fail gracefully

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:03):

installing Coq is not too hard these days using opam, so I'd be reasonable to require setting up opam first

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:03):

I will try to do an OPAM release ASAP

view this post on Zulip Quinn (Nov 04 2021 at 22:04):

Meanwhile, I opened up this issue on the quite young python.on-nix.com project. The maintainer there might come up with a solution, which would be awesome.

view this post on Zulip Quinn (Nov 04 2021 at 22:07):

Meanwhile, it looks like your examples dir is for running code to read the output, but would you like unit and/or property tests?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:07):

Quinn said:

Meanwhile, I opened up this issue on the quite young python.on-nix.com project. The maintainer there might come up with a solution, which would be awesome.

Thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:08):

Quinn said:

Meanwhile, it looks like your examples dir is for running code to read the output, but would you like unit and/or property tests?

Definitively it would be great to set some testing infrastructure, I'd suggest to do only one small test for now, until we can push a better API

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:09):

The current API is just a Proof of Concept, but as I mentioned, we'll push a unified pyCoq / SerAPI soon

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:09):

then we can add a few more tests indeed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:09):

Feel free to open a Pull Request

view this post on Zulip Quinn (Nov 04 2021 at 22:10):

ok i'll get you set up to run pytest both locally and in ci and seed a testing infra that can be built on later

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:55):

Thanks @Quinn , just pushed a commit improving the packing on the OCaml side

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 22:55):

should make pyCoq much easier to install

view this post on Zulip Quinn (Nov 04 2021 at 22:58):

that's great. I failed my first attempt at make haha. Could be a number of things.

view this post on Zulip Quinn (Nov 04 2021 at 23:00):

did some snooping about a nix situation and filed a nixpkgs packaging request for ppx_python. I don't actually know how to add to nixpkgs myself yet.

view this post on Zulip Quinn (Nov 04 2021 at 23:03):

@Emilio Jesús Gallego Arias i'm not sure you pushed. it still says the latest commit was 28 days ago

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:05):

Sorry I just did it, had trouble with the submodule

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:05):

You don't need ppx_python with the latest commit

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:05):

It is a long story, but pycoq requires both ppx_import and ppx_python

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:07):

and due to some portability issues it was not possible to install both

view this post on Zulip Quinn (Nov 04 2021 at 23:07):

i'm not too familiar with submodules. do I cd coq-serapi; git checkout 7099b6c?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:08):

it seems to be broken, one sec

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:09):

I also struggle with submodules, something is off

view this post on Zulip Quinn (Nov 04 2021 at 23:10):

I ran cd coq-serapi; git submodule update --init --recursive which may have brought me to the wrong commit

view this post on Zulip Quinn (Nov 04 2021 at 23:15):

but that was a while ago

view this post on Zulip Quinn (Nov 04 2021 at 23:15):

I'm looking at this and thinking maybe we should write a .opam file? I've never used one of those before.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:15):

Ok, I think I've fixed it

view this post on Zulip Quinn (Nov 04 2021 at 23:15):

great

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:15):

There is already an opam file

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:16):

oh no, there is none

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:16):

sorry, will fix

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:16):

the submodule should work now, sorry for the hassle

view this post on Zulip Quinn (Nov 04 2021 at 23:17):

lmk when i should git fetch upstream

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:18):

Done

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:19):

I'm always confused with git submodules, maybe you need to do git submodules sync ?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:19):

Or maybe clone again? Not sure

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:20):

@Quinn need to go now, thanks for all the feedback

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 23:20):

will be around later today, for now the CI seems to work

view this post on Zulip Quinn (Nov 04 2021 at 23:21):

cool, see ya around

view this post on Zulip Quinn (Nov 05 2021 at 00:12):

why not put coq-serapi in pycoq.opam?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:13):

@Quinn it will happen eventually, but we didn't yet release a version of coq-serapi with python support

view this post on Zulip Quinn (Nov 05 2021 at 00:13):

oh, roger. thanks

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):

so now pycoq is building its own branch of coq-serapi

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):

OCaml has a build system called Dune

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):

which is very practical, as it allows you just to drop another project and things just work

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):

so hence the serapi submodule

view this post on Zulip Quinn (Nov 05 2021 at 00:15):

i'm thinking of writing a .nix file for coq-serapi

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:16):

@quinn there should be already one

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:16):

@Théo Zimmermann may tell you more

view this post on Zulip Quinn (Nov 05 2021 at 00:16):

but it might be easier to use fetchFromGitHub

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:17):

I'm not sure how Nix works, but IIANM, all the packages needed should be in place except for pythonlib and maybe pyml

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:18):

see https://github.com/ejgallego/coq-serapi/issues/241

view this post on Zulip Quinn (Nov 05 2021 at 00:57):

pyml is in neither coq-serapi.opam nor pycoq.opam

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:57):

@Quinn it is pulled by pythonlib

view this post on Zulip Quinn (Nov 05 2021 at 00:58):

roger

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:58):

That's actually a bad practice we do, sometimes we rely on implicit transitive deps

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:58):

That's been the case for a while, I should fix that in SerAPI / PyCoq

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:58):

Actually I have amended the opam file in a branch, now reads

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:59):

  "ppx_base"
  "ppxlib"              {           >= "0.15.0" & < "0.18.0" }
  "pyml"                {           >= "20200115"            }

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:59):

+ pythonlib

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 00:59):

So for the nix package, you need all deps of serapi + these ones

view this post on Zulip Quinn (Nov 05 2021 at 01:00):

I actually read that coq-serapi.opam and pycoq.opam are nearly identical

view this post on Zulip Quinn (Nov 05 2021 at 01:01):

pycoq.opam has pythonlib and coq-serapi.opam doesn't, but that's the difference

view this post on Zulip Quinn (Nov 05 2021 at 01:01):

which branch is that?

view this post on Zulip Quinn (Nov 05 2021 at 01:05):

So i still don't know how pycoq.so is generated nor how coq-serapi.install is generated. This is probably because I haven't gotten make to work. I think it has something to do with coq versioning on my system, based on the error message, the coq version that gets installed via the .opam file isn't overriding the other coq version I have on $PATH, in fact I have no evidence it's installing at all.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:06):

I've pushed a few more changes

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:06):

What message are you getting?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:06):

Quinn said:

pycoq.opam has pythonlib and coq-serapi.opam doesn't, but that's the difference

exactly

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:07):

the serapi branch for python support is this one

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:07):

https://github.com/ejgallego/coq-serapi/pull/240

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:08):

Quinn said:

So i still don't know how pycoq.so is generated nor how coq-serapi.install is generated. This is probably because I haven't gotten make to work. I think it has something to do with coq versioning on my system, based on the error message, the coq version that gets installed via the .opam file isn't overriding the other coq version I have on $PATH, in fact I have no evidence it's installing at all.

The generation of the .so file is just by a regular dune build command, see the makefile, same for python

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:08):

ocamlfind list will provide you a list of the things in scope

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:09):

I am not familiar with Nix (I struggle often with it), but there could be two potential problem sources:

view this post on Zulip Quinn (Nov 05 2021 at 01:10):

i'll check it out. ocamlfind list | grep coq is empty. I used this. PR is up in draft.

view this post on Zulip Quinn (Nov 05 2021 at 01:12):

eval $(opam env) put all the coq stuff in ocamlfind list | grep coq! but not coq.plugins.ring which is what I need.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):

what's your coq version?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):

beware it has to be 8.13 for this branch

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):

you can force opam to stay at a fixed version with opam pin add coq.8.13.1 etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):

or using the opam file opam install --deps-only .

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:14):

pin avoids upgrades tho

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:14):

Coq stuff is tricky anyways, I think you may have a bit better luck starting from the serapi derivation

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:14):

adding the missing stuff should be easy

view this post on Zulip Quinn (Nov 05 2021 at 01:15):

I know. my background system coq version is 8.12 but I was _hoping_ opam2nix would create a shell for me in which coqc --version is 8.13 since that's the one that's in the .opam file.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:16):

That particular error you get is due to the version then

view this post on Zulip Quinn (Nov 05 2021 at 01:16):

and opam-install --deps-only . says "Nothing to do"

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:16):

what does opam show coq say?

view this post on Zulip Quinn (Nov 05 2021 at 01:16):

which doesn't make sense, because coq in .opam file is 8.13

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:16):

but if you use the derivation for serapi, your background version will be the right one I understand, but not in opam

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:17):

maybe both nix and opam are providing the coq version?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:17):

likely you may want not to use opam if you are on nix

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:18):

I'm sure when the Coq Nix experts wake up they will be able to provide the right recipe maybe

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:18):

:)

view this post on Zulip Quinn (Nov 05 2021 at 01:18):

well, some nix/store/.../coq8.13... or something would be the which coqc if nix was working.

view this post on Zulip Quinn (Nov 05 2021 at 01:18):

yeah, i'd use the coqPackages.coq-serapi but we're using a non-main branch of coq-serapi

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:21):

can't you just pull the deps ?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:21):

for that derivation, so you would have the right coq, ppx toolchaing, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:21):

you could just add pyml ppx_base pythonlib and you would be ok I think

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):

pycoq is just coq-serapi extended a bit

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):

know what I mean? So maybe if you just clone the derivation, and tweak it a bit, that will produce a working setup

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):

I hope

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):

sorry for not being able to help with Nix

view this post on Zulip Quinn (Nov 05 2021 at 01:23):

does this .opam file look right, then?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:25):

The current one is a bit more refined https://github.com/ejgallego/pycoq/blob/v8.13/pycoq.opam

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:25):

you may want to rebase

view this post on Zulip Quinn (Nov 05 2021 at 01:29):

working on that now haha

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:30):

derivation for serapi is here in case it helps https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/serapi/default.nix

view this post on Zulip Quinn (Nov 05 2021 at 01:30):

is the correct submodule branch 8.13+pyml or 8.13?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:31):

8.13+pyml

view this post on Zulip Quinn (Nov 05 2021 at 01:31):

in any case, I had so many MCs in the submodule somehow that I had to rm -rf coq-serapi thinking a simple command would pull it back down since the data in .gitmodules is still there. one moment...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:31):

yeah sometimes is better to just do that

view this post on Zulip Quinn (Nov 05 2021 at 01:33):

quinn@Latitude-3340:~/Dropbox/Projects/misc-coq/pycoq$ cat .gitmodules
[submodule "coq-serapi"]
        path = coq-serapi
        url = https://github.com/ejgallego/coq-serapi.git
        branch = v8.13+pyml```

view this post on Zulip Quinn (Nov 05 2021 at 01:33):

nothing in git submodule help is working. not sync, not init, ....

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:33):

sometimes --force helps

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:34):

there is a bit of submodule state in .git

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 01:34):

gonna call it a night, thanks a lot for the efforts

view this post on Zulip Quinn (Nov 05 2021 at 01:35):

i'll get this thing built, you'll see!

view this post on Zulip Quinn (Nov 05 2021 at 01:35):

I need to learn ocaml packaging ecosystem better anyway

view this post on Zulip Quinn (Nov 05 2021 at 03:34):

lmao, gave up on the principles of isolation since opam2nix was having the disappearing coq mystery, just ran opam pin coq 8.13.1 or whatever... and pycoq built!

view this post on Zulip Quinn (Nov 05 2021 at 04:00):

68% optimistic that we can create some world where python users just pip install pycoq and get the opam crap for free

view this post on Zulip Quinn (Nov 05 2021 at 05:45):

pulls/10 is currently bottlenecked by telling pytest and pytype where the coq and pycoq library is, I tried dune exec -- pytest test/py and it didn't work either. I also tried cp -r test _build/default; dune exec -- pytest _build/default/test and it didn't work.

At this point it's sort of unfortunate that the nix attempted is piggybacked with this PR, there's too much different stuff going on with this PR because of the nix stuff. but I don't think it's worth backing it out.

view this post on Zulip Quinn (Nov 05 2021 at 05:46):

moreover, i opened this it's quite concerning to me. I don't know how this happened, must have something to do with ocaml-origin codegen? i have no idea.

view this post on Zulip Quinn (Nov 07 2021 at 15:10):

I don't understand dune exec -- python3

dune build test/py/unit/spec.py test/py/property/spec.py
dune exec -- python3 _build/default/test/py/unit/spec.py
Traceback (most recent call last):
  File "_build/default/test/py/unit/spec.py", line 1, in <module>
    import pycoq
  File "/home/quinn/.local/lib/python3.8/site-packages/pycoq/__init__.py", line 9, in <module>
    dll = PyDLL(f"{curdir}/pycoq.so", RTLD_GLOBAL)
  File "/usr/lib/python3.8/ctypes/__init__.py", line 373, in __init__
    self._handle = _dlopen(self._name, mode)
OSError: /home/quinn/.local/lib/python3.8/site-packages/pycoq/pycoq.so: cannot open shared object file: No such file or directory
make: *** [Makefile:28: pyci] Error 1

view this post on Zulip Quinn (Nov 07 2021 at 15:10):

Moreover I can't detect what happened between a little bit ago when things were basically working and now when I can't get examples to run

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):

See https://github.com/ejgallego/pycoq/pull/10#issuecomment-961893880 , in this case there is nothing telling dune to build pycoq.so

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):

so it fails, you need to do dune build first

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):

or write a rule

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):

the reason we use dune exec is such that the plugins env vars for Coq are properly setup

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):

compare env vs dune exec -- env

view this post on Zulip Quinn (Nov 07 2021 at 15:57):

dune build is definitely getting called.

view this post on Zulip Quinn (Nov 07 2021 at 16:00):

i reread your comment a couple times and it seems like it should add insight, but the actual behavior of dune exec -- isn't matching what I learned from your comment on my machine.

view this post on Zulip Quinn (Nov 07 2021 at 16:01):

see my Makefile targets pyci and $(BUILDDIR)/pycoq/$(PYNAME).so (which pyci depends on)

view this post on Zulip Quinn (Nov 07 2021 at 16:04):

before I run make clean,

$ ls _build/default/pycoq/
coq_init.ml  coq_init.mli  __init__.py  pycoq.ml  pycoq.mli  pycoq.so

the .so exists in the _build target dir that dune writes, it just doesn't exist in ~/.local/lib/python3.8/site-packages/pycoq, and why should it.

view this post on Zulip Quinn (Nov 07 2021 at 16:05):

one hypothesis was that eval $(opam env) needs to be ran from inside the Makefile

view this post on Zulip Quinn (Nov 07 2021 at 16:05):

but it hasn't seemed to help.

view this post on Zulip Quinn (Nov 07 2021 at 16:05):

also. Should I be doing dune clean instead of rm -rf _build?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:06):

Quinn said:

also. Should I be doing dune clean instead of rm -rf _build?

They are pretty similar

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:06):

Quinn said:

before I run make clean,

$ ls _build/default/pycoq/
coq_init.ml  coq_init.mli  __init__.py  pycoq.ml  pycoq.mli  pycoq.so

the .so exists in the _build target dir that dune writes, it just doesn't exist in ~/.local/lib/python3.8/site-packages/pycoq, and why should it.

Yeah I have no idea how the stuff in .loca/lib etc... works, that's pip territory

view this post on Zulip Quinn (Nov 07 2021 at 16:08):

exactly: pip is not communicating with dune correctly. I thought running dune exec -- pip3 ... would help, but it doesn't seem to have.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:08):

Not sure I get what the problem is, but note that _build/default is a private directory to dune, so never cp stuff there manually, in this case you _must_ declare a rule in dune with the cp action

view this post on Zulip Quinn (Nov 07 2021 at 16:09):

roger.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:09):

this is because dune will clean up the _build directory automatically to remove stale files, basically all files it doesn't know about, this is required in order to have things such as bisect work properly

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:10):

Quinn said:

exactly: pip is not communicating with dune correctly. I thought running dune exec -- pip3 ... would help, but it doesn't seem to have.

there is not communication indeed, how should they communicate? dune exec -- pip3 does little, as I mentioned, just sets some env vars, but it doesn't even build the stuff

view this post on Zulip Quinn (Nov 07 2021 at 16:10):

wait a minute... the cp into _build thing I did was on an older version of my Makefile, not the one I just pushed.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:10):

still there I think cp requirements.txt _build/default/requirements.txt && cp README.md _build/default/README.md

view this post on Zulip Quinn (Nov 07 2021 at 16:10):

is there a way to tell dune to do this? cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .

view this post on Zulip Quinn (Nov 07 2021 at 16:11):

oh I see.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:11):

Quinn said:

is there a way to tell dune to do this? cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .

My point is that this is likely wrong

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):

that is not a context free action, but has some dependencies

view this post on Zulip Quinn (Nov 07 2021 at 16:12):

you mean the dune exec i added is likely wrong?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):

no, I mean that depends on some stuff to be built before it is called

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):

so indeed you can write a rule for that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):

(rule
  (deps ...)
  (targets ...) ; whatever pips produces
  (action (progn (run python3 setup.py) (run pip3 install .)))

view this post on Zulip Quinn (Nov 07 2021 at 16:12):

the building target in my Makefile is this

        dune build $(SERAPI) pycoq/$(PYNAME).so pycoq/__init__.py setup.py
    cp requirements.txt _build/default/requirements.txt && cp README.md _build/default/README.md
    cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .
    eval $(shell opam env)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:13):

And the error is?

view this post on Zulip Quinn (Nov 07 2021 at 16:13):

sweet. where would I put that rule? in dune-project?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:13):

in dune

view this post on Zulip Quinn (Nov 07 2021 at 16:14):

it doesn't error, a later call to dune exec -- python3 _build/examples/ whatever.py fails

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:14):

what is that call supposed to do?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:14):

what's the error message

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:14):

I am not familiar with the directory

view this post on Zulip Quinn (Nov 07 2021 at 16:15):

one sec

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):

likely fails because whatever is run in the wrong cwd

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):

this I have no idea how to set the python path

view this post on Zulip Quinn (Nov 07 2021 at 16:15):

yes, that's what i was thinking.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):

if you put the python3 call in a dune rule

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):

it will be executed in the _Build/default

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:16):

it can even be sandboxed [important for caching build rules]

view this post on Zulip Quinn (Nov 07 2021 at 16:16):

right. so, normally what you can do is PYTHONPATH=../../ python3 foo.py to for example make python's cwd be ../../

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:16):

Indeed, so likely python3 foo will set the cwd to . not to _build/default so the .so file is not found

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:17):

tho it is hard to tell without seeing the error message

view this post on Zulip Quinn (Nov 07 2021 at 16:17):

Quinn said:
here

view this post on Zulip Quinn (Nov 07 2021 at 16:18):

i just regenerated it in my shell before i remmebered i had already sent it ,sorry for delay.

view this post on Zulip Quinn (Nov 07 2021 at 16:28):

did you want me to put that (rule in pycoq/dune or a new file in the root dir called dune?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:30):

Makes more sense in the root dir I guess?

view this post on Zulip Quinn (Nov 07 2021 at 16:31):

so a new file then?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:32):

Sure

view this post on Zulip Quinn (Nov 07 2021 at 16:32):

oh hey examples are working now

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:32):

nice :)

view this post on Zulip Quinn (Nov 07 2021 at 16:32):

they were working, then not working, now working again

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:33):

likely due to a missing dependnecy

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:33):

it takes some time to get used to a more strict dep setting if you are coming from make

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:33):

make is very lenient, as it never cleans stuff etc...

view this post on Zulip Quinn (Nov 07 2021 at 16:36):

well, i'd love to go full isolation with nix-shell --pure but the library i found that converts .opam files to .nix files wasn't playing nicely with coq

view this post on Zulip Quinn (Nov 07 2021 at 16:37):

I kinda despise make lmao but i've been learning it recently as I prepare to build a production coq codebase. it's so hard to be in coq without using make. Dune seems bit better, perhaps we should aim to dune everything.

view this post on Zulip Quinn (Nov 07 2021 at 16:39):

i mean the bottom line is my python isn't isolating properly.

view this post on Zulip Quinn (Nov 07 2021 at 16:48):

meanwhile, these started showing up on dune build

Error: Program js_of_ocaml not found in the tree or in PATH
 (context: default)
Hint: opam install js_of_ocaml-compiler
File "coq-serapi/sertop/dune", line 29, characters 63-72:
29 |  (libraries sertop ppx_deriving_yojson.runtime zarith_stubs_js jscoq_lib))
                                                                    ^^^^^^^^^
Error: Library "jscoq_lib" in _build/default/coq-serapi/jscoq/coq-js is
hidden (optional with unavailable dependencies).
Hint: try:
  dune external-lib-deps --missing @@default
File "coq-serapi/tests/sertop/dune", line 7, characters 0-95:
 7 | (rule
 8 |   (targets full_env.out)
 9 |   (mode promote)
10 |   (action (run gunzip %{dep:full_env.out.gz})))
Error: No rule found for coq-serapi/tests/sertop/full_env.out.gz```

view this post on Zulip Quinn (Nov 07 2021 at 16:48):

sorry i'm having so much trouble getting on my feet here!!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:49):

Oh, this is due to dune build trying to build all the artifact of coq-serapi including the js_of_ocaml stuff

view this post on Zulip Quinn (Nov 07 2021 at 16:49):

Quinn said: oh i think that was because i was running dune build with no arguments.

view this post on Zulip Quinn (Nov 07 2021 at 16:49):

which i don't need to do in practice

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:49):

Yup, that's an artifact of the inclusion of coq-serapi

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:50):

dune build works as dune build @all that's a bit too much here

view this post on Zulip Quinn (Nov 07 2021 at 16:55):

i don't understand why pycoq/dune is (libraries pythonlib coq-serapi.serapi_v8_13 coq-serapi.sertop_v8_12) but pycoq.opam lists more deps.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 20:43):

pycoq.opam lists set set of _all_ required deps

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 20:43):

as of now, this also includes the stuff needed by all the coq-serapi/*/dune files

view this post on Zulip Quinn (Nov 07 2021 at 20:46):

ah

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 20:47):

note that there is not a perfect match between the opam deps and dune deps

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 20:47):

people is working on making it indeed more related

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 20:48):

also there is a flag in dune "implicit_transitive_deps"

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 20:48):

which is related to what you ask, but as of now, it is a bit experimental, in the OCaml world transitive deps are quite implicit

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 20:48):

as a norm, but that may break stuff and it has actually

view this post on Zulip Quinn (Nov 07 2021 at 20:51):

fun

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:02):

I've pushed a commit to showcase how to run the tests with dune

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:08):

ok another commit pushing, illustrating the approach we discussed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:08):

I hope it helps

view this post on Zulip Quinn (Nov 07 2021 at 21:46):

thanks! this is great material. I was just learning more dune for a pure coq project today.

view this post on Zulip Quinn (Nov 07 2021 at 21:56):

(rule
 (alias pip-build)

dune build @pip-build doesn't show up in Makefile. should it?

view this post on Zulip Quinn (Nov 07 2021 at 21:56):

i can see how it might be redundant.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):

I added an alias to be able to run it

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):

As I'm learning about how the python stuff works myself

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):

so tests depend on pip-build

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):

or on the target build directory

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):

I dunno what's best, this is really in progress

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 21:59):

But I'm releasing the lock for now, so feel free to push it forward

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:00):

Now the tests fail due to other issues, the output is too precise, but they seem to be running fine, so that's good news

view this post on Zulip Quinn (Nov 07 2021 at 22:05):

that's great!

view this post on Zulip Quinn (Nov 07 2021 at 22:05):

yeah

view this post on Zulip Quinn (Nov 07 2021 at 22:05):

i'm fixing up my branch and catching it up too where you are

view this post on Zulip Quinn (Nov 07 2021 at 22:05):

I kinda manually added your new dune and abandoned most of the Makefile I had written and manually made it like your new one, but i didn't git rebase

view this post on Zulip Quinn (Nov 07 2021 at 22:10):

goals of PR currently are

  1. separate examples from test, tests should be an environment that passes/fails based more on "does it compile" whereas examples can reveal information about how to use the tool by running them.
  2. provide initial nix infrastructure (even if it doesn't actually work).
  3. lint, black, pytest, possibly pytype.

future PRs:

  1. make nix actually work
    separately

  2. migrate to tox for python-side stuff, might be the right call.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):

Cool, note that it is common in our world to also have output tests

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):

this is good to track changes, and dune supports this workflow natively

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):

and allows you to review the diff, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):

so in this sense, the current "tests" that check that we output what we should are not so bad

view this post on Zulip Quinn (Nov 07 2021 at 22:20):

roger

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:20):

but indeed clearly not enough

view this post on Zulip Quinn (Nov 07 2021 at 22:20):

good to keep in mind

view this post on Zulip Quinn (Nov 07 2021 at 22:20):

you said the overall software was a little unstable right now to have piles of unit or property tests just yet

view this post on Zulip Quinn (Nov 07 2021 at 22:21):

$ make examples
dune build @examples/run-examples
     python3 build
running build
running build_py
Error: Unable to resolve symlink
_build/default/examples/out/add_commutative.out
Error: Unable to resolve symlink
_build/default/examples/out/definitions_ast.out
Error: Unable to resolve symlink _build/default/examples/out/syntax_error.out
make: *** [Makefile:26: examples] Error 1```

(I changed the filenames in `examples`, triple checked that everything agrees across `dune` files)

view this post on Zulip Quinn (Nov 07 2021 at 22:21):

do i need to mkdir out manually?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):

That means the file examples/out/definitions_ast.out doesn't exist

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):

you need to touch it to boostrap the process indeed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):

maybe there is a better way

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):

the message is weird, let me check if it is better in dune master

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:26):

it says "symlink" due to an internal detail

view this post on Zulip Quinn (Nov 07 2021 at 22:26):

ok, yeah

view this post on Zulip Quinn (Nov 07 2021 at 22:27):

I don't think I mind just touch in Makefile

view this post on Zulip Quinn (Nov 07 2021 at 22:27):

for the time being

view this post on Zulip Quinn (Nov 07 2021 at 22:27):

to get us started

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):

out files have to be committed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):

they are the output reference

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):

so I mean, you only need to create them once

view this post on Zulip Quinn (Nov 07 2021 at 22:27):

roger.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):

or in this case rename

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:28):

?

view this post on Zulip Quinn (Nov 07 2021 at 22:28):

ah, so if .log files are writing perfectly fine, then i should just cp whatever.log out/whatever.out?

view this post on Zulip Quinn (Nov 07 2021 at 22:28):

wait do i have to touch out/whatever.out to _build/default or to the actual source?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:29):

You can copy, but also you can start with an empty file

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:29):

dune will tell you "the test failed with this diff"

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:29):

and you can run dune promote to accept the new output

view this post on Zulip Quinn (Nov 07 2021 at 22:29):

roger.

view this post on Zulip Quinn (Nov 07 2021 at 22:31):

every time i make clean/dune clean tho....

view this post on Zulip Quinn (Nov 07 2021 at 22:31):

not to mention ci

view this post on Zulip Quinn (Nov 07 2021 at 22:31):

the touch should be in Makefile, can even make a inCI target that only gets called in ci

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:37):

out is supposed to be the reference output

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 22:37):

so no need to touch it, it is supposed to be commited

view this post on Zulip Quinn (Nov 07 2021 at 22:39):

ok cool

view this post on Zulip Quinn (Nov 07 2021 at 22:39):

got it

view this post on Zulip Quinn (Nov 07 2021 at 23:09):

lmao it would appear that dune build @rule succeeds and dune build --verbose @rule fails. They both fail in fact, but one of them hides this fact.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:14):

The rule as such it is not failing, otherwise dune would print also in regular mode

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:14):

maybe the rule is ignoring something

view this post on Zulip Quinn (Nov 07 2021 at 23:15):

okk

view this post on Zulip Quinn (Nov 07 2021 at 23:15):

do we need opam install --deps-only . in ci if dune handles everything? I guess dune isn't ingesting .opam file so, the answer is yes?

view this post on Zulip Quinn (Nov 07 2021 at 23:18):

ok i think i'm ready, if the ci passes. have to fix mc's tho

view this post on Zulip Quinn (Nov 07 2021 at 23:18):

do you mind if i do it? the MC's are things like name changes, housekeeping

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:19):

Yes, dune only handles the build, not the package install

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):

of "global" ocaml libraries

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):

What's an MC?

view this post on Zulip Quinn (Nov 07 2021 at 23:20):

merge conflict.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):

oh indeed, please rebase

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):

and squash as needed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):

will review ASAP once you undraft

view this post on Zulip Quinn (Nov 07 2021 at 23:21):

hm I think the best thing to do is the web interface resolver, rebasing would be much worse. The thing is, it pushes commits to main prematurely when you use the web interface.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:22):

In Coq we always rebase and the workflow is actually good

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:22):

actually you may want to cherry-pick to different PRs

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:23):

if the title is accurate, the nix stuff is independent of the other adjustments, isn't it?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:24):

For sure you want to squash most of it

view this post on Zulip Quinn (Nov 07 2021 at 23:25):

what do you mean squash?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:26):

commit squashing

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:27):

so history doesn't include temporal and internal commits

view this post on Zulip Quinn (Nov 07 2021 at 23:28):

yeah

view this post on Zulip Quinn (Nov 07 2021 at 23:28):

roger

view this post on Zulip Quinn (Nov 07 2021 at 23:29):

what's the commit i should rebase from?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:31):

from master?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:32):

are you experienced with rebasing? If not let me know and I'll be happy to help

view this post on Zulip Quinn (Nov 07 2021 at 23:32):

ah, got it

view this post on Zulip Quinn (Nov 07 2021 at 23:32):

i've done it like 3 times... last time was march 2020 haha

view this post on Zulip Quinn (Nov 07 2021 at 23:32):

so i'm planning to review

view this post on Zulip Quinn (Nov 07 2021 at 23:33):

it's not master tho right it's v8.13

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):

indeed, sorry

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):

v8.13

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):

to rebase it is key to have a good User Interfae

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):

Interface

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):

I use magit, but there are many

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:34):

if you have to rebase with the command line interface you'll be in problems

view this post on Zulip Quinn (Nov 07 2021 at 23:34):

i have magit installed, now's a great time to actually use it's serious features

view this post on Zulip Quinn (Nov 07 2021 at 23:34):

so

view this post on Zulip Quinn (Nov 07 2021 at 23:35):

oh this is pretty straightforward

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):

IMVHO programming with rebasing requires a bit of thinking ahead as to how to structure the commits

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):

but pays off a lot in the long term

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):

in Coq we systematically rebase everything and IMHO has worked super well

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):

people do write commits that are quite "modular"

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):

so they can be foward/backwards ported easily

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):

but YMMV

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):

I did struggle with rebase a lot at first

view this post on Zulip Quinn (Nov 07 2021 at 23:40):

ok in magit

view this post on Zulip Quinn (Nov 07 2021 at 23:40):

Screenshot-from-2021-11-07-18-40-10.png i'm here, and i manually fixed the mc at the commit with message nixified

view this post on Zulip Quinn (Nov 07 2021 at 23:41):

how do i continue onwards, admitting in join and flipping it to done since i fixed everything

view this post on Zulip Quinn (Nov 07 2021 at 23:45):

ah, M-x git-rebase-continue

view this post on Zulip Quinn (Nov 07 2021 at 23:55):

once i've got it all worked out locally a git push origin<which is my fork> mybranch is acceptable to do with a fastforward?

view this post on Zulip Quinn (Nov 07 2021 at 23:58):

aaand i think my issue is a commit i was tryign to skip was a commit where i messed up the submodule

view this post on Zulip Quinn (Nov 08 2021 at 00:00):

woah, it looks like the MCs didn't change at all after I rebased

view this post on Zulip Quinn (Nov 08 2021 at 00:01):

just saw your comment.

view this post on Zulip Quinn (Nov 08 2021 at 00:03):

haha my rebase was in vein https://github.com/ejgallego/pycoq/pull/10#issuecomment-962707235 --- currently thinking of putting up three PRs freshly branching off v8.13 as you suggested.

view this post on Zulip Quinn (Nov 08 2021 at 00:06):

weird how the rebase process just duplicated all my commits, unless i did something wrong.

view this post on Zulip Quinn (Nov 08 2021 at 00:24):

well, I decided that since my commits weren't compositional enough I'm not gonna try to salvage the branch, and i'm instead going to make three unrelated branches, manually copy pasting some of the work i did. But doing better to isolate concerns and make atomic/compositional commits!

view this post on Zulip Quinn (Nov 08 2021 at 00:25):

btw, the build from your latest commit is failing


Last updated: May 20 2022 at 10:03 UTC