-------- 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. ----------------------------------------------------------------------