~ubuntu-branches/ubuntu/wily/acl2/wily

href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html">http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html</a>

328

contains links to ACL2 executables and packages. Each <code>-md5sum</code> file

329

was created using <code>md5sum</code>. We may add additional

330

links from time to time.

331

332

333

334

Now proceed to <A HREF="using.html">Using ACL2</A>.

335

336

337

338

<HR>

339

<H3><A NAME="Other-Unix">Building an Executable Image on a Unix-like System</A></H3>

340

341

We assume you have obtained ACL2 and placed it in directory dir, as

342

described <A HREF="#Sources">above</A>.

343

344

If you downloaded a <A

345

HREF="#Pre-Built-Images">pre-built ACL2 image</A>, you may skip this section.

346

347

Connect to dir as above and execute <CODE>cd

348

acl2-sources</CODE> <CODE>make LISP=</CODE>xxx

349

350

where xxx is the command to run your local Common Lisp.

351

352

By default, if no <CODE>LISP=</CODE>xxx is specified,

353

<CODE>LISP=ccl</CODE> is used. On our hosts, <CODE>ccl</CODE> is the name of

354

Clozure Common Lisp (CCL), which can be obtained as explained <a

355

href="requirements.html#Obtaining-CCL">in the Requirements document</a>.

356

357

358

359

This will create executable <code>saved_acl2</code> in the

360

<code>acl2-sources</code> directory.

361

362

363

364

The time taken to carry out this process depends on the host processor

365

but may be only a few minutes for a fast processor. The size of the

366

resulting binary image is dependent on which Lisp was used, but it may

367

a couple hundred megabytes or so.

368

369

370

This <CODE>make</CODE> works for the Common Lisp implementations listed

371

in <A HREF="requirements.html">Requirements document</A> on systems we

372

have tested. See the file <CODE>acl2-sources/GNUmakefile</CODE> for

373

further details. If this <CODE>make</CODE> command does not work for

374

you, please see the instructions below for <A HREF="#Non-Unix">other

375

than Unix-like systems</A>.

376

377

378

You can now skip to <A HREF="using.html">Using ACL2</A>.

379

380

381

<HR>

382

<H3><A NAME="Non-Unix">Building an Executable Image on Other than a

383

Unix-like System</A></H3>

384

385

Next we describe how to create a binary image containing ACL2 without

386

using the `<code>make</code>' utility. If you are using a trial

387

version of Allegro Common Lisp, then you may not be able to save

388

an image. In that case, skip to <A href="#Running">Running Without

389

Building an Executable Image</A>.

390

391

392

393

See also <a href="#Build-Particular">Building an Executable Image on Some Particular

394

Systems</a>, in case you want to skip directly to the instructions in one of

395

its subtopics.

396

397

398

399

Otherwise, proceed as follows.

400

401

402

403

Your Common Lisp should be one of those listed in

404

<A HREF="requirements.html">Requirements document</A>. Filenames

405

below should default to the dir<CODE>/acl2-sources</CODE>

406

directory; please connect to that directory before continuing.

407

408

<OL>

409

<LI> Remove file <CODE>nsaved_acl2</CODE> if it exists.</LI>

410

411

<LI> Start up Common Lisp in the <CODE>acl2-sources</CODE> directory

412

and submit the following sequence of commands.

413

414

<PRE>

415

; Compile

416

(load "init.lisp")

417

(in-package "ACL2")

418

(compile-acl2)

419

</PRE>

420

421

The commands above will compile the ACL2 sources and create compiled object

422

files on your <CODE>acl2-sources</CODE> subdirectory.

423

</LI>

424

425

<LI> Now exit your Common Lisp and invoke a fresh copy of it (mainly to avoid

426

saving an image with the garbage created by the compilation process). Again

427

arrange to connect to the <CODE>acl2-sources</CODE> subdirectory. In the

428

fresh Lisp <a name="initialization-first-pass">type</a>:

429

430

<PRE>

431

; Initialization, first pass

432

(load "init.lisp")

433

(in-package "ACL2")

434

(load-acl2)

435

(initialize-acl2)

436

</PRE>

437

438

This will load the new object files in the Lisp image and bootstrap ACL2 by

439

reading and processing the source files. But the attempt at initialization

440

will end in an error saying that it is impossible to finish because a certain

441

file was compiled during the processing, thus dirtying the image yet again.

442

(If however the attempt ends with an error during compilation of file

443

<code>TMP1.lisp</code>, see the first troubleshooting tip <a

444

href="#troubleshooting-TMP1">below</a>.)

445

</LI>

446

447

<LI> So now exit your Common Lisp and invoke a fresh copy of it (again arranging

448

to connect to your <CODE>acl2-sources</CODE> subdirectory). Then, in the

449

fresh Lisp type:

450

451

<PRE>

452

; Initialization, second pass

453

(load "init.lisp")

454

(in-package "ACL2")

455

(save-acl2 (quote (initialize-acl2))

456

"saved_acl2")

457

</PRE>

458

459

You have now saved an image. Exit Lisp now. Subsequent steps will put the

460

image in the right place.

461

462

<LI> Remove <CODE>osaved_acl2</CODE> if it exists.

463

464

<LI> IF <CODE>saved_acl2</CODE> and <CODE>saved_acl2.dxl</CODE> both exist THEN:

465

<ul>

466

<li>move <CODE>saved_acl2.dxl</CODE> to <CODE>osaved_acl2.dxl</CODE></li>

467

<li>move <CODE>saved_acl2</CODE> to <CODE>osaved_acl2</CODE>

468

and edit <CODE>osaved_acl2</CODE>, changing <CODE>saved_acl2.dxl</CODE>

469

(at end of line) to <CODE>osaved_acl2.dxl</CODE></li>

470

</ul>

471

ELSE IF <CODE>saved_acl2</CODE> exists THEN:

472

<ul>

473

<li>move <CODE>saved_acl2</CODE> to <CODE>osaved_acl2</CODE></li>

474

</ul>

475

</LI>

476

477

<LI> Move <CODE>nsaved_acl2</CODE> to <CODE>saved_acl2</CODE>.</LI>

478

479

<LI> For some Common Lisps, a

480

file <CODE>nsaved_acl2.</CODE>suffix is created for some

481

suffix.

482

Move it to: <CODE>saved_acl2.</CODE>suffix</LI>

483

484

<LI> Make sure <CODE>saved_acl2</CODE> is executable. For Windows

485

this involves two mini-steps:

486

487

488

489

(a) Remove the <code>"$*"</code> from the <code>saved_acl2</code>

490

script (because Windows does not understand <code>$*</code>).

491

Consequently, any arguments you pass to ACL2 via the command line will

492

be ignored.

493

494

495

496

(b) Rename <code>saved_acl2</code> to <code>saved_acl2.bat</code>, for

497

example by executing the following command.

498

<code>rename saved_acl2 saved_acl2.bat</code>

499

500

</blockquote>

501

</LI>

502

503

</OL>

504

505

<HR>

506

<H3><A NAME="Build-Particular">Building an Executable Image on Some Particular Systems</A></H3>

507

508

Subtopics of this section are as follows.

509

510

<UL>

511

<LI><A HREF="#Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A>

512

<LI><A HREF="windows7.html">Instructions from David Rager

513

for building ACL2 on Windows</A>

514

<LI><A HREF="windows-gcl-jared.html">Older instructions from Jared Davis for

515

building ACL2 on Windows using mingw</A>

516

</UL>

517

518

<HR>

519

<H3><A NAME="Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A></H3>

520

521

You may want to skip this section and instead read <A

522

HREF="windows7.html">Instructions from David Rager for building ACL2

523

on Windows</A>.

524

525

526

Or, you may be able to <a href="#Pre-Built-Images">download a pre-built ACL2 image</a>

527

for Windows instead of reading this section.

528

529

530

531

532

Otherwise here are steps to follow.

533

534

<ol>

535

<li>FIRST get GCL running on your Windows system using ONE of the

536

following two options. Note that GCL can be unhappy with spaces in filenames,

537

so you should probably save the GCL distribution to a directory whose path is

538

free of spaces.

539

540

<ul>

541

<li>OR, obtain GCL for Windows systems from <code><a

542

href="ftp://ftp.gnu.org/gnu/gcl/">ftp://ftp.gnu.org/gnu/gcl/</a></code>

543

or as explained <a href="#Obtaining-GCL">above</a>. You

544

may wish to pick a <code>.zip</code> file from the <code>cvs/</code>

545

subdirectory (containing pre-releases) that has "<code>mingw32</code>" in the

546

name.

547

548

<li>OR ELSE, perhaps you can build GCL on your Windows system from the

549

sources. The mingw tools and the cygnus bash shell have been used to build

550

distributed GCL executables.

551

552

</ul>

553

554

<li>SECOND, create an appropriate GCL batch file. When we tried running

555

the script <code>gclm/bin/gclm.bat</code> that came with

556

<code>gcl-cvs-20021014-mingw32</code> from the above ftp site, a separate

557

window popped up, and with an error. Many ACL2 users prefer running in an

558

emacs shell buffer. (We obtained emacs for Windows from <code><a

559

href="ftp://ftp.gnu.org/gnu/windows/emacs/21.2/emacs-21.2-fullbin-i386.tar.gz">ftp://ftp.gnu.org/gnu/windows/emacs/21.2/emacs-21.2-fullbin-i386.tar.gz</a></code>.)

560

The following modification of <code>gclm.bat</code> seemed to solve the problem

561

(your pathnames may vary).

562

<pre>

563

564

% do not delete this line %

565

@ECHO off

566

set cwd=%cd%

567

path C:\gcl\gclm\mingw\bin;%PATH%

568

C:\gcl\gclm\lib\gcl-2.6.2\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.2/unixport/ -libdir C:/gcl/gclm/lib/gcl-2.6.2/ -eval "(setq si::*allow-gzipped-file* t)" %1 %2 %3 %4 %5 %6 %7 %8 %9

569

</pre>

570

571

<li>THIRD, follow the <A HREF="#Non-Unix">instructions for

572

other than Unix-like systems</A> above, though the resulting file

573

may be called

574

<code>saved_acl2.exe</code> rather than <code>saved_acl2</code>.

575

576

577

578

579

<li>FINALLY, create a file <code>acl2.bat</code> as explained in

580

581

http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html</a></code>.

582

583

</ol>

584

585

586

587

We hope that the above simply works. If you experience

588

problems, the following hints may help.

589

590

591

592

TROUBLESHOOTING:

593

<ul>

594

595

<li><a name="troubleshooting-TMP1">We</a> tried building ACL2 on Windows XP on

596

top of GCL, our attempt broke at the end of the "<a

597

href="#initialization-first-pass">Initialization, first pass</a>" step, while

598

compiling <code>TMP1.lisp</code>. That was easily remedied by starting up a

599

fresh GCL session and invoking <code>(compile-file "TMP1.lisp")</code> before

600

proceeding to the next step.

601

602

<li>Yishai Feldman has provided some nice instructions at <code><a

603

href="http://www.faculty.idc.ac.il/yishai/reasoning/win-install.htm">http://www.faculty.idc.ac.il/yishai/reasoning/win-install.htm</a></code>,

604

some of which we have tried to incorporate here. A useful point made there is

605

that when you want to quit ACL2, use <code>:good-bye</code> (or

606

<code>(good-bye)</code> which works even in raw Lisp). Or you can use

607

<code>(user::bye)</code> in raw Lisp. The point is: Avoid <code>control-c

608

control-d</code>, even thought that often works fine in emacs under

609

Unix-like systems.

610

611

<li>If the above batch file does not work for some reason, an alternate

612

approach may be to set environment variables. You may be able to add to the

613

<code>PATH</code> variable gcl-dir<code>\gcc\bin</code>, where

614

gcl-dir is the directory where GCL is installed. To get to the place to

615

set environment variables, you might be able to go to the control panel, under

616

system, under advanced. Alternately, you might be able to get there by opening

617

<code>My Computer</code> and right-clicking to get to <code>Properties</code>,

618

then selecting the <code>Advanced</code> tab. At one time, when GCL/Windows

619

was release as Maxima, Pete Manolios suggested adding the system variable

620

LD_LIBRARY_PATH with the value "maxima-dir\gcc\i386-mingw32msvc\include"; this

621

may or may not be necessary for your GCL installation (and the path would of

622

course likely be different).

623

624

</ul>

625

626

627

628

<H2><A NAME="Running">Running Without Building an Executable Image</A></H2>

629

630

The most convenient way to use ACL2 is first to install an executable image as

631

described above for <A HREF="#Other-Unix">Unix-like systems</A> and <A

632

HREF="#Non-Unix">other</A> platforms. However, in some cases this is not

633

possible, for example if you are using a trial version of Allegro Common Lisp.

634

In that case you should follow the steps below each time you want to start up

635

ACL2.

636

637

638

639

We assume you have obtained ACL2 and placed it in directory dir, as

640

described above for <A HREF="#Sources">Unix-like systems</A> or <A

641

HREF="#Sources-Non-Unix">other</A> platforms.

642

643

(If you downloaded a <A

644

HREF="#Pre-Built-Images">pre-built ACL2 image</A>, then you may skip this section.)

645

646

Connect to subdirectory <CODE>acl2-sources</CODE> of dir,

647

start up your Common Lisp, and compile by executing the following forms.

648

This sequence of steps need only be performed once.

649

650

<PRE>

651

(load "init.lisp")

652

(in-package "ACL2")

653

(compile-acl2)

654

</PRE>

655

656

Now each time you want to use ACL2, you need only execute the following forms

657

after starting up Common Lisp in subdirectory <CODE>acl2-sources</CODE> of

658

dir.

659

660

<PRE>

661

(load "init.lisp")

662

(in-package "ACL2")

663

(load-acl2)

664

(initialize-acl2)

665

</PRE>

666

667

Note. The resulting process includes the ACL2 documentation, and hence

668

will probably be considerably larger (perhaps twice the size) than the result

669

of running an executable image created as described <A

670

HREF="#Create-Image">above</A>.

671

672

673

674

Now proceed to read more about <A HREF="using.html">Using ACL2</A>.

675

676

677

<H2><A NAME="Summary">Summary of Distribution</A></H2>

678

679

The ACL2

680

distribution, <code><A HREF="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/acl2.tar.gz">

681

acl2.tar.gz</A></code>, includes the ACL2 source files as well as

682

the following files and directories (and a few others not

683

mentioned here). Note that a <code>books/</code> directory

684

is not included; see instructions above to fetch the community

685

books.

686

<PRE>

687

LICENSE ; ACL2 license file

688

GNUmakefile ; For GNU make

689

TAGS ; Handy for looking at source files with emacs

690

doc/ ; ACL2 documentation

691

emacs/ ; Some helpful emacs utilities

692

installation/ ; Installation instructions (start with installation.html)

693

</PRE>

694

695

Also available are the following.

696

697

<ul>

698

699

<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/">images/</a></code>:

700

Some gzip'd tar'd executables; see <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html">images/Readme.html</a></code></li>

701

702

<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/split/">split/</a></code>: The result of splitting up <code>acl2.tar.gz</code></li>

703

704

</ul>

705

706

707

We estimate that the entire <code>acl2.tar.gz</code> consists of

708

approximately 4 MB, which extracts to about 15 MB, and the size of

709

gzipped tarfile <code>books-6.5.tar.gz</code> (obtained as described

710

<a href="#Obtaining-books">above</a>) is about 15 MB, which extracts

711

to about 87 MB. (Gzipped tarfile <code>workshops-6.5.tar.gz</code>

712

and corresponding directory <code>workshops</code>, which are

713

mentioned above, have sizes of about 37 MB and 58 MB, respectively.)

714

Additional space is required to build an image, perhaps 50 to 300

715

megabytes depending on the platform (including the host Lisp); and

716

more will be required to <A HREF="using.html#Certifying">certify

717

books</A>.

718

719

720

721

[<a href="installation.html">Back to Installation Guide.</a>]

722

723

724

<H2><A NAME="Bleeding-edge">Bleeding-edge Distributions via SVN</A></H2>

725

726

We strongly recommend that ACL2 users update their local copies of the

727

system and community books at each ACL2 release. While that should

728

suffice for many ACL2 users, nevertheless for those who prefer to

729

obtain the latest developments, the ACL2 source code and community

730

books have been made available between ACL2 releases, by way of

731

revision control using SVN.

732

The authors of ACL2 consider SVN distributions to be experimental;

733

while they will likely be fully functional in most cases, they could

734

however be incomplete, fragile, and unable to pass our own

735

regression. If you decide to use SVN versions of either the ACL2

736

or the community books, then you should use both, as they tend to be

737

kept in sync. See the project

738

websites, <code><A HREF="http://acl2-books.googlecode.com/">acl2-books</A></code>

739

and <code><A HREF="http://acl2-devel.googlecode.com/">acl2-devel</A></code>,

740

for the ACL2 community books and development sources, respectively.

741

742

743

744

</BODY>

745

</HTML>

Older »