IndexError: list index out of range

[palmskog]

I get this when I try to get suggestions for the file wmso.v in the RegLang project:

$ python -m roosterize.main suggest_lemmas  --project=../reglang  --serapi-options="-Q theories,RegLang"  --model-dir=./models/roosterize-ta  --output=./output
>>>>> Extracting lemmas ...
[   371W]roosterize.data.DataMiner: /home/palmskog/src/coq/misc/roosterize/output/raw-data already exists, will overwrite the files.
100%|...| 12/12 [01:04<00:00,  6.03s/it]
100%|...| 12/12 [00:14<00:00,  1.24s/it]
>>>>> Initializing model ...
[ 80674W]roosterize.ml.naming.OpenNMTMultiSourceForNaming: Cuda is not available
>>>>> Processing data ...
>>>>> Applying model ...
/home/palmskog/opt/miniconda3/envs/pytorch/lib/python3.7/site-packages/seutil/project/../../torchtext/data/field.py:359: UserWarning: To copy construct from a tensor, it is recommended to use sourceTensor.clone().detach() or sourceTensor.clone().detach().requires_grad_(True), rather than torch.tensor(sourceTensor).
  var = torch.tensor(arr, dtype=self.dtype, device=device)
Traceback (most recent call last):
  File "/home/palmskog/opt/miniconda3/envs/pytorch/lib/python3.7/runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "/home/palmskog/opt/miniconda3/envs/pytorch/lib/python3.7/runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/main.py", line 250, in <module>
    CliUtils.main(sys.argv[1:], globals(), normalize_options)
  File "/home/palmskog/opt/miniconda3/envs/pytorch/lib/python3.7/site-packages/seutil/CliUtils.py", line 117, in main
    actions[action](**options)
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/main.py", line 141, in suggest_lemmas
    model.eval(output_dir/"eval-processed-data", model_dir, output_dir/"eval-result")
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/ml/naming/NamingModelBase.py", line 100, in eval
    predictions_results: List[List[Tuple[str, float]]] = self.eval_impl(processed_data_dir, model_dir, self.BEAM_SEARCH_SIZE, self.K)
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/ml/naming/OpenNMTMultiSourceForNaming.py", line 835, in eval_impl
    attn_debug=opt.attn_debug
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/ml/onmt/MultiSourceTranslator.py", line 194, in translate
    translations = xlation_builder.from_batch(batch_data)
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/ml/onmt/MultiSourceTranslationBuilder.py", line 90, in from_batch
    for n in range(self.n_best)]
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/ml/onmt/MultiSourceTranslationBuilder.py", line 90, in <listcomp>
    for n in range(self.n_best)]
  File "/home/palmskog/src/coq/misc/roosterize/roosterize/ml/onmt/MultiSourceTranslationBuilder.py", line 31, in _build_target_tokens
    tokens.append(src_vocab.itos[tok - len(vocab)])
IndexError: list index out of range

[palmskog]

To replicate, install MathComp SSReflect and clone and build the repo:

$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam pin add coq-mathcomp-ssreflect 1.9.0
$ git clone https://github.com/coq-community/reglang.git
$ cd reglang
$ make

Now we can head to the roosterize directory and suggest names for everything in RegLang:

$ cd ../roosterize
$ python -m roosterize.main suggest_lemmas \
 --project=../reglang \
 --serapi-options="-Q theories,RegLang" \
 --model-dir=./models/roosterize-ta \
 --output=./output