search

IBM / graph2tac

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

Mirek/reindex #118

Closed jasonrute closed 1 year ago

jasonrute commented 1 year ago

Make the global argument and index into the global context instead of an absolute index. This will make our model more scalable in the end.

This quickly gets turned back to what it was before, but we will push it further back into the neural network.

jasonrute commented 1 year ago

@mirefek, the tests all run (no crashes), but they fail for me. Can you verify quickly that they pass for you. (In my upcoming changes I'll reduce the tolerance in hope that our tests will be more robust.)

jasonrute commented 1 year ago

Actually, I think this might fix the hmodel. 😄 At least, it makes this line make sense now: https://github.com/IBM/graph2tac/blob/b2779130fff223260b826c03e6c7b28437ce4289/graph2tac/loader/hmodel.py#L34

And it might explain the output of bounds bug I saw in the hmodel last week. Anyway, let's merge this now, and we can figure out if the hmodel is working in a bit.

mirefek commented 1 year ago

I think it is more complicated, in my simple test, the hmodel doesn't work nor in main, nor in this branch, so I guess it is fine to merge, and get hmodel working once we figure out how to do the indices well with the network.

jasonrute commented 1 year ago

Yes, you are right. I misunderstood what context meant here. Anyway, I'll merge now as is.