IBM / graph2tac

Graph-based neural tactic prediction models for Coq.
Apache License 2.0
8 stars 4 forks source link

Add ability to filter bad proof steps from the data loader #50

Open jasonrute opened 2 years ago

jasonrute commented 2 years ago

Add options to the data loader to filter out:

fidel-schaposnik commented 2 years ago

I've now implemented the first two items here. However, note that I've leaned on doing this at the TF-GNN level instead of the loader level, because I think we should stick to the useful conceptual separation:

Eventually, I'd like to clean up the loader from other stuff that is cluttering it and not being used (e.g. train/validation splits), but for now at least I think we should not add here higher-level functionality.

Anyway, maybe we can close this issue and keep #9 as a reminder of what is left?