The recent (as of about a week ago) re-parameterization of Learner in learners.v to support kernel perceptrons has temporarily broken the MLCert/NNCert build process: the generated oracle learners now need to take an additional (unused) argument in order to typecheck.
Until this issue is resolved, a temporary fix is to revert your local repo to commit 2ea101e71c6ca404407e95bbaf3bbac90bf1255f by doing:
This was resolved by the recent reversion and manual merge of kernel_perceptron. The remaining issue (which Robin is working on) is to manually merge the hs/KPerceptron.hs test harness.
The recent (as of about a week ago) re-parameterization of Learner in learners.v to support kernel perceptrons has temporarily broken the MLCert/NNCert build process: the generated oracle learners now need to take an additional (unused) argument in order to typecheck.
Until this issue is resolved, a temporary fix is to revert your local repo to commit 2ea101e71c6ca404407e95bbaf3bbac90bf1255f by doing: