[isabelle] segmentation fault solution



Hello,

I noticed in the archives many problems reporting the segmentation fault with the latest polyml. I managed to get isabelle to build with polyml 4.1.4 by using the 4.1.4 driver and the 4.1.3 database. I am including these in case anyone is still having problem building Isabelle, or is unfamiliar with building polyml from source. This worked for me to get Isabelle working so here are the steps: (I am assuming the x86 architecture - hence the i386, but it can be done for others)

download the driver.tar.gz, basis.tar.gz and mlsource.tar.gz files from

http://sourceforge.net/project/showfiles.php?group_id=148318&package_id=163589&release_id=359990

and then the database file from 4.1.3 from 

http://www.polyml.org/dbases/polyml-4.1.3.i386.tar.gz   

(assuming it's i386 you want - otherwise look in http://www.polyml.org/download.html)

now do the following in the directory where all the downloaded files are:

tar xzvf driver.tar.gz
cd driver
./configure
make
make install

# Now you have a poly driver executable which is ok for 2.6.9 kernels and later

tar xzvf mlsources.tar.gz
tar xzvf basis.tar.gz

cd mlsource/MLCompiler/CodeTree
ln -s CodeCons.i386 CodeCons                       #(here pick your architecture if not i386)

cd ../..

# Now you can make the 4.1.3 database with the 4.1.4 driver

tar xzvf polyml-4.1.3.i386.tar.gz   (or whatever 4.1.3 database you downloaded)

poly ML_dbase < mlsource/BuildAll.sml

# Now you the HOL logic will accept this polyml database

cp  DB413Release /usr/local/polyml-4.1.3/x86-linux/                   (again depends on architecture)

and overwrite the file there.

you may need to check the owner and group permissions of the file and make sure they are the same as before. Do an ls -l first, and then use chown <owner> file, and chgrp <group> file to do this as root.


I hope this helps some people who are struggling with the later linux kernels and Isabelle

Ewen



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.