Materialize Nix expressions

.github/workflows/release.yml

@@ -0,0 +1,57 @@
+name: "Release"
+on:
+  push:
+    branches:
+      - master
+jobs:
+  check:
+    name: 'Check'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out code
+        uses: actions/[email protected]
+        with:
+          submodules: recursive
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v12
+        with:
+          extra_nix_config: |
+            substituters = http://cache.nixos.org https://hydra.iohk.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+
+      - name: Install Cachix
+        uses: cachix/cachix-action@v8
+        with:
+          name: runtimeverification
+          extraPullNames: 'kore'
+          skipPush: true
+
+      - name: Check materialization
+        run: nix-build --arg checkMaterialization true -A project.stack-nix
+
+  release:
+    name: 'Release'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out code
+        uses: actions/[email protected]
+        with:
+          submodules: recursive
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v12
+        with:
+          extra_nix_config: |
+            substituters = http://cache.nixos.org https://hydra.iohk.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+
+      - name: Install Cachix
+        uses: cachix/cachix-action@v8
+        with:
+          name: runtimeverification
+          signingKey: '${{ secrets.RUNTIMEVERIFICATION_CACHIX_SIGNING_KEY }}'
+          extraPullNames: 'kore'
+
+      - name: Build
+        run: nix-build -A kore -A project.kore.checks

.github/workflows/test.yml

@@ -1,43 +1,116 @@
 name: "Test"
 on:
   pull_request:
-  push:
 jobs:
-  test-nix:
+  nix:
+    name: 'Nix'
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/[email protected]
-      with:
-        submodules: recursive
-    - uses: cachix/install-nix-action@v12
-    - uses: cachix/cachix-action@v8
-      with:
-        name: runtimeverification
-        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
-    - run: nix-build -A kore -A project.kore.checks
-    - run: nix-shell --run "echo OK"
-
-  test-cabal:
+      - name: Check out code
+        uses: actions/[email protected]
+        with:
+          submodules: recursive
+          # Avoid cloning a detached-HEAD repository on pull_request events.
+          # git-auto-commit-action (below) needs this to find the original
+          # branch where it should push the changes.
+          ref: ${{ github.head_ref }}
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v12
+        with:
+          extra_nix_config: |
+            substituters = http://cache.nixos.org https://hydra.iohk.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+
+      - name: Install Cachix
+        uses: cachix/cachix-action@v8
+        with:
+          name: kore
+          signingKey: '${{ secrets.KORE_CACHIX_SIGNING_KEY }}'
+
+      - name: Materialize
+        run: ./nix/rematerialize.sh
+
+      - name: Commit changes
+        uses: stefanzweifel/[email protected]
+        with:
+          commit_message: 'Materialize Nix expressions'
+          file_pattern: 'nix/'
+
+      - name: Build
+        run: nix-build -A kore
+
+      - name: Run unit tests
+        run: nix-build -A project.kore.checks
+
+      - name: Check shell
+        run: nix-shell --run "echo OK"
+
+  cabal:
+    name: 'Cabal'
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/[email protected]
-      with:
-        submodules: recursive
-
-    - uses: actions/[email protected]
-      id: setup-haskell-cabal
-      with:
-        ghc-version: "8.10.1"
-        cabal-version: "3.2"
-
-    - name: Cache Cabal store
-      uses: actions/cache@v2
-      with:
-        path: ${{ steps.setup-haskell-cabal.outputs.cabal-store }}
-        key: ${{ runner.os }}-ghc-8.10.1-${{ hashFiles('cabal.project.freeze') }}
-
-    - name: Build project
-      run: cabal v2-build --enable-tests --enable-benchmarks all
-
-    - name: Configure with profiling
-      run: cabal v2-configure --enable-profiling -f-threaded
+      - name: Install prerequisites
+        run: |
+          sudo apt install --yes z3
+
+      - uses: actions/[email protected]
+        with:
+          submodules: recursive
+
+      - uses: actions/[email protected]
+        id: setup-haskell-cabal
+        with:
+          ghc-version: "8.10.1"
+          cabal-version: "3.2"
+
+      - name: Cache Cabal store
+        uses: actions/cache@v2
+        with:
+          path: ${{ steps.setup-haskell-cabal.outputs.cabal-store }}
+          key: ${{ runner.os }}-ghc-8.10.1-${{ hashFiles('cabal.project.freeze') }}
+
+      - name: Build
+        run: cabal v2-build --enable-tests --enable-benchmarks all
+
+      - name: Run unit tests
+        run: cabal v2-test --test-show-details=direct all
+
+      - name: Configure with profiling
+        run: cabal v2-configure --enable-profiling -f-threaded
+
+  stack:
+    name: 'Stack'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Install prerequisites
+        run: |
+          sudo apt install --yes z3
+
+      - uses: actions/[email protected]
+        with:
+          submodules: recursive
+
+      - uses: actions/[email protected]
+        id: setup-haskell-stack
+        with:
+          enable-stack: true
+          stack-no-global: true
+          stack-setup-ghc: true
+
+      - name: Locate Stack root
+        id: locate-stack-root
+        run: |
+          echo "::set-output name=stack-root::$(stack path --stack-root)"
+
+      - name: Cache Stack root
+        uses: actions/cache@v2
+        with:
+          path: ${{ steps.locate-stack-root.outputs.stack-root }}
+          key: ${{ runner.os }}-ghc-8.10.1-${{ hashFiles('stack.yaml.lock') }}
+
+      - name: Build project
+        run: stack build --pedantic
+
+      - name: Run unit tests
+        run: stack test --pedantic

.gitignore

@@ -1,7 +1,6 @@
 /.build/*
 /evm-semantics
 
-*.cache
 *.class
 *.iml
 *.ipr

README.md

@@ -44,23 +44,27 @@ If using `cabal`, version 3.0 or later is recommended.
 
 ## Developing
 
-Developers will require all the dependencies listed above.
-We also recommend (but not require!) the following dependencies.
+Developers will require all the dependencies listed above,
+in addition to the requirements and recommendations below.
+
+### Required dependencies
+
+For integration testing, we require:
+
+- GNU [make]
+- The [K Framework] frontend, or [curl] to fetch an appropriate version.
+  The frontend has other dependencies, most notably a Java runtime.
+
+### Recommended dependencies
 
 For setting up a development environment, we recommend:
 
 - [direnv] to make the project's tools available in shells and editors.
-- [ghcide] or [haskell-ide-engine], [language servers] for Haskell that are
+- [ghcide] or [haskell-language-server], [language servers] for Haskell that are
   compatible with most editors. See instructions
   [below](#running-a-language-server) to run a language server.
 - [hlint] and [stylish-haskell] for compliance with project guidelines.
 
-For integration testing, we also recommend:
-
-- GNU [make]
-- The [K Framework] frontend, or [curl] to fetch an appropriate version.
-  The frontend has other dependencies, most notably a Java runtime.
-
 ### Running a language server
 
 To run a language server, developers will need to activate the appropriate
@@ -85,9 +89,18 @@ cabal build --enable-tests --enable-benchmarks --only-dependencies kore
 
 ### Developing with Nix
 
-For developers so inclined, we provide a `shell.nix` expression with a suitable
-development environment and a binary cache at [kore.cachix.org]. The development
-environment is intended to be used with `nix-shell` and `cabal`.
+We provide a `shell.nix` expression with a suitable development environment and
+a binary cache at [kore.cachix.org]. The development environment is intended to
+be used with `nix-shell` and `cabal`.
+
+When the `.cabal` package description file changes, run:
+
+```.sh
+# Requires Nix to be installed.
+./nix/rematerialize.sh
+```
+
+This script is also run by an automatic workflow.
 
 
 [git]: https://git-scm.com/
@@ -98,8 +111,9 @@ environment is intended to be used with `nix-shell` and `cabal`.
 [make]: https://www.gnu.org/software/make/
 [direnv]: https://github.com/direnv/direnv
 [ghcide]: https://github.com/digital-asset/ghcide
-[haskell-ide-engine]: https://github.com/haskell/haskell-ide-engine
+[haskell-language-server]: https://github.com/haskell/haskell-language-server
 [language servers]: https://langserver.org/
 [hlint]: https://github.com/ndmitchell/hlint
 [stylish-haskell]: https://github.com/jaspervdj/stylish-haskell
 [kore.cachix.org]: https://kore.cachix.org/
+[Nix]: https://nixos.org

default.nix

@@ -1,6 +1,7 @@
 { profiling ? false
 , release ? false
 , threaded ? !profiling
+, checkMaterialization ? false
 }:
 
 let
@@ -14,38 +15,34 @@ let
     in import haskell-nix.sources.nixpkgs-2003 args;
   inherit (pkgs) lib;
 
-  local =
-    if builtins.pathExists ./local.nix
-    then import ./local.nix { inherit default; }
-    else x: x;
-
-  project =
-    (args: pkgs.haskell-nix.stackProject (local args)) {
-      src = pkgs.haskell-nix.haskellLib.cleanGit { name = "kore"; src = ./.; };
-      modules = [
-        {
-          # package *
-          enableLibraryProfiling = true;
-          profilingDetail = "none";
-          # package kore
-          packages.kore = {
-            flags = {
-              inherit release threaded;
-            };
-            enableLibraryProfiling = profiling;
-            enableExecutableProfiling = profiling;
-            profilingDetail = "toplevel-functions";
-
-            # Add Z3 to PATH for unit tests.
-            components.tests.kore-test.preCheck = ''
-              export PATH="$PATH''${PATH:+:}${lib.getBin pkgs.z3}/bin"
-            '';
+  project = pkgs.haskell-nix.stackProject {
+    src = pkgs.haskell-nix.haskellLib.cleanGit { name = "kore"; src = ./.; };
+    inherit checkMaterialization;
+    materialized = ./nix/kore.nix.d;
+    modules = [
+      {
+        # package *
+        enableLibraryProfiling = true;
+        profilingDetail = "none";
+        # package kore
+        packages.kore = {
+          flags = {
+            inherit release threaded;
           };
-        }
-      ];
-    };
-
-  shell = import ./shell.nix { inherit default; };
+          enableLibraryProfiling = profiling;
+          enableExecutableProfiling = profiling;
+          profilingDetail = "toplevel-functions";
+
+          # Add Z3 to PATH for unit tests.
+          components.tests.kore-test.preCheck = ''
+            export PATH="$PATH''${PATH:+:}${lib.getBin pkgs.z3}/bin"
+          '';
+        };
+      }
+    ];
+  };
+
+  shell = import ./shell.nix { inherit default checkMaterialization; };
 
   version = project.kore.components.exes.kore-exec.version;
 

kore/kore.cabal

@@ -10,8 +10,8 @@ description:    Please see the [README](README.md) file.
 category:       Language
 homepage:       https://github.com/kframework/kore#readme
 bug-reports:    https://github.com/kframework/kore/issues
-author:         Virgil Serbanuta
-maintainer:     virgil.serbanuta@runtimeverification.com
+author:         Runtime Verification Inc
+maintainer:     thomas.tuegel@runtimeverification.com
 copyright:      2018-2020 Runtime Verification Inc
 license:        NCSA
 license-file:   LICENSE

kore/package.yaml

@@ -3,8 +3,8 @@ version:             0.35.0.0
 github:              "kframework/kore"
 license:             NCSA
 license-file:        LICENSE
-author:              "Virgil Serbanuta"
-maintainer:          "virgil.serbanuta@runtimeverification.com"
+author:              "Runtime Verification Inc"
+maintainer:          "thomas.tuegel@runtimeverification.com"
 copyright:           "2018-2020 Runtime Verification Inc"
 category:            Language