search

IBM / graph2tac

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

Mirek/predict nesting #133

Closed mirefek closed 1 year ago

mirefek commented 1 year ago

It is not finished yet but quite close to it. What remains:

so this is now waiting for the tests being merged into main. (or I could first merge Lasse's branch directly if it will take a while)

mirefek commented 1 year ago

All tests pass except hmodel

mirefek commented 1 year ago

I'm seeing quite a bit of outcommented code. Do you want to keep that?

I will remove the outcommented debug prints.

Also, is the sanity_check function expensive? If so, should it be behind a flag?

sanity_check is a functionality that was there also before, and I hope it should not be too expensive, so I will keep it. On the other hand, I plan to set paranoic = False as default for the DynamicDataServer.

LasseBlaauwbroek commented 1 year ago

(Sorry, I didn't read your comment about deleting debug code.)

mirefek commented 1 year ago

The code is already in virtually finished state. The only missing part is a functional hmodel test -- I already updated the hmodel code, and tested it (thanks, Jason) on the duplicate_identities test. Unfortunatelly, this test doesn't contain any global argument prediction so I cannot yet guarantee that it is working. On the other hand, since the only possible planned future changes are bugfixes, the code is ready to be thoroughly reviewed, @jasonrute , @LasseBlaauwbroek

mirefek commented 1 year ago

Works about the same with the updated version of coq-tactician-reinforce, I also tested with Set Tactician Neural Autocache. and looks to me as expected.

LasseBlaauwbroek commented 1 year ago

Great, no more problems with the bugs that existed before?

jasonrute commented 1 year ago

I'm still working through all the code. It is fairly complicated. The big thing I'm confused by is the following line: https://github.com/IBM/graph2tac/blob/bbe77e619a1f1043e95abf36c305d3b4e4b6abdf/graph2tac/tfgnn/predict.py#L227 If reserve is 0.5 (which is the default), doesn't this cause the array to shrink? And that isn't what we want. I'm very confused that this works and pasts our tests.

Edit: Never mind. I missed the +=.

mirefek commented 1 year ago

@LasseBlaauwbroek : I haven't encountered any issues. @jasonrute Yes :-). First I had there only multiplication but then it seemed to me that adding this is more fitting the parameter name reserve.

jasonrute commented 1 year ago

Great. Looks good to me! (And thanks for fixing the testing docs.).