Cert-pl-on-windows
Special notes about using cert.pl on Windows.
There are two main ways you can run cert.pl (and for that
matter ACL2) on Windows.
Option 1: Virtual Machine
A good way to run ACL2 on Windows may be to install an operating system like
Linux inside of virtual machine. Some options are:
Using a virtual machine certainly has its downsides. You're committing to a
certain amount of configuration, sacrificing some disk space and memory, and
probably losing some performance. Even so, you may find this option to be
generally more reliable than using Unix tools like make and Lisp runtimes
on a Windows system.
Option 2: Native Windows
If you prefer to avoid using a virtual machine, you may still be able to use
cert.pl on Windows. Unlike other operating systems, Windows does not
include a typical Unix environment with commands like ls, rm,
grep, etc, so using ACL2 on Windows typically means installing a Unix
emulation layer such as cygwin or msys.
We do not know which to recommend because we have experienced problems on
both! With msys, we have seen make hang when we try parallel builds.
With cygwin, we have sometimes seen "random" CCL crashes. From time to time,
we have successfully used cert.pl on msys with a single-threaded
build.
Both cygwin and msys have their own Perl packages available. For
cert.pl to work, please make sure you are using the Cygwin or Msys version
of Perl. Native Windows versions of Perl, such as Strawberry Perl, are not
known to work.
We intend for cert.pl to work on Windows. If you experience any
problems that you believe are due to cert.pl itself, rather than with
make or with your Lisp, then we would appreciate your help with
beta-testing and with making it more robust.
