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

Inference of SerAPI options due to changes in library bindings #37

Open a-gardner1 opened 1 year ago

a-gardner1 commented 1 year ago

Sometimes even if the directory structure does not change, the IQR flags do. We do not currently have a means to detect this situation as a health-check pre-build to trigger inference of SerAPI options.

The recommended approach is to grep Require statements from files in the project (preferably limited to those obtained via Project.get_file_list) and determine if the current IQR flags are reflected in the Require statements.

Completion of this should wait for #36 to be merged to reuse its function for obtaining Require statements per file.

a-gardner1 commented 1 year ago

This may be sufficiently covered by a new feature of cache extraction that will attempt to trigger option inference upon matching certain Coq error messages. See https://github.com/a-gardner1/coq-pearls/blob/f7ae3d74373bfa859dcc295b8b7f2705995d43dc/prism/data/extract_cache.py#L1455