Re: [isabelle] scala interface



Hi Matthias,

since similar questions have popped up now and then on the list, I
have taken a closer look at your request on the basis of the implementation
of the I3P interface (see my web-page), because in principle
it already offers the required API to do "background proving".

To explain: as desirable for user interface software (see the MVC pattern),
the functionality of I3P is implemented entirely in a self-contained
infrastructure layer that is independent of the Netbeans interface
that happens to access that functionality now.
As a result, extended unit tests can be run against the functionality
(which have greatly helped in maintainance and debugging through
the different Isabelle releases of the past 2 years) and the bulk of the
software becomes portable (e.g. to Eclipse, as done prototypically
in a bachelor thesis in Tübingen). For a fuller motivation and
architecture description, see my UITP '10 paper.

In principle, the infrastructure layer thus enables running Isabelle
as a background prover directly, analogously to the existing unit tests
of the Isabelle driver module. At the core, the it provides a simple
execute/revoke model for commands (based on two methods of
CommandState), while I3P takes care of sending
appropriate Isabelle commands, interrupt signals, etc. as necessary.
(I3P even keeps sending INT until the command stops executing.)

However, the abstractions built into the architecture lead to some
boilerplate code (see the @Before methods of the tests) that is not nice
for the specific application.

I have now added a small IsabelleFacade class (in module APIAccess;
for Facade see Gamma et al. "Design Patterns", 1995),
which hopefully makes the procedure straightforward. The attachment
contains a demonstration of the following features:

- start & stop the prover
- execute theories / individual commands and
  * check for sucess, failure, or non-termination
  * access the command's results
  * interrupt (explicit or automatic) looping commands after
    some specified timeout.
  * bulk proof of several proof attempts in different theories,
    with automatic switching between theories.
- The SyncExec wrapper adapts the overall asynchronous
  architecture of I3P to the requirement of synchronous processing
  as necessary for testing or background proving. Its (straightforward)
  implementation shows how to work with the signalling mechanisms
  about changes in the processing state of some command in order to
  wait for the completion of processing.

The new facade, as well as the most important API classes of the
infrastructure module IAPP, have JavaDoc explanations attached. Please
get back to me if I omitted some lazily, such that I can supply them lazily.

Hope this helps,

 Holger


On 02/17/2012 06:13 PM, Matthias Schmalz wrote:
> Hi,
> 
> I am trying to use the scala library Pure.jar to communicate with the Isabelle
> process. A typical use case is to send a theory snipped like the following and
> to check whether the proof attempt succeeds:
> 
> theory Test imports Main begin
> 
> lemma foo:
> fixes x :: bool
> assumes "x = True"
> shows "x | x"
> using assms
> by simp
> 
> I have already discovered the Isabelle_System.init method and I am aware of the
> classes "Isabelle_Process" and "Session". My attempts to communicate the above
> snippet to an Isabelle_Process failed due to my unawareness of the input format
> of Isabelle_Process.input. (Perhaps, this is not the intended interface anyway?)
> I also tried to use Session.init_node, but I am not sure how to choose the
> parameters and how to receive the result.
> 
> I would appreciate any help on this very much!
> 
> Best,
> Matthias
> 
/*
 * Copyright (c) 2012
 *  Universitaet Tuebingen.
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions 
 * are met:
 *
 * * Redistributions of source code must retain the above copyright 
 *  notice, this list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright 
 *   notice, this list of conditions and the following disclaimer in the 
 *   documentation and/or other materials provided with the distribution.
 *
 * * Neither the name of the University of Tuebingen nor the names of
 *   the contributors may be used to endorse or promote products derived
 *   from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 */
package org.i3p.apiaccess;

import org.isabelle.iapp.process.Message;
import org.isabelle.iapp.process.ProverProcessException;
import org.isabelle.iapp.proofdocument.Command;
import javax.swing.text.DefaultStyledDocument;
import java.io.File;
import javax.swing.text.BadLocationException;
import javax.swing.text.Document;
import javax.swing.text.PlainDocument;
import org.isabelle.drivers.tests.DumpIsabelleListener;
import org.isabelle.iapp.facade.IAPP;
import org.isabelle.iapp.installations.Configuration;
import org.isabelle.iapp.process.ProverInstance;
import org.isabelle.iapp.process.ProverManager;
import org.isabelle.iapp.process.features.InjectedCommands;
import org.isabelle.iapp.proofdocument.AbstractDocumentRepresentation;
import org.isabelle.iapp.proofdocument.CommandExecutionError;
import org.isabelle.iapp.proofdocument.ProofDocument;
import org.isabelle.iapp.proofdocument.SyncExec;
import org.isabelle.iapp.util.StyledDocumentDocumentRepresentation;
import org.isabelle.isabelle2009driver.Isabelle2009Configuration;
import org.isabelle.isabelle2009driver.Isabelle2011_1Driver;
import org.isabelle.isainstall.RootDirInstallation;
import org.junit.After;
import org.junit.AfterClass;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;
import static org.junit.Assert.*;
import org.openide.util.Exceptions;

/**
 * Demonstrate the use of { at link IsabelleFacade} by executing tests representing
 * (supposed) standard use-cases of background proof checking. The comments
 * in the source explain the steps.
 * 
 * <p>A different approach to executing commands is through the
 * { at link InjectedCommands} feature, which is supported by the Isabelle
 * driver. The usage of this can be found in the test InjectedCommandsTest
 * contained in the driver module. Injected commands are useful primarily
 * in interactive settings, where some UI component wishes to communicate
 * with Isabelle apart from normal theory processing, usually for querying
 * some state. Please contact me if you need more information on that.
 *
 * @author gast at informatik.uni-tuebingen.de
 */
public class RunningTheoriesTest {
    public static final String ISABELLE_HOME = "/usr/local/Isabelle/Isabelle2011-1";
    public static final String ISABELLE_LOGIC = "HOL";
    private IsabelleFacade isabelle;

    @Before
    public void setup() throws ProverProcessException {
        isabelle = new IsabelleFacade(ISABELLE_HOME, ISABELLE_LOGIC, new Isabelle2011_1Driver());
        isabelle.startup();
    }

    @After
    public void tearDown() throws ProverProcessException {
        if (isabelle.isRunning()) {
            isabelle.shutdown();
        }
    }

    @Test
    public void runGeneratedTheoryTest() throws Exception {
        // dump the messages for demo purposes
        isabelle.getProver().addProverMessageListener(new DumpIsabelleListener());

        // make a buffer to hold the theory, which is connected to the
        // IAPP infrastructure.
        DefaultStyledDocument doc = new DefaultStyledDocument();
        ProofDocument proofDoc = isabelle.createProofDocument(doc, "/tmp/Test.thy");

        // create some theory text
        fillSucceedTheory(doc);

        // everything in the IAPP is asynchronous, in particular
        // the structuring of text into commands. We therefore
        // wait until this structuring is complete.
        proofDoc.awaitStable();

        // demo: show the split commands
        for (Command cmd : proofDoc.getCommands()) {
            System.out.println(cmd);
        }

        // now we can execute/undo the commands
        Command last = proofDoc.getLastCommand();

        // Command execution is asynchronous. However,
        // for testing and background usage, a synchronous
        // wrapper is available.        
        //
        // Its behaviour is defined as follows:
        // - sends commands to Isabelle
        // - fails if any command fails
        // - returns after timeout 2sec; throws exception if
        //   timeout expires
        SyncExec.sendAndWait(last, 2000);

        // demo: of course, the last command has now been executed
        assertTrue(last.getState().isSuccess());

        // demo: now show processing messages of all commands
        for (Command cmd : proofDoc.getCommands()) {
            System.out.println(cmd);
            for (Message m : cmd.getState().getProcessingResults()) {
                System.out.println("  " + m);
            }
        }
    }

    @Test
    public void failingProof() throws Exception {
        DefaultStyledDocument doc = new DefaultStyledDocument();
        ProofDocument proofDoc = isabelle.createProofDocument(doc, "/tmp/TestFail.thy");
        fillFailTheory(doc);
        proofDoc.awaitStable();
        try {
            SyncExec.sendAndWait(proofDoc.getLastCommand(), 2000);
            fail();
        } catch (CommandExecutionError err) {
            // demo: we get the command that caused the overall execution to fail.
            assertNotNull(err.getTarget());
            assertEquals("by simp", err.getError().getText());
        }
    }

    @Test
    public void timeoutTest() throws Exception {
        DefaultStyledDocument doc = new DefaultStyledDocument();
        ProofDocument proofDoc = isabelle.createProofDocument(doc, "/tmp/TestTimeout.thy");
        fillTimeoutTheory(doc);
        proofDoc.awaitStable();
        try {
            SyncExec.sendAndWait(proofDoc.getLastCommand(), 2000);
            // this should never be reached
            fail();
        } catch (CommandExecutionError err) {
            System.out.println(">>OK: timeout on exec reached");
            assertTrue(err.isTimeout());
            // we could now use to cancel the execution
            // SyncExec.revokeAndWait(proofDoc.getLastCommand(), 2000);
        }

        // When we reach this point, the Isabelle instance is still
        // processing the looping command - only we stopped to wait for
        // it. In typical scenarios, one would now just attempt the next proof,
        // which is precisely what we do here. The IAPP keeps sending INT
        // signals to the process until the looping command returns, and
        // then starts processing the next theory.
        doc = new DefaultStyledDocument();
        ProofDocument proofDoc2 = isabelle.createProofDocument(doc, "/tmp/TestAfterTimeout.thy");
        fillSucceedTheory(doc);
        proofDoc2.awaitStable();
        System.out.println(">>goto different theory, will send INT");
        SyncExec.sendAndWait(proofDoc2.getLastCommand(), 5000);
        assertTrue(proofDoc2.getLastCommand().getState().isSuccess());
    }

    @Test
    public void bulkProofs() throws Exception {
        // we now demonstrate a typical background usage: we send one
        // attempt at a time, as before. The IAPP then keeps track of
        // the prover state and does the necessary theory switching etc.
        // in the background.
        for (int i = 0; i != 30; i++) {
            DefaultStyledDocument doc = new DefaultStyledDocument();
            ProofDocument proofDoc = isabelle.createProofDocument(doc, "Test" + i + ".thy");
            fillSucceedTheory(doc);
            proofDoc.awaitStable();

            Command last = proofDoc.getLastCommand();
            SyncExec.sendAndWait(last, 3000);
            assertTrue(last.getState().isSuccess());
            System.out.println("Done with test " + i);
            // Note that by the previous tests such bulk proofs are
            // also feasible for failing and looping commands.
        }

    }

    private void fillSucceedTheory(DefaultStyledDocument doc) throws BadLocationException {
        doc.insertString(doc.getLength(), "theory Test imports Main begin\n", null);
        doc.insertString(doc.getLength(), "lemma foo:\n", null);
        doc.insertString(doc.getLength(), "fixes x :: bool\n", null);
        doc.insertString(doc.getLength(), "assumes \"x = True\"\n", null);
        doc.insertString(doc.getLength(), "shows \"x | x\"\n", null);
        doc.insertString(doc.getLength(), "using assms\n", null);
        doc.insertString(doc.getLength(), "by simp", null);
    }

    private void fillFailTheory(DefaultStyledDocument doc) throws BadLocationException {
        doc.insertString(doc.getLength(), "theory Test imports Main begin\n", null);
        doc.insertString(doc.getLength(), "lemma foo:\n", null);
        doc.insertString(doc.getLength(), "fixes x :: bool\n", null);
        doc.insertString(doc.getLength(), "assumes \"x = False\"\n", null);
        doc.insertString(doc.getLength(), "shows \"x = True\"\n", null);
        doc.insertString(doc.getLength(), "using assms\n", null);
        doc.insertString(doc.getLength(), "by simp", null);
    }

    private void fillTimeoutTheory(DefaultStyledDocument doc) throws BadLocationException {
        doc.insertString(doc.getLength(), "theory Test imports Main begin\n", null);
        doc.insertString(doc.getLength(), "lemma foo:\n", null);
        doc.insertString(doc.getLength(), "fixes x y z\n", null);
        doc.insertString(doc.getLength(), "shows \"x & y & z\"\n", null);
        doc.insertString(doc.getLength(), "by (simp add: conj_assoc[symmetric])", null);
    }
}


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.