[isabelle] segmentation fault solution


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


and then the database file from 4.1.3 from 


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


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