Update install instruction READMEs

.github/workflows/docker-publish.yml

@@ -20,7 +20,7 @@ env:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     steps:
       - name: Checkout
         uses: actions/checkout@v4

INSTALL.MacOS

@@ -70,9 +70,11 @@ cd ~
 mkdir workspace
 cd workspace
 git clone https://github.com/ontologyportal/sigmakee
+cd sigmakee
 
 Install (ensure the above preparations have been performed)
 > ant install
+> ant
 
 *** Legacy install steps now taken care of by the above command "ant install"
 cd ~
@@ -104,7 +106,7 @@ and try to uncompress again:
 cp -iav WordNet-3.0/dict/* ~/workspace/sumo/WordNetMappings/
 rm WordNet-3.0.tar.gz
 
-curl -O 'https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.0/E.tgz'
+curl -O 'http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_3.1/E.tgz'
 tar xvzf E.tgz
 rm E.tgz
 cd E

README.md

@@ -335,6 +335,7 @@ Then,
 ```sh
 cd sigmakee
 ant install
+ant
 ```
 
 To keep this repository updated
@@ -352,7 +353,7 @@ mkdir Programs
 cd Programs
 wget 'https://archive.apache.org/dist/tomcat/tomcat-9/v9.0.97/bin/apache-tomcat-9.0.97.zip'
 wget 'https://wordnetcode.princeton.edu/3.0/WordNet-3.0.tar.gz'
-wget 'https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.0/E.tgz'
+wget 'http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_3.1/E.tgz'
 tar -xvzf E.tgz
 unzip apache-tomcat-9.0.97.zip
 rm apache-tomcat-9.0.97.zip

build.xml

@@ -95,8 +95,6 @@
     <property name="build.classes.dir" value="${build.home}/WEB-INF/classes"/>
     <property name="build.lib" value="${build.home}/lib"/>
     <property name="build.test.classes.dir" value="${build.home}/test/classes"/>
-    <property name="dist.dir" value="dist"/>
-    <property name="dist.jar" value="${dist.dir}/${app.name}.jar"/>
     <property name="dist.javadoc.dir" value="doc"/>
     <property name="web.dir" value="web"/>
     <property name="reports.dir" value="${build.home}/test/results"/>
@@ -235,7 +233,7 @@
         <mkdir dir="${reports.dir}"/>
     </target>
 
-    <target name="dist" depends="compile" description="Create the *.war file and place in ${dist.dir}.">
+    <target name="dist" depends="compile,compile.test" description="Create the *.war file and place in $CATALINA_HOME/webapps/sigma, create sigmakee.jar.">
         <manifest file="${manifest.mf}">
             <attribute name="Built-By" value="${user.name}"/>
             <attribute name="Specification-Title"
@@ -360,7 +358,6 @@
     <target name="clean" description="Delete old build, lib, dist and deployed web aritifacts">
         <delete includeemptydirs="true" failonerror="false">
             <fileset dir="${build.home}"/> <!-- avoid problems with package name changes by deleting everything -->
-            <fileset dir="${dist.dir}"/>
             <!-- Delete the old web code -->
             <fileset dir="${deploy.home}"/>
             <fileset dir="${tomcat.home}/work/Catalina/localhost/${web.app.name}"/>
@@ -415,7 +412,7 @@
     </target>
 
     <target name="retrieve.E">
-        <get src="https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.0/E.tgz" dest="${programs.dir}" tryGzipEncoding="true"/>
+        <get src="http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_3.1/E.tgz" dest="${programs.dir}" tryGzipEncoding="true"/>
         <untar src="${programs.dir}/E.tgz" dest="${programs.dir}" compression="gzip"/>
         <delete file="${programs.dir}/E.tgz"/>
     </target>
@@ -562,7 +559,7 @@
         </exec>
     </target>
 
-    <!-- If Vampire fails to build on Hamming, here is a alternate source of the binary -->
+    <!-- If Vampire fails to build on Hamming, here is an alternate source of the binary -->
     <target name="alternate.vampire">
         <get src="https://github.com/vprover/vampire/releases/download/v4.9casc2024/vampire" dest="${programs.dir}/vampire/build" tryGzipEncoding="true"/>
         <chmod dir="${programs.dir}/${programs.dir}/vampire/build" perm="ugo+rx" includes="vampire"/>

config.xml

@@ -25,7 +25,7 @@
   <preference name="sumokbname" value="SUMO" />
   <preference name="systemsDir" value="/home/theuser" />
   <preference name="termFormats" value="no" />
-  <preference name="testOutputDir" value="/var/tomcat/apache-tomcat-9.0.97/webapps/sigma/tests" />
+  <preference name="testOutputDir" value="/usr/local/tomcat/apache-tomcat-9.0.97/webapps/sigma/tests" />
   <preference name="TPTPDisplay" value="no" />
   <preference name="tptpHomeDir" value="/home/theuser" />
   <preference name="TPTP" value="yes" />

docker/sigma-ci/Dockerfile

@@ -1,36 +1,70 @@
 FROM tomcat:9.0.97-jdk21-temurin-jammy AS builder
 
-# Followed instructions from: https://github.com/vprover/vampire/wiki/Source-Build-for-Users
-# for buildling latest vampire w/ latest z3
-
-RUN apt update; \
-    apt-get install -y --no-install-recommends \
-            build-essential \
-            cmake \
-            git \
-            python3 \
-    ;\
-    wget 'http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.6/E.tgz' &&\
-    tar xf E.tgz ;\
+# Follow instructions from: https://github.com/vprover/vampire/wiki/Source-Build-for-Users
+# for buildling the latest vampire w/ latest z3
+
+# Here, we are utilizing a known Vampire build w/ Z3 matched to that build
+ARG VAMPIRE_GIT='https://github.com/vprover/vampire/archive/refs/tags/v4.9casc2024.tar.gz'
+ARG Z3_GIT='https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz'
+# Latest E Theorem Prover (2024-05-01)
+ARG E_PROVER='http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_3.1/E.tgz'
+ARG WORD_NET='https://wordnetcode.princeton.edu/3.0/WordNet-3.0.tar.gz'
+
+# We're in /usr/local/tomcat
+RUN apt-get update && apt-get install -y --install-recommends \
+    build-essential \
+    cmake \
+    git \
+    python3 ;\
+    wget $E_PROVER && tar xf E.tgz ;\
     cd E ;\
-    ./configure && make ;\
+    ./configure && make -j2 ;\
     cd .. ;\
-    wget 'https://wordnetcode.princeton.edu/3.0/WordNet-3.0.tar.gz' ;\
-    tar xf WordNet-3.0.tar.gz ;\
+    wget $WORD_NET && tar xf WordNet-3.0.tar.gz ;\
     git clone https://github.com/vprover/vampire ;\
     cd vampire ;\
     git submodule update --init ;\
     mkdir build ;\
-    mkdir z3/build && cd z3/build ;\
+    mkdir -p z3/build && cd z3/build ;\
     cmake .. -DZ3_SINGLE_THREADED=1 -DCMAKE_BUILD_TYPE=Release ;\
-    make -j`nproc` ;\
+    make -j2 ;\
     cd ../../build ;\
     cmake .. ;\
-    make -j`nproc` ;\
+    make -j2 ;\
     cd .. ;\
     cp build/vampire vampire ;\
     ./checks/sanity vampire
 
+#RUN apt update && apt install -y --install-recommends \
+#    build-essential \
+#    clang \
+#    cmake \
+#    git \
+#    python3 ;\
+#    wget $E_PROVER &&\
+#    tar xf E.tgz ;\
+#    cd E ;\
+#    ./configure && make CC="clang" CXX="clang++" ;\
+#    cd .. ;\
+#    wget $WORD_NET &&\
+#    tar xf WordNet-3.0.tar.gz ;\
+#    wget $VAMPIRE_GIT &&\
+#    tar -xzf v4.9casc2024.tar.gz ;\
+#    wget $Z3_GIT &&\
+#    tar -xzf z3-4.12.3.tar.gz ;\
+#    mv z3-z3-4.12.3/* vampire-4.9casc2024/z3 ;\
+#    cd vampire-4.9casc2024 ;\
+#    mkdir build ;\
+#    mkdir -p z3/build && cd z3/build ;\
+#    CC=clang CXX=clang++ cmake .. -DZ3_SINGLE_THREADED=1 -DCMAKE_BUILD_TYPE=Release ;\
+#    make -j`nproc` ;\
+#    cd ../../build ;\
+#    CC=clang CXX=clang++ cmake .. ;\
+#    make -j`nproc` ;\
+#    cd .. ;\
+#    cp build/bin/vampire_* vampire ;\
+#    ./checks/sanity vampire
+
 #################################################
 # runtime image.
 FROM tomcat:9.0.97-jdk21-temurin-jammy AS runtime
@@ -41,15 +75,20 @@ COPY --from=builder \
 COPY --from=builder \
     /usr/local/tomcat/WordNet-3.0 /opt/WordNet-3.0
 
+#COPY --from=builder \
+#    /usr/local/tomcat/vampire-4.9casc2024/vampire /usr/local/bin/vampire
+#
+#COPY --from=builder \
+#    /usr/local/tomcat/vampire-4.9casc2024/z3/build/libz3.* /usr/local/bin/
+
 COPY --from=builder \
     /usr/local/tomcat/vampire/vampire /usr/local/bin/vampire
 
 COPY --from=builder \
     /usr/local/tomcat/vampire/z3/build/libz3.* /usr/local/bin/
 
-RUN apt update; \
-    apt-get install -y --no-install-recommends \
-            ant \
-            ant-optional \
-            git \
-            graphviz
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    ant \
+    ant-optional \
+    git \
+    graphviz

docker/sigmakee/Dockerfile

@@ -5,15 +5,8 @@
 # runtime image.
 FROM tomcat:9.0.97-jdk21-temurin-jammy AS runtime
 
-# Switch to root user
-USER root
-
-RUN apt update && apt-get install -y --no-install-recommends \
-            sudo \
-            graphviz
-
-# Set kernel parameter
-RUN sysctl -w kernel.perf_event_paranoid=-1
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    graphviz
 
 COPY --from=builder \
     /usr/local/bin/e_ltb_runner /usr/local/bin/e_ltb_runner
@@ -35,4 +28,4 @@
 
 ENV SIGMA_HOME=/root/sigmakee-runtime
 ENV LD_LIBRARY_PATH=/usr/local/bin:$LD_LIBRARY_PATH
 ENV CATALINA_OPTS="$CATALINA_OPTS -Xmx10g -Xss1m"

docker/sumo-ci/Dockerfile

@@ -5,15 +5,8 @@ FROM $IMAGE_ACCOUNT/sigma-ci:latest AS builder
 # runtime image.
 FROM tomcat:9.0.97-jdk21-temurin-jammy AS runtime
 
-# Switch to root user
-USER root
-
-RUN apt update && apt-get install -y --no-install-recommends \
-            sudo \
-            graphviz
-
-# Set kernel parameter
-RUN sysctl -w kernel.perf_event_paranoid=-1
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    graphviz
 
 COPY --from=builder \
     /usr/local/bin/e_ltb_runner /usr/local/bin/e_ltb_runner

nbproject/build.properties

@@ -20,8 +20,8 @@ debug.test.modulepath=\
 # Files in build.classes.dir which should be excluded from distribution jar
 dist.archive.excludes=
 # This directory is removed when the project is cleaned:
-#dist.dir=dist
-#dist.jar=${dist.dir}/${app.name}.jar
+dist.dir=dist
+dist.jar=${dist.dir}/${app.name}.jar
 #dist.javadoc.dir=${dist.dir}/doc/api
 excludes=
 file.reference.src-java=src/java