search

Radiance-Technologies / prism

Utilities for creating and curating a dataset for automated proof repair in the Coq Proof Assistant.
GNU Lesser General Public License v3.0
5 stars 2 forks source link

alignment utilities #21

Closed tom-p-reichel closed 2 years ago

tom-p-reichel commented 2 years ago

new file containing alignment utilities, documentation, and tests.

also, had to rename one of your utilities named "re.py", since that name seemed to clobber the standard library "re" module.

a-gardner1 commented 2 years ago

Why did you rename prism.util.re to prism.util.re_utils?

I didn't see the second sentence in your MR description. The rename should not be necessary; that implies to me that you have either not correctly installed the package or are running a script in an unconventional manner.

I'm not sure what your development environment is, but if you need help setting it up to avoid needing to rename, I'd be happy to help. You may take a look at the README in the root of the project for our expected environment.

tom-p-reichel commented 2 years ago

Ha, I usually do everything on the command line and I tend to be in the same working directory as files I'm working on, so a file called re.py is problematic as it overrides the standard library import. Even starting python in the same directory throws an exception. I realize now that's not an issue for anyone else so I'll just do a work-around and revert that change, whoops.

tom-p-reichel commented 2 years ago

I was not aware that I had write permissions in this repo, plus I forgot to change my default upstream, so that's merged by accident now.

Only change that was applied was adding alignment.py to a directory.

I could revert that change with a git push -f, but in general commands that edit history are dangerous so I'll hold off on that.

We can continue discussion here and that file can be deleted in a commit if desired, or merely updated with another pull request.

a-gardner1 commented 2 years ago

I also was not aware that you had write permissions :(

I'm not used to managing a private Github project. Apparently, permissions cannot be enforced for private repos without paying, so we'll have to just go by the honor system.

You do not need to revert it, even with git revert. We'll just work around it.