1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en">
<head>
<title>Helpful Instructions for Setting up ACL2 and Windows</title>
</head>
<body>
<h1>Helpful Instructions for Setting up <A HREF="http://www.cs.utexas.edu/users/moore/acl2/">ACL2</A> and Windows</h1>
<p> We thank David Rager for providing
instructions, which we include verbatim below and expect apply to
future versions. Note: We recommend using CCL for Windows
builds, in part so that interrupts (Control-C) will work. But
first, a remark:</p>
<p>At least one user has built ACL2 on Windows 10 in July, 2016 by
following the instructions below, using the "bleeding edge" versions
of CCL, mingw, and ACL2. This user said the the bleeding edge
versions might not be necessary, but with older versions there were
too many times that the ACL2 build was hanging. Even with the
bleeding edge versions there were some hangs, but it wasn't clear if
that was the fault of CCL, Mingw, MSys, or something else. This user
explained further:</p>
<blockquote>
The problem with hangs: It seems that while compiling ACL2 there were
a few times when it simply hung. But apparently this is
non-deterministic. Simply cleaning and retrying several times managed
to get me out of the problem.
</blockquote>
<p><b><font color="red">Here are David Rager's instructions.</font></b></p>
<p> I was able to get ACL2 3.6.1 to install and build the regression suite
on Windows 7 with the following steps. I did not have to install
cygwin.</p>
<ol>
<li><p>Install MinGW. At the time of this writing, the following direct link works<br />
<a
href="http://sourceforge.net/projects/mingw/files/Automated%20MinGW%20Installer/MinGW%205.1.6/MinGW-5.1.6.exe/download">MinGW-5.1.6.exe</a></p>
<p>If that direct link doesn't work, click on "Automated MinGW Installer"
on the more general <a
href="http://sourceforge.net/projects/mingw/files/">MinWG project files
page</a>.</p>
</li>
<li><p>Install MSys. At the time of this writing, the following direct link
works<br />
<a
href="http://sourceforge.net/projects/mingw/files/MSYS%20Base%20System/msys-1.0.11/MSYS-1.0.11.exe/download">MSYS-1.0.11.exe</a></p>
<p>If that direct link doesn't work, click on "MSYS Base System" on the
more general <a
href="http://sourceforge.net/projects/mingw/files/">MinWG project files
page</a>.</p>
</li>
<li>Add "C:\msys\1.0\bin" to my environment variable "path". The way you
do this varies with each Windows XP/Vista/7. Roughly speaking, you need
to go to the control panel, and open up your system settings. Get to the
advanced system settings and click on environment variables. Edit the
"path" environment variable and add ";C:\msys\1.0\bin" to it. At this
point you might need to restart your computer, but I did not have to do
so on Windows 7. I did, however, have to restart my emacs.</li>
<li><p>Realize that using "\" to indicate paths in windows confuses some
linux programs and that you might need to use "/" sometimes.</p></li>
<li>
<p>After expanding the ACL2 sources, cd to that directory and type
something similar to the following (modify it to set LISP to your LISP
executable<sup>1</sup>)<br />
<code>make LISP=c:/ccl/wx86cl64.exe</code><br />
The "make.exe" that will be used is intentionally the MSys version,
not the MinGW version.</p>
</li>
<li>After your ACL2 image builds, make acl2 executable, specifically
<ul>
<li>Remove the "$*" from the saved_acl2 script (because Windows does
not understand $*). Consequently, any arguments you pass to ACL2 via
the command line will be ignored.</li>
<li>Rename saved_acl2 to saved_acl2.bat, for example by executing the
following command: <code>rename saved_acl2 saved_acl2.bat</code></li>
</ul>
</li>
<li><p>You can now make the regression suite by typing<br />
<code>make regression ACL2=c:/acl2-3.6.1/acl2-sources/saved_acl2.bat</code>
</p>
<p>[Note added later: you may need to add `<code>make</code>' option
<code>ACL2_CENTAUR=skip</code>, for example if you have
issues with Perl.]</p></li>
</ol>
<hr />
<p><sup>1</sup>I have intentionally ommitted instructions on how to setup a
LISP on windows. However, I include one link that should suffice: <a
href="http://trac.clozure.com/openmcl#GettingClozureCL">Obtaining
CCL</a></p>
</body>
</html>
|
