source: trunk/dports/math/acl2/Portfile

Last change on this file was 123356, checked in by mf2k@…, 3 years ago

acl2 cadabra ccl cln cosmoplayer dillo DoCon emacs-w3m GiNaC gtk2hs gtkwave hs-hashed-storage hs-libcabal hs-typenats LiE modglue nestedsums opendx opendx-java40 opendx-samples pcrexx sbcl simh TeXmacs: Ports abandoned by gwright. (#43784)

  • Property svn:eol-style set to native
  • Property svn:keywords set to Id
File size: 12.2 KB
Line 
1# $Id: Portfile 123356 2014-08-08 17:33:44Z ryandesign@macports.org $
2
3PortSystem 1.0
4
5name            acl2
6version         3.5
7set shortversion        v3-5
8categories      math
9maintainers     nomaintainer
10platforms       darwin
11description     Applicative Common Lisp / A Computational Logic
12long_description        \
13                ACL2 (Applicative Common Lisp / A Computational         \
14                Logic) is the successor to nqthm, the Boyer-Moore       \
15                theorem prover.                                         \
16                                                                        \
17                ACL2 can be used to automatically or semi-automatically \
18                prove theorems and has been used extensively in real    \
19                applications (e.g., proving the correctness of certain  \
20                calculations in the floating point unit of the AMD K5   \
21                microprocessor.                                         \
22                                                                        \
23                ACL2 is a very large, multipurpose system.              \
24                You can use it as a programming language,               \
25                a specification language, a modeling language,          \
26                a formal mathematical logic, or a semi-automatic        \
27                theorem prover. Because the meta-language is the same   \
28                as the language (a subset of Common Lisp), it is very   \
29                flexible.
30
31#user_notes     Users who want to use ACL2 for serious work should      \
32#               install the certify variant (sudo port install +certify), \
33#               which will certify (i.e., prove all of the theorems)    \
34#               in the included examples. This can take several hours.
35
36
37distfiles       ${name}-${version}${extract.suffix}:sources     \
38                workshops-${version}${extract.suffix}:workshops \
39                nonstd-${version}${extract.suffix}:nonstd
40
41homepage        http://www.cs.utexas.edu/users/moore/acl2/${shortversion}
42master_sites    ${homepage}/distrib/:sources                            \
43                ${homepage}/distrib/acl2-sources/books:workshops        \
44                ${homepage}/distrib/acl2-sources/books:nonstd
45
46checksums       acl2-${version}.tar.gz                                  \
47                    md5     a2738f4582d14f74664c93dad93ac055            \
48                    sha1    d4052a49a3c2112eeb04cf97570e2caea8df38dd    \
49                    rmd160  167b61cd8a812de804225096f4f3f04b87ba84cb    \
50                workshops-${version}.tar.gz                             \
51                    md5     5ae8123cadfe323c3088a3666112ce07            \
52                    sha1    b3a10d4cd876cb6ccde96920f0103ec0d89f7e2f    \
53                    rmd160  63401f257b8b61564ed660681f82776c762d43da    \
54                nonstd-${version}.tar.gz                                \
55                    md5     7de68f04ee468e25b24a230507cdb663            \
56                    sha1    71e1da0cf417ef85f1002279b67227d729822a6e    \
57                    rmd160  caa90d4a742fb1df8ddeb24686bc49a2d79754ab
58
59
60# ACL2 is distributed without a version number attached to the files.
61# So we can't tell if we have the latest version of a file by looking
62# at the name.  (This breaks also MacPorts checksum handling.)
63# Here, the files are manually fetched and renamed with a version number.
64#
65# MacPorts should always checksum the distribution files, instead
66# of assuming that if a file's name is unchanged, the previously computed
67# checksum is valid.
68fetch           {
69                  ui_msg "starting special fetch procedure for acl2"
70                  file mkdir ${distpath}
71
72                  if {![file exists ${distpath}/acl2-${version}.tar.gz]} {
73                        eval curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2.tar.gz ${distpath}/acl2.tar.gz.TMP
74                        file rename -force "${distpath}/acl2.tar.gz.TMP" "${distpath}/acl2-${version}.tar.gz"
75                  }
76
77                  if {![file exists ${distpath}/workshops-${version}.tar.gz]} {
78                        eval curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/workshops.tar.gz ${distpath}/workshops.tar.gz.TMP
79                        file rename -force "${distpath}/workshops.tar.gz.TMP" "${distpath}/workshops-${version}.tar.gz"
80                  }
81
82                  if {![file exists ${distpath}/nonstd-${version}.tar.gz]} {
83                        eval curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/nonstd.tar.gz ${distpath}/nonstd.tar.gz.TMP
84                        file rename -force "${distpath}/nonstd.tar.gz.TMP" "${distpath}/nonstd-${version}.tar.gz"
85                  }
86
87                  ui_msg "completed special fetch procedure for acl2"
88                }
89
90post-extract    {
91                  file rename ${workpath}/${name}-sources ${workpath}/${name}-${version}
92                  file rename ${workpath}/workshops ${workpath}/${name}-${version}/books
93                  file rename ${workpath}/nonstd    ${workpath}/${name}-${version}/books
94                }
95
96use_configure   no
97
98depends_run     port:sbcl
99
100set heap_image          "saved_acl2.core"
101set heap_image_nonstd   "saved_acl2r.core"
102set run_script          "saved_acl2"
103set run_script_nonstd   "saved_acl2r"
104
105# There is no universal binary for acl2, because there is no universal
106# build of sbcl or ccl.
107#
108universal_variant       no
109
110# By converntion, the 64 bit version of Clozure CL is invoked by the
111# script "ccl64"
112#
113# The ccl compiler produces a heap image whose filename extension depends
114# on the platorm.
115#
116set ccl_script ccl
117
118platform i386 {
119    global ccl_ext
120    set ccl_ext dx86cl
121}
122
123platform x86_64 {
124    global ccl_ext
125    set ccl_ext dx86cl64
126
127    global ccl_script
128    set ccl_script ccl64
129}
130
131platform powerpc {
132    global ccl_ext
133    set ccl_ext dppccl
134}
135
136platform ppc64 {
137    global ccl_ext
138    set ccl_ext dppccl64
139
140    global ccl_script
141    set ccl_script ccl64
142}
143
144# The emacs variant does not require that we use emacs from MacPorts,
145# since many users prefer Aquamacs.  It just copies the emacs support
146# files to ${prefix}/share/emacs/site-lisp.
147#
148variant emacs description {Include support for using acl2 under emacs} { }
149
150variant ccl description {Use ccl as the underlying lisp} {
151                  depends_run-delete    port:sbcl
152                  depends_run-append    port:ccl
153
154                  global heap_image
155                  global heap_image_nonstd
156                  set heap_image        saved_acl2.${ccl_ext}
157                  set heap_image_nonstd saved_acl2r.${ccl_ext}
158                }
159
160set target_path ${prefix}/share/${name}/${version}
161
162variant certify description {Certify the included books} { }
163variant regression description {Run the regression test suite (nb: takes hours)} { }
164variant nonstd description {Build the nonstandard analysis books for handling real numbers} { }
165
166build           { if {[variant_isset ccl]} {
167                         system "cd ${worksrcpath} && make large LISP=${prefix}/bin/ccl"
168                         if {[variant_isset nonstd]} {
169                                 system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/ccl"
170                         }
171                  } else {
172                         system "cd ${worksrcpath} && make large LISP=${prefix}/bin/sbcl"
173                         if {[variant_isset nonstd]} {
174                                 system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/sbcl"
175                         }
176                  }
177                }
178
179destroot        { file mkdir ${destroot}/${target_path}
180                  foreach f [glob -directory ${workpath}/${name}-${version} *] {
181                        file copy $f ${destroot}/${target_path}
182                  }
183
184                  if {[variant_isset emacs]} {
185                     set emacs_target ${prefix}/share/emacs/site-lisp
186                     file mkdir ${destroot}/${emacs_target}
187                     file copy ${destroot}/${target_path}/emacs/emacs-acl2.el ${destroot}/${emacs_target}
188                     file copy ${destroot}/${target_path}/emacs/monitor.el ${destroot}/${emacs_target}
189
190                     ui_msg "Emacs support files for acl2 are in ${emacs_target}"
191                  }
192                }
193
194post-destroot   { file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
195                  set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script}" w 755]
196
197                  if {[variant_isset ccl]} {
198                        puts $script "#!/bin/sh"
199                        puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
200                        puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --load ${destroot}${prefix}/share/${name}/${version}/cert_location --image-name ${destroot}/${target_path}/${heap_image}"
201                        puts $script ""
202                  } else {
203                        puts $script "#!/bin/sh"
204                        puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
205                        puts $script "sbcl --core ${destroot}/${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\' --load ${destroot}${prefix}/share/${name}/${version}/cert_location"
206                        puts $script ""
207                  }
208
209                  close $script
210                  system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script}"
211
212                  if {[variant_isset nonstd]} {
213                        file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
214                        set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}" w 755]
215                       
216                        if {[variant_isset ccl]} {
217                               puts $script "#!/bin/sh"
218                               puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
219                               puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --load ${destroot}${prefix}/share/${name}/${version}/cert_location --image-name ${destroot}/${target_path}/${heap_image_nonstd}"
220                               puts $script ""
221                        } else {
222                               puts $script "#!/bin/sh"
223                               puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
224                               puts $script "sbcl --core ${destroot}/${target_path}/${heap_image_nonstd} --userinit /dev/null --eval \'(acl2::sbcl-restart)\' --load ${destroot}${prefix}/share/${name}/${version}/cert_location"
225                               puts $script ""
226                        }
227
228                        close $script
229                        system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}"
230                  }
231
232                  set script [open "${destroot}${prefix}/share/${name}/${version}/cert_location" w 755]
233
234                  puts $script "(acl2::f-put-global \'acl2::old-certification-dir \"${destroot}${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
235                  puts $script "(acl2::f-put-global \'acl2::new-certification-dir \"${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
236                  close $script
237
238                  if {[variant_isset certify]} {
239                        set clogfile ${prefix}/share/${name}/${version}/certify-books.log
240                        ui_msg "certify-books log will be in ${clogfile}"
241                        system "cd ${destroot}/${target_path} && make clean-books"
242                        system "cd ${destroot}/${target_path} && make certify-books 2>&1 | tee ${destroot}/${clogfile}"
243                  }
244
245                  if {[variant_isset regression]} {
246                        set rlogfile ${prefix}/share/${name}/${version}/regression.log
247                        ui_msg "regression log will be in ${rlogfile}"
248                        system "cd ${destroot}/${target_path} && make clean-books"
249                        system "cd ${destroot}/${target_path} && make regression 2>&1 | tee ${destroot}/${rlogfile}"
250
251                        if {[variant_isset nonstd]} {
252                                set rlogfile_nonstd ${prefix}/share/${name}/${version}/regression-nonstd.log
253                                ui_msg "regression-nonstd log will be in ${rlogfile_nonstd}"
254                                system "cd ${destroot}/${target_path} && make ACL2=${destroot}${prefix}/share/${name}/${version}/saved_acl2r regression-nonstd 2>&1 | tee ${destroot}/${rlogfile_nonstd}"
255                        }
256                  }
257
258                  file delete ${destroot}${prefix}/share/${name}/${version}/cert_location
259                  file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
260                  set script [open "${destroot}${prefix}/bin/acl2" w 755]
261
262                  if {[variant_isset ccl]} {
263                        puts $script "#!/bin/sh"
264                        puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
265                        puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image}"
266                        puts $script ""
267                  } else {
268                        puts $script "#!/bin/sh"
269                        puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
270                        puts $script "sbcl --core ${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
271                        puts $script ""
272                  }
273
274                  close $script
275                  system "chmod 755 ${destroot}${prefix}/bin/acl2"
276
277                  if {[variant_isset nonstd]} {
278                        file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
279                        set script [open "${destroot}${prefix}/bin/acl2r" w 755]
280
281                        if {[variant_isset ccl]} {
282                                puts $script "#!/bin/sh"
283                                puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
284                                puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image_nonstd}"
285                                puts $script ""
286                        } else {
287                                puts $script "#!/bin/sh"
288                                puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
289                                puts $script "sbcl --core ${target_path}/${heap_image_nonstd} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
290                                puts $script ""
291                        }
292
293                        close $script
294                        system "chmod 755 ${destroot}${prefix}/bin/acl2r"
295                   }
296
297# Now remove all of the .out and build directory certificate files,
298# and rename the final (installation directory) certificates:
299                  foreach out_file [exec find ${destroot}/${target_path} -name "\*.out"] {
300                           file delete ${out_file}
301                  }
302
303                  foreach cert_file [exec find ${destroot}/${target_path} -name "\*.cert"] {
304                      file delete ${cert_file}
305                      file rename ${cert_file}.final ${cert_file}
306                  }
307                }
308
Note: See TracBrowser for help on using the repository browser.