Package Details: acl2 8.5-1

Git Clone URL: (read-only, click to copy)
Package Base: acl2
Description: ACL2 theorem prover.
Upstream URL:
Licenses: BSD
Submitter: soimort
Maintainer: soimort
Last Packager: soimort
Votes: 6
Popularity: 0.000000
First Submitted: 2014-03-04 23:51 (UTC)
Last Updated: 2022-12-13 00:26 (UTC)

Latest Comments

ragerdl commented on 2017-04-14 19:07 (UTC)

If you'd like the dependency upon etags to not exist (and you've confirmed that ACL2 really does depend on etags), then it'd be good to file a bug at

ragerdl commented on 2017-04-14 19:06 (UTC)

This probably needs a dependency upon etags... hopefully that doesn't require emacs.

soimort commented on 2015-01-08 14:46 (UTC)

Seems like an upstream-related issue. Can you reproduce the bug following the official instruction here (

aspirogrammer commented on 2015-01-08 14:39 (UTC)

I get the following error: debugger invoked on a SIMPLE-ERROR in thread #<THREAD "main thread" RUNNING {1003016473}>: Couldn't execute "etags": No such file or directory After two errors and exiting the debugger (with 0), the installation fails: Initialization FAILED: acl2-status.txt should contain :INITIALIZED. GNUmakefile:335: recipe for target 'check_init_ok' failed make[1]: *** [check_init_ok] Error 1