LPL: Tarski's World on 64-bit Ubuntu
Prev Part I.  Miscellaneous subjects (and those still to be sorted)  Next

LPL: Tarski's World on 64-bit Ubuntu

Jurjen Bokma

December 2012

Abstract

Succesful attempt to install Tarski's World on 64 bit Ubuntu Precise

So I wanted to follow a Logic 101. The book - Language, Proof and Logic - seems excellent to me, the software is decent. But it wouldn't run on my 64-bit Ubuntu Precise.

Turns out the packaging is a bit below the standards of the book. The .deb package is just an alien-ized version of the RPM, with very little post-processing. One of the debs, op-jre, depends on 'fglrx'. That happens to be a package that contains the Xorg video driver for ATI VGA cards. I believe that dependency is wrong. More likely the package should 've depended on 

libgl1-mesa-glx | libgl1

or something the like.

My (wild) guess is that the .deb was created on a machine which got its gl through fglrx, hence alien concluded that op-jre needed fglrx and didn't abstract. And the people doing the packaging didn't know any better either.

Here's how I got it to work on my 64-bit Ubuntu Precise, with an Intel card. YMMV...

  1. Make sure you 've got OpenGL working

    Depending on your video card, this may be a lot of work or a walk in the park. And I can't describe it here since it depends so strongly on what card you 've got.

    I have a not too recent Intel card. I installed xserver-xorg-video-intel. Then I ran sudo Xorg -configure, and manually tuned the resulting xorg.conf.new before copying it to /etc/X11/xorg.conf.

  2. Create a fake package that provides fglrx

    Use the package equivs to create a fake and empty package that 

    <snip>
Provides: fglrx
Architecture: i386
<snip>

    No details here, the docs that come with equivs docs are both short and clear. Install the newly created package using dpkg.

  3. Pry the .debs from the installer

    The software isn't free. It comes on a CD, and on that CD is a monolithic installer consisting of a script with appended gzipped tarball containing .deb packages. The script just unpacks the tarball an installs the debs. And doing that it makes a slight mistake: if it doesn't succeed at once, the next time it won't install the packages, supposedly because dpkg lists them already. (It lists them as 'not installed'.)

    So we want the packages, and hence need the tarball. Let's see on which line it starts:

    apprentice@box:~.lpl$ grep -an ARCHIVE_FOLLOWS ../lpl-1105-linux-deb-installe.sh
    46:SKIP=wk '/^__ARCHIVE_FOLLOWS__/ { print NR + 1; exit 0; }' "$0"
    157:__ARCHIVE_FOLLOWS__

    Ah, line 157 is the last one of the script, so cut it there:

    apprentice@box:~.lpl$ sed '1,157 d' ../lpl-1105-linux-deb-installe.sh > lpl-1105-linux-deb-installe.tgz
    apprentice@box:~.lpl$ tar zxvf lpl-1105-linux-deb-installe.tgz
    op-boole_3.0-0_all.deb
    op-fitch_3.0-0_all.deb
    op-jre_1.5.0-22_i386.deb
    op-lpl-common_3.0-0_all.deb
    op-lpl-doc_3.0-0_all.deb
    op-submit_3.0-0_all.deb
    op-tarski_7.0-0_all.deb

  4. Install the LPL packages

    Just install the LPL packages (op-boole, op-fitch etc. you pried out of the installer. Fix any unsatisfied dependencies, repeat until they all install properly. Of if you want to be smart about it, install their dependencies first, then install the packages themselves.

Now enjoy 'tarski' running on 64-bit Ubuntu.

Prev Up Next
Ugrading and NSLU2 to Wheezy Home Foreman on Wheezy (not!)