-------- Original Message --------
Subject: RE: [PPL-devel] Compiling PPL under Cygwin?
Date: Mon, 15 Mar 2004 18:05:16 -0500
From: Goran Frehse gfrehse@andrew.cmu.edu
To: 'Roberto Bagnara' bagnara@cs.unipr.it
Dear Roberto,
I'm sorry for not answering sooner. I was extremely busy these past
weeks, and unfortunately I'm still not able to compile under Cygwin.
I will attach my installation notes so far - they should work under
Mandrake, SuSE and Redhat Linux.
On a different topic, I've submitted two papers on a prototype tool that
I'm working on. It verifies Linear Hybrid Automata using the polyhedral
computations of the PPL. Compared to an existing tool (HyTech) it
performs very nicely, and I am quite pleased with the speed of the PPL.
I tried to give due credit to you in the papers and cited some of your
work. In case you're interested in the topic, I'd be happy to send you
the submitted drafts.
Best wishes,
Goran
--
Goran Frehse
Department of Electrical and Computer Engineering
Carnegie Mellon University
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
----------------------------------------------------------------------
How to install PPL 0.5
----------------------------------------------------------------------
1. Install GMP (4.2)
- Run cygwin bash-shell.
- Change to gmp-directory (gmp-4.2)
- Type: CPPFLAGS=-fexceptions ./configure --enable-cxx
- Type: make
- Type: make install
Take note in which directory gmp was installed. At several places in the output
it will say something like:
"Libraries have been installed in:
/usr/local/lib"
2. Install PPL (0.5)
- Change to ppl-directory (ppl-0.5)
- Type: ./configure --with-gmp-dir=/usr/local/lib --with-gmp-includes=/usr/local/include
Note: These paths vary with your distribution and depend on the installation of GMP.
- Type: make
- Type: make install
----------------------------------------------------------------------
Testing
----------------------------------------------------------------------
- go to gmp-directory
- Type: make check
- go to ppl-directory
- Type: make check
Note: Bug in Cygwin might require fixing libgmpxx.la (see below).
----------------------------------------------------------------------
Compile a test file for GMP
----------------------------------------------------------------------
- If your compiler is gcc:
gcc -g test2.c -lgmp
----------------------------------------------------------------------
Compile a program using PPL
----------------------------------------------------------------------
- If your compiler is gcc:
gcc -g name.cpp -lgmp -lgmpxx -lppl
----------------------------------------------------------------------
Error in Cygwin 1.5.7-1
----------------------------------------------------------------------
Symptom: False reference in libgmpxx.la leads to error in libtool when trying to compile programs using the PPL.
Fix: In "libgmpxx.la" (usually in /usr/local/lib), replace
"/GCC/gcc-3.3.1-3/.inst/package-gcc/usr/lib/./libstdc++.la" with appropriate path, usually "/usr/lib/libstdc++.la" or "lib/libstdc++.la".
----------------------------------------------------------------------
Excerpt from "make install" in GMP that contains path information:
----------------------------------------------------------------------
Libraries have been installed in:
/usr/local/lib
If you ever happen to want to link against installed libraries
in a given directory, LIBDIR, you must either use libtool, and
specify the full pathname of the library, or use the `-LLIBDIR'
flag during linking and do at least one of the following:
- add LIBDIR to the `PATH' environment variable
during execution
- add LIBDIR to the `LD_RUN_PATH' environment variable
during linking
- use the `-Wl,--rpath -Wl,LIBDIR' linker flag
See any operating system documentation about shared libraries for
more information, such as the ld(1) and ld.so(8) manual pages.
----------------------------------------------------------------------
Roberto Bagnara