Work log 2016-08-16

Posted on 2016-08-16 by Chris Warburton

ML4HSTechReport builds; just needs data.

IsaCoSy running with Nat theory. Need to run it with TIP (first the gutted export; then automatically gut the export).

Working in jEdit; trying from console.

Make table for Nats and Lists:

IsaCoSy | HipSpec | ML4HS

X% | Y% | Z% X seconds | Y seconds | Z seconds

What have we done so far?

ML4HS pipeline:

Haskell pkg -> Clusters -> Equations

TIP definitions:

TIP benchmarks -> SMTlib combination --+-> Haskell pkg
                                       |
                                       +-> Isabelle

IsaCoSy script:

Theory (hard coded :( ) -> Equations

Stumbling on connecting TIP haskell pkg to ML4HS. Connecting TIP Isabelle to IsaCoSy needs to be done.

Emailed Omar asking about IsaScheme.

Thinking about the current haskell-te setup, it’s a bit weird. Nix for tests is fine, but why for plumbing the components together?

Maybe we should have the Nix take in parameters (cluster number, WIDTH, HEIGHT, etc. [maybe just inherit these from runtime?]) and spit out a single, self-contained script, which logs times and everything.

How would that look?

ML4HS path/to/foo/package