Merge branch 'main' into permutation-minimal

conjure-cp · Jun 26, 2024 · 022185b · 022185b
2 parents ca742f6 + 843ec48
commit 022185b
Show file tree

Hide file tree

Showing 208 changed files with 2,715 additions and 482 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -38,14 +38,14 @@ jobs:
 
     steps:
 
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         name: Checkout repository
 
       - name: Stack version
         shell: bash
         run: GHC_VERSION=${{ matrix.GHC_VERSION }} make stack.yaml
 
-      - uses: actions/cache@v3
+      - uses: actions/cache@v4
         name: Cache stack
         with:
           path: |

diff --git a/.github/workflows/docker-publish.yml → .github/workflows/publish-ghcr.yml b/.github/workflows/docker-publish.yml → .github/workflows/publish-ghcr.yml
@@ -1,4 +1,4 @@
-name: Publishing Docker image to ghcr.io
+name: Publishing container on ghcr.io
 
 # This workflow uses actions that are not certified by GitHub.
 # They are provided by a third-party and are governed by
@@ -20,7 +20,7 @@ on:
   pull_request:             # and for PRs that edit the docker files
     paths:
       - Dockerfile
-      - .github/workflows/docker-publish.yml
+      - .github/workflows/publish-ghcr.yml
                             # other branches that want testing must create a PR
 
 
@@ -50,16 +50,16 @@ jobs:
     steps:
 
       - name: Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       # Set up buildx (Docker CLI plugin for extended build capabilities with BuildKit)
       - name: Setup Docker buildx
-        uses: docker/setup-buildx-action@v2
+        uses: docker/setup-buildx-action@v3
 
       # Login against a Docker registry except on PR
       - name: Log into registry
         if: github.event_name != 'pull_request'
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
@@ -68,14 +68,18 @@ jobs:
       # Extract metadata (tags, labels) for Docker
       - name: Extract Docker metadata
         id: meta
-        uses: docker/metadata-action@v4
+        uses: docker/metadata-action@v5
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
 
+      - name: Extract git version
+        shell: bash
+        run: bash etc/build/version.sh
+
       # Build and push Docker image with Buildx (don't push on PR)
       - name: Build and push Docker image
         id: build-and-push
-        uses: docker/build-push-action@v3
+        uses: docker/build-push-action@v5
         with:
           context: .
           push: ${{ github.event_name != 'pull_request' }} # do not push if this was triggered by a PR

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -40,14 +40,14 @@ jobs:
 
     steps:
 
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         name: Checkout repository
 
       - name: Stack version
         shell: bash
         run: GHC_VERSION=${{ matrix.GHC_VERSION }} make stack.yaml
 
-      - uses: actions/cache@v3
+      - uses: actions/cache@v4
         name: Cache stack
         with:
           path: |
@@ -72,14 +72,17 @@ jobs:
         run: |
           echo "${HOME}/solver-binaries" >> ${GITHUB_PATH}
 
-      - name: Installing dependencies (gperf) on Linux
+      # libnuma-dev for runsolver
+      # autoconf, cmake, gmp for yices
+
+      - name: Installing dependencies on Linux
         shell: bash
-        run: sudo apt-get install -y gperf
+        run: sudo apt-get install -y gperf libnuma-dev
         if: runner.os == 'Linux'
 
-      - name: Installing dependencies (gperf) on macOS
+      - name: Installing dependencies on macOS
         shell: bash
-        run: brew install gperf
+        run: brew install autoconf cmake gmp gperf
         if: runner.os == 'macOS'
 
       - name: Build solvers

diff --git a/.github/workflows/solvers.yml b/.github/workflows/solvers.yml
@@ -10,12 +10,12 @@ on:
     branches:
       - main                # run for the main branch
     paths:
-      - etc/build/install*.sh
+      - etc/build/*.sh
       - Makefile
       - .github/workflows/solvers.yml
   pull_request:             # and for PRs
     paths:
-      - etc/build/install*.sh
+      - etc/build/*.sh
       - Makefile
       - .github/workflows/solvers.yml
                             # other branches that want testing must create a PR
@@ -36,7 +36,7 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         name: Checkout repository
 
       - name: Run sccache-cache
@@ -47,14 +47,17 @@ jobs:
         run: |
           echo "${HOME}/.local/bin" >> ${GITHUB_PATH}
 
-      - name: Installing dependencies (gperf) on Linux
+      # libnuma-dev for runsolver
+      # autoconf, cmake, gmp for yices
+
+      - name: Installing dependencies on Linux
         shell: bash
-        run: sudo apt-get install -y gperf
+        run: sudo apt-get install -y gperf libnuma-dev
         if: runner.os == 'Linux'
 
-      - name: Installing dependencies (gperf) on macOS
+      - name: Installing dependencies on macOS
         shell: bash
-        run: brew install gperf
+        run: brew install autoconf cmake gmp gperf
         if: runner.os == 'macOS'
 
       - name: Building solvers

diff --git a/.github/workflows/test-coverage.yml b/.github/workflows/test-coverage.yml
@@ -29,14 +29,14 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         name: Checkout repository
 
       - name: Stack version
         shell: bash
         run: make stack.yaml
 
-      - uses: actions/cache@v3
+      - uses: actions/cache@v4
         name: Cache stack
         with:
           path: |

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -8,7 +8,7 @@ on:
     paths:
       - conjure-cp.cabal
       - Makefile
-      - Dockerfile          # this is here because the docker-publish.yml depends on successful completion of this action
+      - Dockerfile          # this is here because publish-ghcr.yml depends on successful completion of this action
       - src/**
       - tests/**
       - etc/build/**
@@ -42,14 +42,14 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         name: Checkout repository
 
       - name: Stack version
         shell: bash
         run: make stack.yaml
 
-      - uses: actions/cache@v3
+      - uses: actions/cache@v4
         name: Cache stack
         with:
           path: |

diff --git a/Dockerfile b/Dockerfile
@@ -9,13 +9,13 @@
 # Setting up
 FROM ubuntu:23.10 AS builder
 ENV DEBIAN_FRONTEND noninteractive
-WORKDIR /conjure/
+WORKDIR /conjure
 
 # All binaries will end up in /root/.local/bin
 RUN mkdir -p /root/.local/bin
 ENV PATH /root/.local/bin:$PATH
 ENV LD_LIBRARY_PATH /root/.local/bin/lib:$LD_LIBRARY_PATH
-ENV MZN_STDLIB_DIR /root/.local/bin/share/minizinc/
+ENV MZN_STDLIB_DIR /root/.local/bin/share/minizinc
 # Dependencies
 RUN apt-get update
 RUN apt-get install -y --no-install-recommends build-essential          # so we can compile stuff
@@ -30,6 +30,7 @@ RUN apt-get install -y --no-install-recommends autoconf                 # needed
 RUN apt-get install -y --no-install-recommends gperf                    # needed when building some solvers (for example yices)
 RUN apt-get install -y --no-install-recommends python3                  # needed when building some solvers (for example z3)
 RUN apt-get install -y --no-install-recommends default-jre-headless     # savilerow
+RUN apt-get install -y --no-install-recommends libnuma-dev              # runsolver
 
 # Only copying the install*.sh scripts
 RUN mkdir -p etc
@@ -51,17 +52,28 @@ RUN PROCESSES=2 etc/build/install-open-wbo.sh
 RUN PROCESSES=2 etc/build/install-ortools.sh
 RUN PROCESSES=2 etc/build/install-yices.sh
 RUN PROCESSES=2 etc/build/install-z3.sh
+RUN PROCESSES=2 etc/build/install-runsolver.sh
 
-# Copy everything
-COPY . .
+# An attempt to cache more
+COPY Makefile Makefile
+COPY etc/hs-deps etc/hs-deps
+COPY conjure-cp.cabal conjure-cp.cabal
+RUN make installdeps
 
-# Building Conjure and copying Savile Row
+# Copy the rest
+COPY etc etc
+COPY src src
+COPY LICENSE LICENSE
 RUN make install
 
 # List the binaries
 RUN ls -l /root/.local/bin
 RUN du -sh /root/.local/bin
 
+# Copy the allsolvers test case
+RUN mkdir -p tests
+COPY tests/allsolvers tests/allsolvers
+
 # a test to see if all solvers work as expected
 RUN tests/allsolvers/test.sh
 
@@ -73,8 +85,9 @@ FROM ubuntu:23.10
 WORKDIR /conjure
 ENV PATH /root/.local/bin:$PATH
 ENV LD_LIBRARY_PATH /root/.local/bin/lib:$LD_LIBRARY_PATH
-ENV MZN_STDLIB_DIR /root/.local/bin/share/minizinc/
-RUN apt-get update
-RUN apt-get install -y --no-install-recommends default-jre-headless     # savilerow
+ENV MZN_STDLIB_DIR /root/.local/bin/share/minizinc
+RUN apt-get update && apt-get install -y --no-install-recommends build-essential          # so we can compile stuff
+RUN apt-get update && apt-get install -y --no-install-recommends default-jre-headless     # savilerow
+RUN apt-get update && apt-get install -y --no-install-recommends libnuma-dev              # runsolver
 RUN mkdir -p /root/.local/bin/lib
 COPY --from=builder /root/.local/bin /root/.local/bin
diff --git a/LICENSE b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2009-2023 Özgür Akgün
+Copyright 2009-2024 Özgür Akgün
     School of Computer Science, University of St Andrews
 
 All rights reserved.

diff --git a/Makefile b/Makefile
@@ -53,6 +53,14 @@ install:
 	@echo
 	@echo
 
+# mainly for CI
+.PHONY: installdeps
+installdeps:
+	bash etc/build/install-stack.sh
+	make stack.yaml
+	stack --local-bin-path ${BIN_DIR} setup;
+	stack build --only-dependencies
+
 .PHONY: test
 test:
 	@if ${COVERAGE}; then \
@@ -150,4 +158,5 @@ solvers:
 	@etc/build/silent-wrapper.sh etc/build/install-minizinc.sh
 	@etc/build/silent-wrapper.sh etc/build/install-yices.sh
 	@etc/build/silent-wrapper.sh etc/build/install-z3.sh
+	@etc/build/silent-wrapper.sh etc/build/install-runsolver.sh
 	@if ls make-solvers-*.stderr make-solvers-*.stdout > /dev/null 2> /dev/null; then echo "At least one solver didn't build successfully."; exit 1; fi
diff --git a/conjure-cp.cabal b/conjure-cp.cabal
@@ -259,6 +259,7 @@ Library
                      , Conjure.UI.ParameterGenerator
                      , Conjure.UI.NormaliseQuantified
                      , Conjure.UI.ErrorDisplay
+                     , Conjure.UI.SolveStats
 
                      , Conjure.LSP.LanguageServer
                      , Conjure.LSP.Documentation
@@ -329,6 +330,7 @@ Library
                      , template-haskell
                      , http-client
                      , http-client-tls
+                     , hostname
 
     default-extensions:
         FlexibleContexts

diff --git a/docs/conjure-help.html b/docs/conjure-help.html
@@ -136,6 +136,10 @@
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--seed=INT</td><td style='padding-left:2ex;'>Random number generator seed.</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--limit-models=INT</td><td style='padding-left:2ex;'>Maximum number of models to generate.</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--use-existing-models=FILE</td><td style='padding-left:2ex;'>File names of Essence' models generated beforehand.<br />If given, Conjure skips the modelling phase and uses the existing models for solving.<br />The models should be inside the output directory (See -o).</td></tr>
+<tr><td colspan='3'>runsolver:</td></tr>
+<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--runsolver-cpu-time-limit=INT</td><td style='padding-left:2ex;'>Use runsolver to limit total CPU time (in seconds)</td></tr>
+<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--runsolver-wall-time-limit=INT</td><td style='padding-left:2ex;'>Use runsolver to limit total elapsed time (in seconds)</td></tr>
+<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--runsolver-memory-limit=INT</td><td style='padding-left:2ex;'>Use runsolver to limit total memory usage (Maximum RSS - in megabytes).</td></tr>
 <tr><td colspan='3'>Options for other tools:</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--savilerow-options=ITEM</td><td style='padding-left:2ex;'>Options passed to Savile Row.</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--solver-options=ITEM</td><td style='padding-left:2ex;'>Options passed to the backend solver.</td></tr>

diff --git a/docs/conjure-help.txt b/docs/conjure-help.txt
@@ -269,6 +269,10 @@
                                               If given, Conjure skips the modelling phase and uses the existing models
                                               for solving.
                                               The models should be inside the output directory (See -o).
+ runsolver:
+      --runsolver-cpu-time-limit=INT          Use runsolver to limit total CPU time (in seconds)
+      --runsolver-wall-time-limit=INT         Use runsolver to limit total elapsed time (in seconds)
+      --runsolver-memory-limit=INT            Use runsolver to limit total memory usage (Maximum RSS - in megabytes).
  Options for other tools:
       --savilerow-options=ITEM                Options passed to Savile Row.
       --solver-options=ITEM                   Options passed to the backend solver.