Skip to content

UCSD-PL/proverbot9001

master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.

PWC

Proverbot9001

Proverbot logo A bot for proving.

You can find the paper and talk video at our website.

Prerequisites

You'll need to install git, opam, rustup, graphviz, libgraphviz-dev, python3.7, python3.7-dev and python3.7-pip to run Proverbot.

Newer versions of python than 3.7 also work, as long as you also have their development headers and pip version.

If you're running Linux, all three can be generally found in your package repositories. If that Linux is ubuntu, you'll have to first run:

sudo apt install software-properties-properties
sudo add-apt-repository ppa:avsm/ppa
sudo apt update

before you can install OPAM.

If you're running OS X, you can find these packages in Homebrew.

If you're on Windows, follow:

https://gitforwindows.org/

https://fdopen.github.io/opam-repository-mingw/installation/

https://graphviz.gitlab.io/_pages/Download/Download_windows.html

https://www.python.org/downloads/windows/

or use Windows Subsystem for Linux

Getting Started

The first thing you'll need to do is clone the repository (download the code).

I recommend that you do this over ssh. Open a terminal (windows users can use "Bash on Ubuntu on Windows"), move to the directory you want to work in, and run:

git clone git@github.com:UCSD-PL/proverbot9001.git

That should give you a new folder called proverbot9001 with all the code inside. Move into this new directory:

cd proverbot9001

And run this command to install the dependencies

make setup

this step will take a while, and might involve having to type y a few times.

Once that's finished, you're ready to start running the tool!

Running Proverbot9001 requires training on existing proof files. Training takes a while, and usually you need some pretty advanced hardware. So to quickly get started, we'll download pre-trained weights instead:

make download-weights

Now you can run Proverbot9001:

make search-report

Which will generate some html in the reports directory.

You should be able to check out the results by opening a web browser and navigating to the reports directory in the project.

Once you've done that, you might like to try training from scratch with make scrape and make train, or writing your own predictor.

About

No description, website, or topics provided.

Resources

License

GPL-3.0, GPL-3.0 licenses found

Licenses found

GPL-3.0
LICENSE
GPL-3.0
COPYING

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published