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

Infer Opam Deps [WIP] #36

Closed tom-p-reichel closed 1 year ago

tom-p-reichel commented 1 year ago

TODO:

a-gardner1 commented 1 year ago

I think you might need to rebase on main

a-gardner1 commented 1 year ago

TODO:

  • figure out why yml doesn't get added to pip package.
  • import yml from pip package install location rather than make weird assumption about working dir.

I would just place the yaml in the prism.util.opam directory and define a constant _MAPPING_DATA_PATH = pathlib.Path(__file__).parent / "logical_mapping.yml" in prism.util.opam.mappings. I don't think it belongs in the dataset directory since it is an integral part of the package whereas the dataset directory defines items that can be used with the package to work with a specific dataset.

tom-p-reichel commented 1 year ago

Somehow I picked up a commit by you that wasn't on the main branch that edited cache extraction. Edited it out.

tom-p-reichel commented 1 year ago

OK, added another check to filter out false positives (Import doesn't seem to be able to import 3rd party libraries without at least two parts-- though mathcomp.algebra.matrix exists, it wouldn't import it if you asked for matrix without providing at least mathcomp as a prefix).

Yaml file has a proper home in the package now and we use Project's run instead of seutil.

a-gardner1 commented 1 year ago

Thanks. Doesn't look like it will get merged today, but wanted to let you know of some refactoring I'll be doing before it is: I'm going to pull out the grepping of require statements into its own function that can be used for other purposes (for example, inferring staleness of SerAPI options by not finding a bound library in any imports).

We also recently discovered that we may want to strace more things in the near future. For example, options given to coqc like -w +ident (which corresponds to Vernacular Set Warnings +ident) can affect the execution of a file and impact whether something is considered an error in need of repair, but these options cannot be given in the same form to sertop. This can produce a discrepancy between behavior when one builds versus extracts.