coqhammer
coqhammer copied to clipboard
Improve CoqHammer error message when 'predict' not found
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.
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.
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.