Easier install process

[delcypher]

@hellovijay would prefer a simpler install process. Could you state what things you think need addressing?

I recall you saying in #62 that you don't like the Boost dependency. I really don't see this as a problem because Boost is available pretty much everywhere and is very easy to install.

However if you would like something simpler then something we could do is provide our own Ubuntu PPA that provides the latest build of STP. A user would simply need to do something like...

sudo add-apt-repository something:something
sudo apt-get update
sudo apt-get install stp

I think this could work well with the #76 because we can test STP before building a new STP package.

This would be even easier for a user because the Boost dependency will be explicit and will be installed as a dependency. Also the user doesn't to build STP themselves.

[hellovijay]

Hi Dan,

I agree with you that we should provide the user with the Ubuntu PPA
option. This would make life easier for many STP users.

-Vijay Ganesh.

On Sun, Mar 9, 2014 at 10:53 AM, Dan Liew notifications@github.com wrote:

@hellovijay https://github.com/hellovijay would prefer a simpler
install process. Could you state what things you think need addressing?

I recall you saying in #62 #62 that
you don't like the Boost dependency. I really don't see this as a problem
because Boost is available pretty much everywhere and is very easy to
install.

However if you would like something simpler then something we could do is
provide our own Ubuntu PPA that provides the latest build of STP. A user
would simply need to do something like...

sudo add-apt-repository something:something
sudo apt-get update
sudo apt-get install stp

I think this could work well with the #76https://github.com/stp/stp/pull/76because we can test STP before building a new STP package.

This would be even easier for a user because the Boost dependency will be
explicit and will be installed as a dependency. Also the user doesn't to
build STP themselves.

Reply to this email directly or view it on GitHubhttps://github.com//issues/77
.

[msoos]

I have worked quite a bit on this today. Here is where I got to:

• I have created an Ubuntu PPA: https://launchpad.net/~soos-mate-j/+archive/stp and uploaded an STP package there. This is currently my own PPA, not that of the team (see below)
• Created a team for us: https://launchpad.net/~simple-theorem-prover Please apply so I can add you.
• Created a project for STP: https://launchpad.net/stp/ Please apply so I can add you.

I have also pointed Ubuntu to the github repo, see the bottom of this: https://code.launchpad.net/~soos-mate-j/stp/master .Unfortunately, it errored: "The repository you are fetching from contains submodules, which are not yet supported".

We need to keep the repos in sync manually and update the package once in a while. Not a big deal. Ubuntu builds the binaries by itself, so all I need to do is package the source with somethings along the line of:

bzr builddeb -- -us -uc
debuild -S
(only for dependency check:) cd ../build-area && pbuilder-dist trusty build *.dsc
debsign *.changes
dput ppa:soos-mate-j/stp stp_1.0-1_amd64.change

What we need to do is look a this http://bazaar.launchpad.net/~soos-mate-j/stp/stp-package/files/head:/debian/ and fix it. Once you are part of the team on Ubuntu you can fix it with bazar and push it. Then I can build&upload the source -- or you can, too, but I already went through the hassle, and there aren't many tweaks one can do outside of changing what's in debian/

[delcypher]

On 24 June 2014 02:36, Mate Soos notifications@github.com wrote:

I have worked quite a bit on this today. Here is where I got to:

I have created an Ubuntu PPA: https://launchpad.net/~soos-mate-j/+archive/stp and uploaded an STP package there. This is currently my own PPA, not that of the team (see below)
Created a team for us: https://launchpad.net/~simple-theorem-prover Please apply so I can add you.
Created a project for STP: https://launchpad.net/stp/ Please apply so I can add you.

I can't apply. The team seems to be in "Restricted Team" mode so you
have to invite me (my username is delcypher on launchpad))

I have also pointed Ubuntu to the github repo, see the bottom of this: https://code.launchpad.net/~soos-mate-j/stp/master .Unfortunately, it errored: "The repository you are fetching from contains submodules, which are not yet supported".

We need to keep the repos in sync manually and update the package once in a while. Not a big deal. Ubuntu builds the binaries by itself, so all I need to do is package the source with somethings along the line of:

By keep in sync do you mean we have to copy the entire source tree
into a bzr repository?

bzr builddeb -- -us -uc
debuild -S
(only for dependency check:) cd ../build-area && pbuilder-dist trusty build *.dsc
debsign *.changes
dput ppa:soos-mate-j/stp stp_1.0-1_amd64.change

What we need to do is look a this http://bazaar.launchpad.net/~soos-mate-j/stp/stp-package/files/head:/debian/ and fix it. Once you are part of the team on Ubuntu you can fix it with bazar and push it. Then I can build&upload the source -- or you can, too, but I already went through the hassle, and there aren't many tweaks one can do outside of changing what's in debian/

I'm not very familiar with debian packages but...

• Shouldn't this debian/ folder live the stp github repository?
• We need to establish a system for version numbers. We should
  probably start tagging releases (using git tag). Where is the version
  number specified in the debian files?

Thanks,
Dan.

[msoos]

Thanks for the pointers. I looked around, using bzr is useless. As for the debian/ dir, I would love to keep it in this git, if you are OK with that, I'll put it right up. I also changed the membership to allow anyone to request to join and invited you. The team is now the maintainer for this PPA:

https://launchpad.net/~simple-theorem-prover/+archive/ppa

into which I uploaded an older version of STP just to test, you can delete it. Given the /debian folder (available if you download the source package), it's a bit tricky to create the initial package:

cd stp
dh_make --createorig
dpkg-buildpackage -S 
-> will error out, do: mv ../stp-versionname.orig.tar.xz ../stp-whatever-dpkg-buildpackage-needs.orig.tar.xz
dpkg-buildpackage -S 
dput ppa:simple-theorem-prover/ppa stp_1.0-1_source.changes 

The next versions are easy, just add a line to debian/changes and:

cd stp
dpkg-buildpackage -S 
dput ppa:simple-theorem-prover/ppa stp_PREV_VERSION_source.changes 

It needs the .orig.xz file that was the previous version (which is what dh_make --createorig made), though.

As for version numbers, I agree with the tagging idea. We can then release the tagged versions as a package.

Should I move the debian/ folder over?

[delcypher]

Sorry for the delay on this. I recently learnt how to build ubuntu PPA packages for another project and I thought I'd put my new skills to use.

I've uploaded a new package which follows a 1.0+1SNAPSHOTYYYYMMDD-X~trusty1 version naming scheme.

I've created a separate repo for packaging files to contain packaging files for various platforms. It has a handy script with a README for creating snapshot packages.

We should probably advertise this PPA more as it's quite a handy way to get a recent build of STP.

[delcypher]

Oh. I should probably note as well I decided not to put the debian/ folder in STP's source tree because it may need to be modified for different Ubuntu distributions and also because of recommendations in this guide. I still wanted it under version control though so that's why I made a separate repository for it.

[msoos]

Separate repo is great. The PPA really needs to be advertised, I agree. We should make a new release soon and put the PPA and the tarball right next to one another so people can see & download either.

I'm going to take a look at this over the weekend, but we should be able to have more than one Ubuntu binary package automatically generated -- currently, it's only Trusty. I think it can auto-generate for all Ubuntu versions, which would be really useful (at least for the past ~2 years). I'll try to do that, put a bit of documentation up into the README (thanks for starting it!) and then close this issue. We can open new issue later for anything that comes up.

Thanks for all!

Mate

[delcypher]

@msoos There's an issue with building for Precise because we depend on a version of CMake not available in the standard repos. There are two solutions I think

• It's possible to mark your PPA as dependent on another PPA. We could mark our PPA as being dependent on a PPA that provides the newer CMake version (e.g. the one we use for Travis). I'm not sure how great this is though because we only really need the CMake packages for precise and not for trusty
• Add a newer cmake build to our PPA for precise only. This might be the easier thing to do.

[msoos]

There is specific CMake bug that would make something (I forgot what) a bit hairy. I can try to see what happens if we make the requirement lower, but it's really not that simple. I'll get a Precise virtual machine and see what happens :)

[delcypher]

@msoos I've copied over the CMake package that we use for Travis (there's a handy option for doing this in launchpad's web interface) to our PPA so in principle once we upload a the package for precise it should build

I'm not on a machine that has my signing keys so I can't do this right now. I can do this at some point over the weekend.

[delcypher]

@msoos Okay I've uploaded packages for precise, trusty and utopic. That's the currently supported Ubuntu versions covered.

[delcypher]

I forgot to mention. Maybe at some point in the future we should switch to the OpenSUSE Build service instead because we support many more Linux distributions that way. Also I found launchpad rather painful to use.

[msoos]

Wow, great work! Thanks a lot! I added a link to the packages to the README and updated the WIKI to reflect this. I think we can now close this and add a wish "Move to OpenSUSE Build service": #139

Closing, thanks!