IBM / graph2tac

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

Make hmodel test with aligned definitions in trace #136

Closed jasonrute closed 1 year ago

jasonrute commented 1 year ago

This adds tests which will hopefully help to fix current issues with the hmodel. The other hmodel server test doesn't have a trace where the definitions are aligned. This one does. That should make it possible to fix the hmodel and by making sure this test still passes.

It is still in my plan to fix the other traces, but this is faster so I'm starting with this.