Beautiful, interactive visualizations of logical inference
Haskell JavaScript Coq C Shell
Latest commit 35fc5ac Dec 20, 2012 @ezyang Fix some bugs and refactor some common code.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
Failed to load latest commit information.
doc Writeup. May 16, 2012
.gitignore Writeup. May 16, 2012
ClassicalFOL.hs Linear checkpoint. Sep 16, 2012
ClassicalFOL.v Support for iff connective. May 21, 2012
ClassicalFOLFFI.hs Linear checkpoint. Sep 16, 2012
Common.hs Linear checkpoint. Sep 16, 2012
CommonFFI.hs Linear checkpoint. Sep 16, 2012
Coq.hs Turn on warnings. May 21, 2012
CoqTop.hs Turn on warnings. May 22, 2012
Intuitionistic.hs Lots of stuff for intuitionistic. Sep 17, 2012
IntuitionisticFFI.hs Lots of stuff for intuitionistic. Sep 16, 2012
IntuitionisticFOL.v Intuitionistic first order logic yo. Feb 24, 2012
JSONGeneric.hs Turn on warnings. May 22, 2012
LICENSE Add cabal file for easy library version checking. Apr 29, 2012
Linear.hs Fix some bugs and refactor some common code. Dec 20, 2012
LinearFFI.hs Linear checkpoint. Sep 16, 2012
Ltac.hs Turn on warnings. May 22, 2012
README Notes about static files. Jul 29, 2012
Setup.hs Add cabal file for easy library version checking. Apr 29, 2012
TODO Turn off checkState due to lack of alpha-equivalence support. May 17, 2012
build.sh Fix some bugs and refactor some common code. Dec 20, 2012
common.ur Fix some bugs and refactor some common code. Dec 20, 2012
ffi.js Convert to using activate. Jul 23, 2012
haskell.c Lots of stuff for intuitionistic. Sep 16, 2012
haskell.h Lots of stuff for intuitionistic. Sep 16, 2012
haskell.urp Lots of stuff for intuitionistic. Sep 16, 2012
haskell.urs Lots of stuff for intuitionistic. Sep 16, 2012
intuitionistic.ur Fix some bugs and refactor some common code. Dec 20, 2012
intuitionistic.urp G4ip intuitionistic implementation. Oct 1, 2012
intuitionistic.urs Lots of stuff for intuitionistic. Sep 16, 2012
jquery-ui.js JavaScript libraries. Mar 13, 2012
jquery.infinitedrag.js JavaScript libraries. Mar 13, 2012
jquery.js JavaScript libraries. Mar 13, 2012
jquery.tipsy.js Convert to using activate. Jul 23, 2012
js.urp Convert to using activate. Jul 23, 2012
js.urs Convert to using activate. Jul 23, 2012
linear.ur Fix some bugs and refactor some common code. Dec 20, 2012
linear.urp Lots of stuff for intuitionistic. Sep 16, 2012
linear.urs Experimental propositional variant. Sep 13, 2012
logitext.cabal Note about what happened to process. May 18, 2012
logitext.ur Fix some bugs and refactor some common code. Dec 20, 2012
logitext.urp Hook up intuitionistic and ordinary together. Sep 17, 2012
logitext.urs Add beginnings of web app. Mar 10, 2012
style.css Lots of stuff for intuitionistic. Sep 16, 2012
style.ur Hook up intuitionistic and ordinary together. Sep 17, 2012
style.urp Hook up intuitionistic and ordinary together. Sep 17, 2012
tc.sh Add cabal file for easy library version checking. Apr 29, 2012
tipsy.css HTML tooltip support, fix the boogs. May 23, 2012

README

Install
-------

1) Get a copy of Coq with PGIP support

    git clone https://github.com/ezyang/coq
    # build Coq using the standard methods

You need to tell Logitext about where this Coq lives.
The easiest way is to create a file named config in the
Logitext directory that sets the PATH to the bin directory of
the built Coq, e.g.

    echo 'export PATH=$HOME/coq/bin:$PATH' > config

(Note: We use the -boot option to run Coq; this makes installation
easier but requires you to keep the build directory around.  If
you really want to 'make install' your copy of Coq, you'll need
to edit CoqTop.hs to remove the -boot flag, or make a coqtop wrapper
executable that strips the -boot flag.)

Test this setup by running the following commands:

    . config
    coqtop -v    # should have build date equal to current date
    coqtop -boot # should put you into repl

2) Get the Ur metaprogramming library

    hg clone http://hg.impredicative.com/meta/

Place this as a subdirectory of the logitext folder, and it will
automatically get picked up.

3) Get the Ur/Web compiler

    hg clone http://hg.impredicative.com/urweb
    # build Ur/Web using the standard method

You have a few options for setting up Ur/Web.  If you can install
it globally on the system, you need no further changes.

Alternatively, you can configure an alternate --prefix for Ur/Web, and
then add the Ur/Web in that location to your PATH.  (The build.sh script
references 'config', so you can place it there.) You'll also need to add
the include directory to C_INCLUDE_PATH, as we use the C FFI, which
needs a fully qualified header name (GHC will need this too).

Another convenient option is to just set URWEB_FLAGS="-boot",
and don't bother installing into an alternate prefix.  You'll
still need to modify PATH and C_INCLUDE_PATH, but you can directly
point them at the build directory.

4) Prepare GHC and Haskell

Any widely available distribution should do; the author personally
is using 7.4.1 with the Haskell Platform.  Run

    cabal configure

in order to find out what libraries you need, and install them.
We don't use cabal to build the Haskell products though, because
we need to use GHC to link Ur/Web and Haskell code together.

5) Build it!

You'll need a Linux system with inotify to use the normal scripts. Run

    ./build.sh

which sets up a continuous rebuilding server, and automatically starts
up with the normal parameters.  Tweak the script for your own needs
as necessary.  You can also run

    ./tc.sh

to get continuous typechecking on the Ur/Web files.

6) Serve static files

Ur/Web doesn't support serving static files natively, so you will need
to have another running web server to serve the external JavaScript and
CSS files.  By default they are expected to be at the URL
http://localhost/logitext/ but you can change this by editing
js.urp, logitext.urp, and logitext.ur (be sure to change the <link>
href, the script directives and the allow url directives).

Troubleshooting
---------------

    Database connection initialized.
    Starting up coqtop...
    Ready coqtop
    fd:9: commitBuffer: resource vanished (Broken pipe)

This means you are not using a version of Coq which understands the -pgip flag.

    In file included from /tmp/fileMvYC8r/webapp.c:7:0:
    /home/ezyang/Dev/logitext/haskell.h:1:25: fatal error: urweb/urweb.h: No such file or directory

You have not set your C_INCLUDE_PATH correctly.

    unhandled exception: Io: openIn "/usr/local/lib/urweb/ur/char.ur" failed with SysErr: No such file or directory [noent]

You forgot to pass the -boot flag to Ur/Web using URWEB_FLAGS.