GitHub - kryptine/ghilbert: Automatically exported from code.google.com/p/ghilbert

kryptine / ghilbert Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Automatically exported from code.google.com/p/ghilbert

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 249 Commits
app		app
babygit		babygit
js		js
static		static
.gitignore		.gitignore
.hgignore		.hgignore
COPYING		COPYING
README		README
app.yaml		app.yaml
backends.yaml		backends.yaml
ghapp.py		ghapp.py
index.yaml		index.yaml
testsuite		testsuite
verify.py		verify.py
verify_all.py		verify_all.py
verify_test.py		verify_test.py

Repository files navigation

README for Ghilbert prototype

Raph Levien
26 Feb 2010

Here is a prototype of the Ghilbert implementation.

You can use the batch verifier as follows:

python verify.py peano/peano_thms.gh

You can run the web app locally by installing the appengine SDK and running:

dev_appserver.py .

Then navigating to http://localhost:8080/edit/thmname

Save the proof by pressing Ctrl-S, then navigating to:

http://localhost:8080/recent

The interactive proof tool is, at present, extremly rough.

For more details, see http://ghilbert.googlecode.com/

Note: includes the minified JavaScript version of google-diff-match-patch,
which is (also) under Apache 2 license. For full attribution, please see:
http://code.google.com/p/google-diff-match-patch/