ml4tp / gamepad

A Learning Environment for Theorem Proving
Apache License 2.0
72 stars 15 forks source link

Error when trying to create `tacst.pickle` file via tacst_prep.py #11

Open frieders opened 5 years ago

frieders commented 5 years ago

I'm trying to create for one of the foo files. But there are errors, namely ZeroDivisionError for foo1, foo4, foo5, foo6 and foo8, and NameError for the other foo files from ~/examples. What is happening here?

Here is my output for each type of error:

(gamepad_venv)$ coqc examples/foo4.v > examples/foo.dump; python3 gamepad/tactr_prep.py file foo.dump -p examples;  python3 gamepad/ml/tacst_prep.py
==================================================
Reconstructing file examples/foo.dump
progress: 0.50% @ foo4
Loading tactr.pickle...
Creating dataset tactr.pickle...
Working on (0/1) foo4
tacsts 3 avg_size 11.0 avg_mid_size 11.0 avg_mid_noimp_size 11.0
TACTICS {'<coretactics::split@0>', '<coretactics::assumption@0>', '<coretactics::intro@0>', '<g_auto::auto@0> $n $lems $db'}
TACHIST
TAC <coretactics::intro@0> 2
TAC ml4tp.MYDONE 0
TAC <coretactics::clear@0> 0
TAC <coretactics::exact@0> 0
TAC <coretactics::constructor@0> 0
TAC <coretactics::left@0> 0
TAC <coretactics::right@0> 0
TAC <coretactics::split@0> 0
TAC <coretactics::symmetry@0> 0
TAC <coretactics::transitivity@0> 0
TAC <g_auto::auto@0> 1
TAC apply 0
TAC case 0
TAC compute 0
TAC <ssreflect_plugin::ssrcongr@0> 0
TAC <ssreflect_plugin::ssrelim@0> 0
TAC <ssreflect_plugin::ssrhave@0> 0
TAC <ssreflect_plugin::ssrmove@0> 0
TAC <ssreflect_plugin::ssrpose@0> 0
TAC <ssreflect_plugin::ssrrewrite@0> 0
TAC <ssreflect_plugin::ssrset@0> 0
TAC <ssreflect_plugin::ssrsuff@0> 0
TAC <ssreflect_plugin::ssrtcldo@0> 0
TAC <ssreflect_plugin::ssrwithoutloss@0> 0
Split Train=1 Valid=0 Test=0
Split Tactrs Train=3 Valid=0 Test=0
Traceback (most recent call last):
  File "gamepad/ml/tacst_prep.py", line 350, in <module>
    tacst_dataset = tacst.split_by_lemma()
  File "gamepad/ml/tacst_prep.py", line 312, in split_by_lemma
    ps = [len(data_train) / len(train), len(data_val) / len(val), len(data_test) / len(test)]
ZeroDivisionError: division by zero
(gamepad_venv)$ coqc examples/foo3.v > examples/foo.dump; python3 gamepad/tactr_prep.py file foo.dump -p examples;  python3 gamepad/ml/tacst_prep.py
==================================================
Reconstructing file examples/foo.dump
progress: 0.17% @ foo2
Loading tactr.pickle...
Creating dataset tactr.pickle...
Working on (0/1) foo2
Traceback (most recent call last):
  File "gamepad/ml/tacst_prep.py", line 350, in <module>
    tacst_dataset = tacst.split_by_lemma()
  File "gamepad/ml/tacst_prep.py", line 286, in split_by_lemma
    self.mk_tactrs()
  File "gamepad/ml/tacst_prep.py", line 227, in mk_tactrs
    self.mk_tactr(tactr_id, tactr)
  File "gamepad/ml/tacst_prep.py", line 273, in mk_tactr
    tac_bin = self.tac_bin(tac)
  File "gamepad/ml/tacst_prep.py", line 239, in tac_bin
    raise NameError("Not assigned to bin", tac[-1].name)
NameError: ('Not assigned to bin', 'induction n')