Как исправить ошибку проверки работоспособности книг ACL2?

Из каталога книг ACL2 всякий раз, когда я пытаюсь создать или очистить книги, я получаю сообщение об ошибке, которое выглядит так:

GNUmakefile:299: *** Books Sanity Check Failed. Stop.

Как я могу избежать этого сообщения об ошибке?


acl2
person interestedparty333    schedule 11.08.2015    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Эта ошибка возникает из-за того, что makefile теперь проверяет, считает ли make acl2, что вы используете тот же каталог, в котором вы сейчас находитесь. Решение состоит в том, чтобы сказать make использовать acl2, который находится в вашем текущем каталоге. Вы можете добиться этого, передав ACL2 в качестве аргумента, например:

make ACL2=~/sw/acl2-extra/saved_acl2 clean

person interestedparty333    schedule 11.08.2015