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

[frieders]

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')