spechub · b-gehrke · Jan 19, 2023 · Jan 19, 2023 · Jan 19, 2023 · Feb 4, 2023
diff --git a/.dockerignore b/.dockerignore
@@ -0,0 +1,18 @@
+.github/**
+.gitignore
+.travis.yml
+LIZENZ.txt
+README*
+_parameters
+debian/**
+doc/**
+ideas
+pretty/**
+sample-ghci-script
+todo*
+**.tex
+**.pdf
+Docker/**
+GMP/CoLoSS/data/GMP.tar.gz
+GMP/papers/**
+HolLight/OcamlTools/**
diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
@@ -0,0 +1,21 @@
+name: Deploy Sphinx documentation to Pages
+
+on:
+  push:
+    branches: [master] # branch to trigger deployment
+
+jobs:
+  pages:
+    runs-on: ubuntu-20.04
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    permissions:
+      pages: write
+      id-token: write
+    steps:
+    - id: deployment
+      uses: sphinx-notes/pages@v3
+      with:
+        documentation_path: ./python/api/docs
+        requirements_path: ./python/api/docs/requirements.txt
diff --git a/.gitignore b/.gitignore
@@ -15,16 +15,16 @@ rev.txt
 *.orig
 .stack-work/
 stack
-doc/*.aux
-doc/*.bbl
-doc/*.blg
-doc/*.fdb_latexmk
-doc/*.fls
-doc/*.log
-doc/*.out
-doc/UserGuide.pdf
-doc/hs2isa.ps
-docs/
+/doc/*.aux
+/doc/*.bbl
+/doc/*.blg
+/doc/*.fdb_latexmk
+/doc/*.fls
+/doc/*.log
+/doc/*.out
+/doc/UserGuide.pdf
+/doc/hs2isa.ps
+/docs/
 __pycache__
 .idea
 programatica/
@@ -199,3 +199,6 @@ NeSyPatterns/AS.hs
 NeSyPatterns/ATC_NeSyPatterns.der.hs
 NeSyPatterns/ATC_NeSyPatterns.hs
 OWL2/scripts/runTest
+*.gresource
+/python/api/docs/_build
+/python/api/docs/code
diff --git a/CMDL/Interface.hs b/CMDL/Interface.hs
@@ -22,7 +22,8 @@ import Comorphisms.LogicGraph (logicGraph)
 import Logic.Grothendieck
 #endif
 
-import Proofs.AbstractState (getListOfConsCheckers, usableCC)
+import Proofs.AbstractState (getAllConsCheckers, sublogicOfTheory, getCcName
+                            , getListOfConsCheckers, usableCC)
 
 import System.IO
 

diff --git a/Common/Consistency.hs b/Common/Consistency.hs
@@ -26,7 +26,7 @@ import Data.Data
      required for extending imports (no confusion) in Maude -}
 data Conservativity =
     Inconsistent
-  | Unknown String
+  | Unknown { conservativityUnknownReason :: String}
   | None
   | PCons
   | Cons
@@ -53,8 +53,7 @@ translated sentence of the source. -}
 data ConservativityChecker sign sentence morphism = ConservativityChecker
     { checkerId :: String
     , checkerUsable :: IO (Maybe String)
-    , checkConservativity
-        :: (sign, [Named sentence])
-        -> morphism
-        -> [Named sentence]
-        -> IO (Result (Conservativity, [sentence])) }
+    , checkConservativity :: (sign, [Named sentence]) -- source or initial signature and sentences
+        -> morphism                                   -- morphism between specs
+        -> [Named sentence]                           -- target sentences of extended spec
+        -> IO (Result (Conservativity, [sentence])) } -- conservativity with obligations of the extensions
diff --git a/Common/GtkGoal.hs b/Common/GtkGoal.hs
@@ -88,8 +88,8 @@ proofStatusToGStatus p = case goalStatus p of
   Proved False -> GInconsistent
   Proved True -> GProved
   Disproved -> GDisproved
-  Open (Reason s) ->
-    if any (isInfixOf "timeout" . map toLower) s then GTimeout else GOpen
+  Open reason ->
+    if any (isInfixOf "timeout" . map toLower) reason then GTimeout else GOpen
 
 -- | Converts a BasicProof into a GStatus
 basicProofToGStatus :: BasicProof -> GStatus

diff --git a/Docker/hetsapi.Dockerfile b/Docker/hetsapi.Dockerfile
@@ -1,58 +1,101 @@
-FROM hyphen:20.04
+FROM spechub2/hyphen:22.04 as base
 
-ENV TZ=Europe/Berlin
-RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
-
-RUN apt-get update && apt-get -y install locales && locale-gen en_US.UTF-8
+ENV TZ Europe/Berlin
 ENV LANG en_US.UTF-8
 ENV LANGUAGE en_US:en
 ENV LC_ALL en_US.UTF-8
+ENV HETS_LIB /opt/Hets-lib
 
-RUN apt-get install -y software-properties-common apt-utils make
-RUN apt-add-repository -y ppa:hets/hets
-RUN apt-get update
-RUN apt-get install -y openjdk-8-jdk-headless ant cabal-install\
- ksh perl-base tar xz-utils zip\
- libmysqlclient-dev\
- ghc-haddock libghc-missingh-dev\
- ghc>=7.10.3 happy\
- libghc-mutable-containers-dev\
- libghc-haxml-dev libghc-tar-dev libghc-random-dev libghc-parsec3-dev\
- libghc-fgl-dev libghc-xml-dev\
- libghc-http-dev libghc-warp-dev libghc-wai-extra-dev\
- libghc-split-dev libghc-file-embed-dev libghc-monad-logger-dev\
- libghc-yaml-dev libghc-esqueleto-dev>=2.5.3\
- libghc-persistent-dev>=2.7.0 libghc-persistent-template-dev>=2.5.2\
- libghc-persistent-postgresql-dev>=2.6.1\
- libghc-persistent-sqlite-dev>=2.6.2\
- libghc-utf8-string-dev libghc-relation-dev\
- libghc-persistent-mysql-dev\
- libghc-hexpat-dev\
- libghc-aterm-dev\
- libghc-xeno-dev\
- libghc-heap-dev
-
-
-# RUN git clone https://github.com/spechub/Hets.git /hets
-## OR
-COPY ./ /hets
-
-WORKDIR /hets
+RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone && \
+   apt-get update && apt-get -y install locales && locale-gen en_US.UTF-8 && \
+   apt-get install -y software-properties-common apt-utils make && \
+# Install build and runtime dependencies
+   apt-add-repository -y ppa:hets/hets && \
+   apt-get update && \
+   apt-get install -y openjdk-8-jdk-headless ant cabal-install\
+      ksh perl-base tar xz-utils zip\
+      libmysqlclient-dev\
+      ghc-haddock libghc-missingh-dev\
+      ghc>=7.10.3 happy haskell-stack\
+      libghc-mutable-containers-dev\
+      libghc-haxml-dev libghc-tar-dev libghc-random-dev libghc-parsec3-dev\
+      libghc-fgl-dev libghc-xml-dev\
+      libghc-http-dev libghc-warp-dev libghc-wai-extra-dev\
+      libghc-split-dev libghc-file-embed-dev libghc-monad-logger-dev\
+      libghc-yaml-dev libghc-esqueleto-dev>=2.5.3\
+      libghc-persistent-dev>=2.7.0 libghc-persistent-template-dev>=2.5.2\
+      libghc-persistent-postgresql-dev>=2.6.1\
+      libghc-persistent-sqlite-dev>=2.6.2\
+      libghc-utf8-string-dev libghc-relation-dev\
+      libghc-persistent-mysql-dev\
+      libghc-hexpat-dev\
+      libghc-aterm-dev\
+      libghc-xeno-dev\
+      libghc-heap-dev
 
-RUN make derived
 
+FROM base as build-lib
+
+RUN apt-get -y install git
+# Get source
+# RUN git clone --branch 2109_python_gui https://github.com/spechub/Hets.git /opt/hets
+## Alternatively copy local files.
+COPY ./ /opt/hets
+WORKDIR /opt/hets/
+# Build and install haskell library
+RUN make derived
 RUN runhaskell Setup.hs configure \
-   --ghc --prefix=/ \
-   --disable-executable-stripping \
-   --disable-benchmarks \
-   --libdir=/lib/haskell-packages/ghc/lib/x86_64-linux-ghc-8.6.5 \
-   --libsubdir=hets-api-0.100.0 \
-   --datadir=share \
-   --datasubdir=hets-api \
-   --haddockdir=/lib/ghc-doc/haddock/hets-api-0.100.0 \
-   --docdir=share/doc/hets-api-doc \
-   --package-db=/var/lib/ghc/package.conf.d \
-   --disable-profiling \
-   lib:Hets
+      --ghc --prefix=/ \
+      --disable-executable-stripping \
+      --disable-benchmarks \
+      --libdir=/lib/haskell-packages/ghc/lib/x86_64-linux-ghc-8.6.5 \
+      --dynlibdir=/lib/haskell-packages/ghc/lib/x86_64-linux-ghc-8.6.5 \
+      --libsubdir=hets-api-0.100.0 \
+      --datadir=share \
+      --datasubdir=hets-api \
+      --haddockdir=/lib/ghc-doc/haddock/hets-api-0.100.0 \
+      --docdir=share/doc/hets-api-doc \
+      --package-db=/var/lib/ghc/package.conf.d \
+      --disable-profiling \
+      lib:Hets
 RUN runhaskell Setup.hs build -j$(nproc) lib:Hets
+RUN runhaskell Setup.hs copy --destdir=/tmp/hets-pkg
+RUN runhaskell Setup.hs register --gen-script
+RUN mv register.sh /tmp/install-hets.sh
+RUN tar -czf /tmp/hets.tar.gz -C /tmp/hets-pkg/ .
+
+FROM build-lib AS debug
+WORKDIR /opt/hets
 RUN runhaskell Setup.hs install
+RUN \
+   apt-get update && \
+   apt-get install -y cvc-47 darwin eprover fact++ maude minisat pellet spass vampire yices z3 zchaff && \
+   git clone https://github.com/spechub/Hets-lib.git ${HETS_LIB}
+
+ENV PYTHONPATH=/opt/hets/python/api/src
+
+
+FROM base
+COPY --from=build-lib /tmp/hets.tar.gz /tmp/hets.tar.gz
+COPY --from=build-lib /tmp/install-hets.sh /tmp/install-hets.sh
+# RUN tar -tzf /tmp/hets.tar.gz && ls -l /bin /bin/sh && false
+RUN tar -xzkpom -C / -f /tmp/hets.tar.gz
+RUN /tmp/install-hets.sh
+
+# Install provers and Hets-lib
+RUN \
+   apt-get update && \
+   apt-get install -y cvc-47 darwin eprover fact++ maude minisat pellet spass vampire yices z3 zchaff && \
+   git clone https://github.com/spechub/Hets-lib.git ${HETS_LIB}
+# Install python library
+
+COPY --from=build-lib /opt/hets/python/api /opt/hets/python/api
+RUN   python3 -m pip install /opt/hets/python/api
+# Add non-root user and cleanup
+RUN \
+   useradd -ms /bin/bash -u 921 hets && \
+   rm -rf /opt/hets
+
+WORKDIR /home/hets
+
+USER hets
diff --git a/Docker/hetsgui.Dockerfile b/Docker/hetsgui.Dockerfile
@@ -0,0 +1,31 @@
+FROM spechub2/hets-api as base
+
+USER root
+
+COPY python/gui /opt/hetsgui
+
+RUN apt-get update && apt-get upgrade -y && \
+        apt-get install -y libgtk-3-dev python3-gi python3-gi-cairo \
+            gir1.2-gtk-3.0 python3-pip graphviz \
+            libcanberra-gtk-module libcanberra-gtk3-module
+
+FROM base as debug
+
+ENV PYTHONPATH=${PYTHONPATH}:/opt/hetsgui/src
+
+RUN python3 -m pip install xdot numpy graphviz
+
+WORKDIR /root
+
+FROM base
+
+RUN cd /opt/hetsgui/src/hetsgui && \
+    glib-compile-resources hetsgui.gresource.xml && \
+    python3 -m pip install /opt/hetsgui && \
+    rm -rf /opt/hetsgui
+
+WORKDIR /home/hets
+
+USER hets
+
+ENTRYPOINT /usr/local/bin/hets
diff --git a/Docker/hyphen.Dockerfile b/Docker/hyphen.Dockerfile
@@ -1,5 +1,5 @@
 
-FROM ubuntu:20.04
+FROM ubuntu:22.04
 
 RUN apt-get update && \
     apt-get upgrade -y && \
@@ -22,5 +22,7 @@ packages = [ "hyphen" ]\n\
 [tool.setuptools.package-data]\n\
 "*" = [ "hslowlevel.*" ]\n' > /hyphen/pyproject.toml
 
-RUN pip3 install /hyphen
+RUN python3 -m pip install --upgrade pip setuptools
+
+RUN python3 -m pip install /hyphen
 
diff --git a/Hets.cabal b/Hets.cabal
@@ -694,6 +694,7 @@ Library
         HasCASL.TypeRel
         HasCASL.Unify
         HasCASL.VarDecl
+        HetsAPI.Refinement
         HolLight.ATC_HolLight
         HolLight.Helper
         HolLight.HolLight2DG

diff --git a/HetsAPI/Commands.hs b/HetsAPI/Commands.hs
@@ -34,7 +34,7 @@ module HetsAPI.Commands (
    , HPC.getUsableConsistencyCheckers
    , HPC.proveNode
    , HPC.checkConsistency
-   , HPC.checkConservativityNode 
+   , HPC.checkConservativityEdge
 
    -- Hets.InfoCommands
    , HIC.getGraphForLibrary

diff --git a/HetsAPI/DataTypes.hs b/HetsAPI/DataTypes.hs
@@ -5,26 +5,40 @@ License     :  GPLv2 or higher, see LICENSE.txt
 -}
 module HetsAPI.DataTypes (
     Sentence
-  , SentenceByName
+  , TheorySentence
+  , TheorySentenceByName
   , SignatureJSON
   , SymbolJSON
   , GenericTransportType
-  , TheoryPointer) where
-import qualified Common.OrderedMap as OMap
+  , TheoryPointer
+  , LinkPointer) where
+
 import Data.ByteString.Lazy(ByteString)
+import Data.Graph.Inductive.Graph (LNode, LEdge)
 
+import Common.AS_Annotation(SenAttr(..))
 import Common.LibName (LibName)
-import Static.DevGraph (LibEnv, DGraph, DGNodeLab)
+import qualified Common.OrderedMap as OMap
+
+import Logic.Comorphism (AnyComorphism(..))
+import Logic.Prover(ThmStatus(..))
+
+import Static.DevGraph (LibEnv, DGraph, DGNodeLab, DGLinkLab)
+import Static.GTheory (BasicProof(..))
+
 
-import Data.Graph.Inductive.Graph (LNode)
 
 -- | In the API if it is not possible to export the generic type, they are converted to JSON.
 type GenericTransportType = ByteString
 
+
 type Sentence = GenericTransportType
-type SentenceByName = OMap.OMap String Sentence
+
+type TheorySentence = SenAttr Sentence (ThmStatus (AnyComorphism, BasicProof))
+type TheorySentenceByName = OMap.OMap String TheorySentence
 
 type SignatureJSON = GenericTransportType
 type SymbolJSON = GenericTransportType
 
 type TheoryPointer = (LibName, LibEnv, DGraph, LNode DGNodeLab)
+type LinkPointer = (LibName, LibEnv, LEdge DGLinkLab)