Build static kind2-mcil binaries

kind2-mc · Oct 20, 2023 · 0a9b7fa · 0a9b7fa
1 parent 8ed99f0
commit 0a9b7fa
Show file tree

Hide file tree

Showing 3 changed files with 70 additions and 26 deletions.
diff --git a/.github/workflows/kind2-mcil.yml b/.github/workflows/kind2-mcil.yml
@@ -8,42 +8,78 @@ on:
     branches: [ mcil ]
 
 jobs:
-  kind2-build:
+  kind2-linux-bin:
+    runs-on: ubuntu-latest
+    services:
+      registry:
+        image: registry:2
+        ports:
+          - 5000:5000
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v3
+
+    - name: Set up Docker Buildx
+      uses: docker/setup-buildx-action@v1
+      with:
+        driver-opts: network=host
+
+    - name: Build and push to local registry
+      uses: docker/build-push-action@v2
+      with:
+        file: docker/Dockerfile
+        context: ./
+        target: builder
+        push: true
+        tags: localhost:5000/name/kind2:latest
+
+    - name: Extract kind2-mcil binary
+      id: extract
+      uses: shrink/actions-docker-extract@v1
+      with:
+        image: localhost:5000/name/kind2:latest
+        path: /home/opam/kind2-build/bin/kind2-mcil
+
+    - name: Upload kind2-mcil binary
+      uses: actions/upload-artifact@v3
+      with:
+        path: ${{ steps.extract.outputs.destination }}
+        name: kind2-mcil-linux
+
+
+  kind2-macos-bin:
     strategy:
-      matrix:
-        ocaml-version: [ 4.09.1 ]
-        os: [ ubuntu-20.04, macos-11 ]
-        include:
-          - os: macos-11
-            pkg_update: brew update
-          - os: ubuntu-20.04
-            pkg_update: sudo apt-get update -y
+      matrix: # Single configuration
+        ocaml-version: [ 4.14.0 ]
+        # Only matrix variables can be used at runs-on
+        os: [ macos-11 ]
 
     runs-on: ${{ matrix.os }}
 
     steps:
     - name: Checkout code
       uses: actions/checkout@v3
 
-    #- name: Update package information
-    #  run: ${{ matrix.pkg_update }}
-
-    - name: Set up OCaml ${{ matrix.ocaml-version }}
+    - name: Set up OCaml ${{ matrix.ocaml-version }}+flambda
       uses: ocaml/setup-ocaml@v2
       with:
-        ocaml-compiler: ${{ matrix.ocaml-version }}
+        ocaml-compiler: ocaml-variants.${{ matrix.ocaml-version }}+options,ocaml-option-flambda
 
     - name: Pin MCIL version of Dolmen packages
       run: |
         opam pin -y add dolmen https://github.com/ModelChecker/dolmen.git#mcil
         opam pin -y add dolmen_type https://github.com/ModelChecker/dolmen.git#mcil
         opam pin -y add dolmen_loop https://github.com/ModelChecker/dolmen.git#mcil
 
-    - name: Install Kind2-MCIL OCaml dependencies
+    - name: Install Kind2 OCaml dependencies
       run: opam install -y . --deps-only
 
-    - name: Build all binaries
-      run: opam exec make
+    - name: Build Kind 2
+      run: opam exec make static
+
+    - name: Strip binary
+      run: strip bin/kind2-mcil
 
     - name: Upload kind2-mcil artifact
       uses: actions/upload-artifact@v3

diff --git a/doc/usr/source/home.rst b/doc/usr/source/home.rst
@@ -8,23 +8,28 @@ It requires a `modified version <https://github.com/ModelChecker/dolmen/tree/mci
 the `Dolmen <https://github.com/Gbury/dolmen>`_ library capable of reading MCIL files.
 Here are the installation instructions:
 
-1. Start by installing `OPAM 2.1 <https://opam.ocaml.org/>`_ or later
+Start by installing `OPAM 2.1 <https://opam.ocaml.org/>`_ or later
 following the instructions on the OPAM website, and
-make sure OPAM has been initialized by running ``opam init``.
+make sure OPAM has been initialized by running ``opam init --compiler=4.14.1``.
+
+Install OCaml 4.14.1 or below:
+
+.. code-block:: bash
+
+  opam switch create 4.14.1
 
-2. Then run the following shell commands:
+Then run the following shell commands:
 
 .. code-block:: bash
 
    opam pin -y add dolmen https://github.com/ModelChecker/dolmen.git#mcil
    opam pin -y add dolmen_type https://github.com/ModelChecker/dolmen.git#mcil
    opam pin -y add dolmen_loop https://github.com/ModelChecker/dolmen.git#mcil
    opam pin -y add kind2-mcil https://github.com/kind2-mc/kind2.git#mcil
-   opam install --update-invariant kind2-mcil
 
-3. Install one or more of the supported SMT solvers listed in the section Required Software below.
+Finally, install one or more of the supported SMT solvers listed in the section Required Software below.
 
-Now you should be able to run ``kind2-mcil`` as follows: `kind2-mcil <input>.mcil`
+Now you should be able to run ``kind2-mcil`` as follows: ``kind2-mcil <input>.mcil``
 
 Kind 2
 ======

diff --git a/docker/Dockerfile b/docker/Dockerfile
@@ -14,9 +14,12 @@ WORKDIR kind2-build
 
 # Note: we use remote OPAM repo until local one is updated
 RUN eval $(opam env) && \
-    opam repo set-url default https://opam.ocaml.org && \
-    opam update && opam install -y . --deps-only && \
-    make static && strip bin/kind2
+    opam repo set-url default https://opam.ocaml.org && opam update \
+    opam pin -y add dolmen https://github.com/ModelChecker/dolmen.git#mcil && \
+    opam pin -y add dolmen_type https://github.com/ModelChecker/dolmen.git#mcil && \
+    opam pin -y add dolmen_loop https://github.com/ModelChecker/dolmen.git#mcil && \
+    opam install -y . --deps-only && \
+    make static && strip bin/kind2*
 
 FROM alpine:latest