1

I have been trying to install SRILM to use with Kaldi and have run into a particularly frustrating issue.

To create a clear timeline of actions, here goes:

I downloaded the tar.gz from the SRILM website.

I extracted the file into a subdirectory in my home folder (/Home/Speech/SRILM) using the file manager program included with Ubuntu.

I changed the SRILM = line in the makefile to SRILM = /Home/Speech/SRILM.

I did not change anything else in the makefile because I am running Linux x86_64 and the instructions state that this should be able to compile out of the box (which I am beginning to doubt).

I attempted to make and was met with the following error.

make: /Home/Speech/SRILM/sbin/machine-type: Command not found
Makefile:13: /Home/Speech/SRILM/common/Makefile.common.variables: No such file or directory
make: *** No rule to make target `/Home/Speech/SRILM/common/Makefile.common.variables'. Stop.

All of the paths, files, and directories exist, so I am confused as to why the program is incapable of finding them.

If there is a well made, step by step guide to installing/compiling SRILM I would greatly appreciate a link. I have attempted to find one and all the ones I have found (including the instructions in the install file) appear to be missing some steps/not very clear.

Solution: Replaced Home with /home/username, learned a bit more about Ubuntu filesystems.

2
  • Home isn't a real directory: it's just what the file manager (nautilus) uses as a shorthand for the user's home directory, otherwise known in the shell as $HOME. It usually expands to /home/username (where username is replaced by your actual login name) but you should confirm by running echo $HOME in a terminal. Jul 26, 2015 at 22:35
  • Just edited the makefile and changed Home to /home/myusername and ran make again, process ran. There may be other errors, but this one is fixed. Thank you.
    – K G
    Jul 26, 2015 at 22:39

1 Answer 1

2

Home isn't a real directory: it's just what the file manager (nautilus) uses as a shorthand for the user's home directory, otherwise known in the shell as $HOME.

It usually expands to /home/username (where username is replaced by your actual login name) but you should confirm by running echo $HOME in a terminal.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .