Merge pull request #167 from terry-norbraten/master

Fine tune the CI/CD and use ProcessBuilder to produce proof image as SVG

Author: apease

.github/workflows/ant.yml

@@ -158,7 +158,7 @@ jobs:
           name: sigma-webapp
           path: /usr/local/tomcat/webapps/sigma.war
 
-  build-sumo-ci:
+  build-sumo-ci-and-sigmakee:
     runs-on: ubuntu-latest
     needs: build
     steps:

.github/workflows/docker-publish.yml

@@ -36,15 +36,15 @@ jobs:
           password: ${{ secrets.DOCKERHUB_TOKEN }}
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2
+        uses: docker/setup-buildx-action@v3
 
       - name: Set image account name
         env:
           DOCKER_ACCOUNT: ${{ secrets.DOCKERHUB_USERNAME }}
         run: |
           echo "IMAGE_ACCOUNT=${DOCKER_ACCOUNT:-$DEFAULT_DOCKER_ACCOUNT}" >> $GITHUB_ENV
 
-      - name: Build and push
+      - name: Build and push sigma-ci
         uses: docker/build-push-action@v6
         with:
           context: .

docker/sigma-ci/Dockerfile

@@ -49,7 +49,7 @@ RUN apt-get update && apt-get install -y --install-recommends \
 #    wget $E_PROVER &&\
 #    tar xf E.tgz ;\
 #    cd E ;\
-#    ./configure && make CC="clang" CXX="clang++" ;\
+#    ./configure && make -j`nproc` CC="clang" CXX="clang++" ;\
 #    cd .. ;\
 #    wget $WORD_NET &&\
 #    tar xf WordNet-3.0.tar.gz ;\

docker/sigmakee/Dockerfile

@@ -20,9 +20,16 @@ COPY --from=builder \
 COPY --from=builder \
     /usr/local/bin/libz3.* /usr/local/bin/
 
-COPY ./sigmakee-runtime /root/sigmakee-runtime/
-
+# Just the essentials
+COPY ./sigmakee-runtime/KBs/config.xml /root/sigmakee-runtime/KBs/
+COPY ./sigmakee-runtime/KBs/*.kif /root/sigmakee-runtime/KBs/
+COPY ./sigmakee-runtime/KBs/Translations /root/sigmakee-runtime/KBs/
+COPY ./sigmakee-runtime/KBs/WordNetMappings /root/sigmakee-runtime/KBs/
+COPY ./sigmakee-runtime/KBs/development /root/sigmakee-runtime/KBs/
+
+# Not necessary since everything is in the WAR
 COPY ./sigmakee/build/WEB-INF/lib/*.jar /root/sigmakee/
+COPY ./sigmakee/build/sigmakee.jar /root/sigmakee/
 
 COPY ./sigma.war $CATALINA_HOME/webapps/sigma.war
 

docker/sumo-ci/Dockerfile

@@ -20,7 +20,7 @@ COPY --from=builder \
 COPY --from=builder \
     /usr/local/bin/libz3.* /usr/local/bin/
 
-COPY ./sigmakee-runtime /root/sigmakee-runtime/
+COPY ./sigmakee-runtime/KBs/config.xml /root/sigmakee-runtime/KBs/
 
 COPY ./sigmakee/build/WEB-INF/lib/*.jar /root/sigmakee/
 

nbproject/build.properties

@@ -125,48 +125,6 @@ kbs_home=../sumo
 #spec.vendor=Adam Pease
 project.license=LICENSE
 
-# Can't override immutable props
-#main.class=com.articulate.sigma.KB
-#run.class=com.articulate.sigma.KButilities
-run.class=${main.class}
-
-# Various runtime arguments here
-
-# Intentional empty arguments
-#run.args=
-
-# Default run for the KB
-#run.args=-c Object Transaction
-
-# Load KB files w/ KButilities (should regenerate the KB if cleaned). Add -N for
-# sequential (slower) processing <- original implementation
-#run.args=-l
-run.args=-f ${vamp.out.file}
-
-# KB.cache
-#run.args=-a
-
-# Run Vampire on SUMO.tptp and output proof
-#run.args=-p
-
-# KB, KIF, TPTP3ProofProcessor, TPTPutil, SUMOtoTFAform - run a test
-#run.args=-t
-
-# Formula check for errors
-formula='(=> (and (muscleInsertion ?MC ?BPC) (instance ?H Human) (attribute ?H Healthy)) (exists (?M ?BP) (and (instance ?M ?MC) (instance ?BP ?BPC) (part ?M ?H) (part ?BP ?H) (connects ?M ?BP))))'
-
-# Error checking a formula w/ com.articulate.sigma.KButilities
-#run.args=-v ${formula}
-
-# Test internal clause in TPTP2SUMO
-#run.args=-c
-
-# Translate KB to TFF, no args
-# run com.articulate.sigma.trans.SUMOKBtoTFAKB
-
-# Translate KB to FOF, no args
-# run com.articulate.sigma.trans.SUMOKBtoTPTPKB
-
 # Tomcat Manager properties
 catalina.ops=-Xmx10g -Xss1m
 catalina.base=${catalina.home}
@@ -201,27 +159,87 @@ test.integration.resources.dir=${test.integration.dir}/resources
 #unit.test.suite=com.articulate.sigma.UnitTestSuite
 #integration.test.suite=com.articulate.sigma.IntegrationTestSuite
 
+# Can't override immutable props
+#main.class=com.articulate.sigma.KB
+#run.class=${main.class}
+# Load KB files w/ KButilities (should regenerate the KB if cleaned). Add -N for
+# sequential (slower) processing <- original implementation
+#run.args=-l
+# Default run for checking KB operation
+#run.args=-c Object Transaction
+
+#run.class=com.articulate.sigma.KButilities
+# Formula check for errors
+formula='(=> (and (muscleInsertion ?MC ?BPC) (instance ?H Human) (attribute ?H Healthy)) (exists (?M ?BP) (and (instance ?M ?MC) (instance ?BP ?BPC) (part ?M ?H) (part ?BP ?H) (connects ?M ?BP))))'
+# Error checking a formula w/ com.articulate.sigma.KButilities
+#run.args=-v ${formula}
+
+#run.class=com.articulate.sigma.KBcache
+#run.args=-a
+
+# WordNet term search
+#run.class=com.articulate.sigma.wordNet.WordNet
+#run.args=-w Cat
+
+# KB, KIF, TPTP3ProofProcessor, TPTPutil, SUMOtoTFAform - run a test
+#run.args=-t
+
+# Test internal clause in TPTP2SUMO
+#run.class=com.articulate.sigma.trans.TPTP2SUMO
+#run.args=-c
+
+### Ontology Process
+
+# (1) Generates FOF, no args
+#run.class com.articulate.sigma.trans.SUMOKBtoTPTPKB
+#run.args=
+# or
+# (1) Generates TFF, no args
+#run.class=com.articulate.sigma.trans.SUMOKBtoTFAKB
+#run.args=
+
+# (2 & 3) Runs Vampire on ~.sigmakee/KBs/SUMO.tptp, produces and analyzes proof
+#run.class=com.articulate.sigma.tp.Vampire
+#run.args=-p
+# or
+# (2) run: ant run.vampire
+# (3) Analyzes proof after CLI run of Vampire
+#run.class=com.articulate.sigma.trans.TPTP3ProofProcessor
+#run.args=-f ${vamp.out.file}
+
+# (4) View the proof
+# run: ant open.dot.image
+
+### end Ontology Process
+
 # Vampire
 
 # default timeout is 60 if -t is not specified
 # NOTE: [- -mode casc] is a shortcut for [- -mode portfolio -sched casc -p tptp]
 #tptp.file=${workspace}/sigmakee/nbproject/private/resources/tiny/SUMO.tptp
+#vamp.out.file=${workspace}/sigmakee/nbproject/private/resources/tiny/vamp-out.txt
 tptp.file=${sigma_home}/KBs/SUMO.tptp
 vamp.out.file=${sigma_home}/KBs/vamp-out.txt
-#vamp.out.file=${workspace}/sigmakee/nbproject/private/resources/tiny/vamp-out.txt
-#vamp.args=--mode casc -t 900 ${tptp.file} &amp;> ${vamp.out.file}
-vamp.args=--cores 0 --mode portfolio --schedule snake_tptp_uns -p tptp --input_syntax tptp --output_axiom_names on -t 10 ${tptp.file} &> ${vamp.out.file}
+vamp.time=-t 900
+#vamp.args=--mode casc ${vamp.time} ${tptp.file} &amp;> ${vamp.out.file}
+vamp.args=--cores 0 --mode portfolio --schedule snake_tptp_uns -p tptp --input_syntax tptp --output_axiom_names on ${vamp.time} ${tptp.file} &> ${vamp.out.file}
 
-dot.file='${deploy_home}/graph/proof.dot'
 dot.cmd=/usr/local/bin/dot
-dot.args=-Tsvg -Kosage -O ${dot.file}
+image.ext=svg
+# default: dot
+#dot.layout=
+dot.layout=-Kdot
+dot.file='${deploy_home}/graph/proof.dot'
+dot.args=-T${image.ext} ${dot.layout} -O ${dot.file}
+dot.image.file=${dot.file}.${image.ext}
 
+# PasswordService
 #System.out.println("PasswordService: ");
 #System.out.println("-h    show this Help message");
 #System.out.println("-l    Login");
 #System.out.println("-c    Create db");
 #System.out.println("-a    create Admin user");
-#
+
 #System.out.println("-u    show User IDs");
 #System.out.println("-r    Register a new username and password (fail if username taken)");
 #System.out.println("-a3 <u> <p> <e>  create Admin user");

nbproject/ide-targets.xml

@@ -564,7 +564,7 @@
         <copy tofile="${sigma_home}/KBs/config.xml" file="${tiny.sumo.config}" overwrite="true"/>
     </target>
     <target name="thorough.clean" depends="clean">
-        <antcall target="kb.clean"/>
+        <antcall target="clean.kbs"/>
         <delete includeemptydirs="true" failonerror="false">
             <!-- Delete the old web code -->
             <fileset dir="${deploy_home}"/>
@@ -615,7 +615,7 @@
     =========
     -->
 
-    <target name="run.vampire" depends="init" description="Assumes that ${sigma_home}/KBs/SUMO.tptp has already been generated">
+    <target name="run.vampire" depends="init" description="Assumes that ${sigma_home}/KBs/SUMO.* has already been generated">
         <exec executable="sh">
             <arg value="-c"/>
             <arg value="${programs.dir}/vampire/build/vampire ${vamp.args}"/>
@@ -629,6 +629,14 @@
             <arg value="-c"/>
             <arg value="${dot.cmd} ${dot.args}"/>
         </exec>
+        <antcall target="open.dot.image"/>
+    </target>
+
+    <target name="view.dot.image" depends="init" description="Open the image produces by GraphViz">
+        <exec executable="sh" osfamily="mac">
+            <arg value="-c"/>
+            <arg value="open -a 'Google Chrome' ${dot.image.file}"/>
+        </exec>
     </target>
 
 </project>

src/java/com/articulate/sigma/tp/Vampire.java

@@ -359,15 +359,8 @@ else if (args.length > 0 && args[0].equals("-p")) {
                 StringBuilder answerVars = new StringBuilder("?X ?Y ?Z");
                 System.out.println("input: " + vampire.output + "\n");
                 tpp.parseProofOutput(vampire.output, query, kb, answerVars);
-
-                String sep = File.separator;
-                dir = System.getenv("CATALINA_HOME") + sep + "webapps"
-                + sep + "sigma" + sep + "graph";
-                File webGphDir = new File(dir);
-                if (!webGphDir.exists())
-                    webGphDir.mkdirs();
                 tpp.createProofDotGraph();
-                
+
                 System.out.println("Vampire.main(): " + tpp.proof.size() + " steps ");
                 System.out.println("Vampire.main() bindings: " + tpp.bindingMap);
                 System.out.println("Vampire.main() skolems: " + tpp.skolemTypes);

src/java/com/articulate/sigma/trans/TPTP3ProofProcessor.java

@@ -1150,7 +1150,7 @@ private void createProofDotGraphImage(String filename) throws IOException {
         List<String> cmd = new ArrayList<>();
         cmd.add(graphVizDir + File.separator + "dot");
         cmd.add("-T" + imageExt);
-        cmd.add("-Kosage");
+        cmd.add("-Kdot");
         cmd.add("-O");
         cmd.add(filename + ".dot");
         try {
@@ -1484,10 +1484,10 @@ public static void main(String[] args) throws IOException {
                     tpp.parseProofOutput(lines, query, kb, answerVars);
                     tpp.createProofDotGraph();
                     System.out.println("TPTP3ProofProcessor.main(): " + tpp.proof.size() + " steps ");
-                    Formula f;
+                    Formula f = new Formula();
                     for (TPTPFormula step : tpp.proof) {
                         System.out.println(":: " + step);
-                        f = new Formula(step.sumo);
+                        f.setFormula(step.sumo);
                         System.out.println(f.format("", "  ", "\n"));
                     }
                     System.out.println("TPTP3ProofProcessor.main() bindings: " + tpp.bindingMap);