2109 python gui

.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/**

.github/workflows/ci.yml

@@ -245,7 +245,7 @@ jobs:
       # ~ 496 MiB, 20 s
       - name: Upload cached stack
         if: env.DEBUG == 'true'
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: stack0
           path: ${{ runner.temp }}/stack0.tzst
@@ -254,7 +254,7 @@ jobs:
       # ~ 9 MiB
       - name: Upload Hets source dir
         if: env.DEBUG == 'true'
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: hets0
           path: ${{ runner.temp }}/hets0.tzst
@@ -302,7 +302,7 @@ jobs:
       - name: Upload Binary
         continue-on-error: true
         #if: github.event_name == 'push'
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: hets server binary
           path: hets-server.xz
@@ -311,7 +311,7 @@ jobs:
       # ~ 125 MiB , 15s
       - name: Upload Hets build dir
         if: github.event_name == 'pull_request'
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: hets-server
           path: ${{ runner.temp }}/${{ env.HETS_ARC }}
@@ -326,7 +326,7 @@ jobs:
       # ~ 496 MiB, 20 s
       - name: Upload post build stack
         if: env.DEBUG == 'true'
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: stack1
           path: ${{ runner.temp }}/stack1.tzst
@@ -405,7 +405,7 @@ jobs:
       - name: Upload Binary
         continue-on-error: true
         #if: github.event_name == 'push'
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: hets desktop binary
           path: hets.xz
@@ -414,7 +414,7 @@ jobs:
       # ~ 17 s
       - name: Upload Hets build dir
         if: github.event_name == 'pull_request'
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: hets-desktop
           path: ${{ runner.temp }}/${{ env.HETS_ARC }}
@@ -459,7 +459,7 @@ jobs:
         uses: actions/checkout@v2
 
       - name: Download Hets build dir
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: hets-server
           path: ${{ runner.temp }}
@@ -501,7 +501,7 @@ jobs:
     needs: job_2a
     steps:
       - name: Download Hets build dir
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: hets-server
           path: ${{ runner.temp }}
@@ -539,7 +539,7 @@ jobs:
     needs: job_2a
     steps:
       - name: Download Hets build dir
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: hets-server
           path: ${{ runner.temp }}
@@ -575,7 +575,7 @@ jobs:
     needs: job_2a
     steps:
       - name: Download Hets build dir
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: hets-server
           path: ${{ runner.temp }}
@@ -683,7 +683,7 @@ jobs:
         if: startsWith(env.FAKE_URL, 'http')
           && steps.download.outcome == 'failure'
         continue-on-error: true
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: docs
           path: ${{ runner.temp }}/docs.tgz

.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

.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

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
 

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

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

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 LANG en_US.UTF-8
-ENV LANGUAGE en_US:en
-ENV LC_ALL en_US.UTF-8
-
-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
+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 make derived
+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
+
+
+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