Improve CoqHammer error message when 'predict' not found

[aleloi]

Steps to reproduce

• On ubuntu 21.10 install opam.
• Install coq=8.15.2, coq-hammer=1.3.2+8.15 In emacs-28.1 with proof-general 20220707.758, run

From Hammer Require Import Hammer.
Require Import Arith.
Lemma lem_1 : le 1 2.
  predict 1.

The expected result is something like

Extracting features...

Learning done; awaiting your features ...
Coq.Arith.PeanoNat.Nat.le_0_2

The actual result is

Error:
Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predict104c50fea /tmp/predict104c50dep /tmp/predict104c50seq -n 1 -p knn  < /tmp/predict104c50conj > /tmp/coqhammer_outknn1760fe8

The cause is apparent after removing 2> /dev/null in the construction of the predict call in src/plugin/featurs.ml : the command fails with sh: 1: predict: not found.

There are no problems with coqide installed from opam. Maybe this is an issue with proof-general, or it is a configuration issue. In any case, it took me a few hours to figure out that the problem was sh PATH, and I'd like to see it documented somewhere.

[lukaszcz]

You need 'predict' on the path. This is mentioned in the documentation, but maybe the error message from CoqHammer should clearly state that it's the most probable reason. Perhaps you didn't configure 'opam' properly and its binary directory is not on the path.

[aleloi]

Thanks for the reply! I followed some documentation to put test -r $HOME/.opam/opam-init/init.sh && . $HOME/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true in .bashrc, but that only changes path for bash on not sh.