lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

Install non-user-facing programs in /usr/libexec #139

Open SnarkBoojum opened 2 years ago

SnarkBoojum commented 2 years ago

I'm packaging coqhammer for Debian, and there's something not satisfying with installing htimeout and predict in /usr/bin: they are not supposed to be called by the user directly.

According to the Filesystem Hierarchy Standard, they should rather be installed in /usr/libexec, see discussion here, where /usr/lib/ would also be an option.

lukaszcz commented 2 years ago

Thank you for pointing this out. I'll leave it for now, because it's a bit complicated to change.

The problem is that libexec is typically not on the path. So one would need to somehow hardcode the path to libexec during installation/configuration (which might end up e.g. somewhere in the home directory below ~/.opam/).

Currently, CoqHammer's build system doesn't support such path hardcoding.