Merge branch 'master' into full-correctness

Author: F-WRunTime

.github/workflows/release.yml

@@ -13,13 +13,12 @@ jobs:
         with:
           submodules: recursive
 
-      - name: Install Nix
-        uses: cachix/install-nix-action@v14.1
+      - name: 'Install Nix'
+        uses: cachix/install-nix-action@v15
         with:
           extra_nix_config: |
-            substituters = http://cache.nixos.org https://hydra.iohk.io
+            substituters = http://cache.nixos.org https://cache.iog.io
             trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
-          install_url: "https://releases.nixos.org/nix/nix-2.3.16/install"
 
       - name: Install Cachix
         uses: cachix/cachix-action@v10
@@ -28,8 +27,19 @@ jobs:
           extraPullNames: 'kore'
           skipPush: true
 
+      - name: Materialize
+        run: nix run .#update-cabal
+
+      - name: Materialize GHC 9
+        run: nix run .#update-cabal-ghc9
+
       - name: Check materialization
-        run: nix-build --arg checkMaterialization true -A project.stack-nix
+        run: |
+          if [ -n "$(git status --porcelain 'nix/')" ]; then
+            echo 2>&1 "Error: found modified files"
+            git diff
+            exit 1
+          fi
 
   release:
     name: 'Release'

.github/workflows/test.yml

@@ -16,15 +16,14 @@ jobs:
           ref: ${{ github.event.pull_request.head.sha }}
           submodules: recursive
 
-      - name: Install Nix
-        uses: cachix/install-nix-action@v14.1
+      - name: 'Install Nix'
+        uses: cachix/install-nix-action@v15
         with:
           extra_nix_config: |
-            substituters = http://cache.nixos.org https://hydra.iohk.io
+            substituters = http://cache.nixos.org https://cache.iog.io
             trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
-          install_url: "https://releases.nixos.org/nix/nix-2.3.16/install"
 
-      - name: Install Cachix
+      - name: 'Install Cachix'
         uses: cachix/cachix-action@v10
         with:
           name: runtimeverification
@@ -33,66 +32,12 @@ jobs:
       - name: Build
         run: nix-build -A kore
 
-  nix-shell:
-    name: 'Nix / Shell'
-    strategy:
-      matrix:
-        os: [ubuntu-latest, macos-latest]
-    runs-on: ${{ matrix.os }}
-    steps:
-      - name: Check out code
-        uses: actions/[email protected]
-        with:
-          # Check out pull request HEAD instead of merge commit.
-          ref: ${{ github.event.pull_request.head.sha }}
-          submodules: recursive
-
-      - name: Install Nix
-        uses: cachix/[email protected]
-        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=
-          install_url: "https://releases.nixos.org/nix/nix-2.3.16/install"
-
-      - name: Install Cachix
-        uses: cachix/cachix-action@v10
-        with:
-          name: runtimeverification
-          signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+      - name: Build GHC9
+        run: GC_DONT_GC=1 nix build .#kore-exec-prof
 
       - name: Check shell
         run: nix-shell --run "echo OK"
 
-  nix-test:
-    name: 'Nix / Test'
-    needs: nix-build
-    strategy:
-      matrix:
-        os: [ubuntu-latest, macos-latest]
-    runs-on: ${{ matrix.os }}
-    steps:
-      - name: Check out code
-        uses: actions/[email protected]
-        with:
-          # Check out pull request HEAD instead of merge commit.
-          ref: ${{ github.event.pull_request.head.sha }}
-          submodules: recursive
-
-      - name: Install Nix
-        uses: cachix/[email protected]
-        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=
-          install_url: "https://releases.nixos.org/nix/nix-2.3.16/install"
-
-      - name: Install Cachix
-        uses: cachix/cachix-action@v10
-        with:
-          name: runtimeverification
-          signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
-
       - name: Run unit tests
         run: nix-build -A project.kore.checks
 
@@ -209,6 +154,8 @@ jobs:
   hlint:
     name: 'HLint'
     runs-on: ubuntu-latest
+    env:
+      hlint_version: "3.4.1"
     steps:
       - uses: actions/[email protected]
         with:
@@ -217,7 +164,7 @@ jobs:
           submodules: recursive
 
       - name: Run hlint
-        run: curl -sSL https://raw.github.com/ndmitchell/hlint/master/misc/run.sh | sh -s kore -j
+        run: curl -sSL https://raw.github.com/ndmitchell/hlint/v${{ env.hlint_version }}/misc/run.sh | sh -s kore -j
 
   performance:
     needs: [nix-build]
@@ -264,4 +211,9 @@ jobs:
           ./scripts/join-statistics.sh master.json pull-request.json \
             | ./scripts/format-statistics.sh \
             > comment.md
-          gh pr comment ${{ github.event.pull_request.number }} -F comment.md
+          if [[ $(sed -E -e '1,2d ; /.*\| (0|-?0.00[0-9]*) \| (0|-?0.00[0-9]*) \|$/d' comment.md | wc -l) -ne 0 ]]; then\
+            gh pr comment ${{ github.event.pull_request.number }} -F comment.md; \
+          else \
+            echo "Produced statistics are boring, just printing them right here:"; \
+            cat comment.md; \
+          fi

.github/workflows/update.yml

@@ -27,22 +27,26 @@ jobs:
           ref: ${{ steps.config.outputs.ref }}
           submodules: recursive
 
-      - name: Install Nix
-        uses: cachix/install-nix-action@v14.1
+      - name: 'Install Nix'
+        uses: cachix/install-nix-action@v15
         with:
           extra_nix_config: |
-            substituters = http://cache.nixos.org https://hydra.iohk.io
+            substituters = http://cache.nixos.org https://cache.iog.io
             trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
-          install_url: "https://releases.nixos.org/nix/nix-2.3.16/install"
 
-      - name: Install Cachix
+      - name: 'Install Cachix'
         uses: cachix/cachix-action@v10
         with:
           name: runtimeverification
+          extraPullNames: kore
           signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
 
+
       - name: Materialize
-        run: ./nix/rematerialize.sh
+        run: nix run .#update-cabal
+
+      - name: Materialize GHC 9
+        run: nix run .#update-cabal-ghc9
 
       - name: Update branch
         env:

.gitignore

@@ -49,3 +49,4 @@ cabal.project.local
 kore-exec.tar.gz
 hie.yaml
 .hie/
+.direnv

.hlint.yaml

@@ -157,6 +157,7 @@
     within:
       - GlobalMain
       - Kore.Log.InfoExecDepth
+      - Kore.Log.WarnUnexploredBranches
 
 - ignore: {name: "Redundant compare", within: [Kore.Syntax.Id]}
 

Dockerfile

@@ -1,5 +1,5 @@
 ARG K_COMMIT
-FROM runtimeverificationinc/kframework-k:ubuntu-bionic-${K_COMMIT}
+FROM runtimeverificationinc/kframework-k:ubuntu-focal-${K_COMMIT}
 
 ENV TZ=America/Chicago
 RUN    ln --symbolic --no-dereference --force /usr/share/zoneinfo/$TZ /etc/localtime \
@@ -50,4 +50,4 @@ RUN mkdir -p ~/.ssh                                                   \
     && echo '    user git'                         >> ~/.ssh/config   \
     && echo '    identityagent SSH_AUTH_SOCK'      >> ~/.ssh/config   \
     && echo '    stricthostkeychecking accept-new' >> ~/.ssh/config   \
-    && chmod go-rwx -R ~/.ssh
+    && chmod go-rwx -R ~/.ssh

Makefile

@@ -31,12 +31,13 @@ haddock:
 		--fast \
 		>haddock.log 2>&1 \
 		|| ( cat haddock.log; exit 1; )
-	cat haddock.log
-	if grep -B 2 'Module header' haddock.log; then \
+        #remove header warning for Paths_kore
+	sed -e "/.*in 'Paths_kore'$/{n;n;/^ *Module header$/d}" haddock.log | tee haddock.log.noPaths
+	if grep -B 2 'Module header' haddock.log.noPaths; then \
 		echo >&2 "Please fix the missing documentation!"; \
 		exit 1; \
 	else \
-		rm haddock.log; \
+		rm haddock.log*; \
 	fi
 
 haskell_documentation: haddock
@@ -74,4 +75,4 @@ clean:
 	$(MAKE) -C test clean
 
 clean-execution:
-	$(MAKE) -C test clean-execution
+	$(MAKE) -C test clean-execution

README.md

@@ -43,6 +43,8 @@ cabal build kore
 ```
 
 If using `cabal`, version 3.0 or later is recommended.
+You may pass `--fast` to `stack build` or `-O0` to `cabal build` in order to
+disable compiler optimizations and make build faster at the cost of slower runtime.
 
 Using [make]:
 
@@ -132,19 +134,101 @@ cabal build --enable-tests --enable-benchmarks --only-dependencies kore
 
 ### Developing with Nix
 
+To build and run nix based packages at RV, please follow these instructions to set up nix:
+
+_We are switching to using [nix flakes](https://nixos.wiki/wiki/Flakes) in all our repos. What this means at a high level is that some of the commands for building packages look a bit different._
+
+To set up nix flakes you will need to install `nix` 2.4 or higher.If you are on a standard Linux distribution, such as Ubuntu, first [install nix](https://nixos.org/download.html#download-nix)
+and then enable flakes by editing either `~/.config/nix/nix.conf` or `/etc/nix/nix.conf` and adding:
+
+```
+experimental-features = nix-command flakes
+```
+
+This is needed to expose the Nix 2.0 CLI and flakes support that are hidden behind feature-flags. (If you are on a different system like nixOS, see instructions for enabling flakes here: https://nixos.wiki/wiki/Flakes)
+
+By default, Nix will build any project and its transitive dependencies from source, which can take a very long time. We therefore need to set up some binary caches to speed up the build
+process. First, install cachix
+
+```
+nix-env -iA cachix -f https://cachix.org/api/v1/install
+```
+
+and then add the `kore` cachix cache
+
+```
+cachix use kore
+```
+
+Next, we need to set up the cache for our haskell infrastructure, by adding the following sections to `/etc/nix/nix.conf` or, if you are a trusted user, `~/.config/nix/nix.conf` (if you don't know what a "trusted user" is, you probably want to do the former):
+
+```
+trusted-public-keys = ... hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+substituters = ... https://cache.iog.io
+```
+
+i.e. if the file was originally
+
+```
+substituters = https://cache.nixos.org
+trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+```
+
+it will now read
+
+```
+substituters = https://cache.nixos.org https://cache.iog.io
+trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+```
+
+
+### Nix dev shell
+
 We provide a `shell.nix` expression with a suitable development environment and
 a binary cache at [runtimeverification.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 with flakes enabled.
+nix run .#update-cabal
+```
+
+or
+
+```
 # Requires Nix to be installed.
 ./nix/rematerialize.sh
 ```
 
 This script is also run by an automatic workflow.
 
+### New GHC 9.2.3 dev shell
+
+In order to make use of the new profiling options in GHC 9.2, we've added a nix shell which builds kore with GHC 9.2.3, to open the shell, run
+
+```
+nix develop .#ghc9
+```
+
+Then, use stack to build against `stack-nix-ghc9.yaml`:
+
+```
+stack --stack-yaml stack-nix-ghc9.yaml build
+```
+
+If you modified the `kore.cabal` file and want to build with GHC 9, you will have to run
+
+```
+# Requires Nix with flakes enabled.
+nix run .#update-cabal-ghc9
+```
+
+
+### Integration tests
+
 We provide a `test.nix` for running integration tests:
 
 ``` sh
@@ -153,6 +237,15 @@ nix-build test.nix --argstr test imp  # run the integration tests in test/imp
 nix-shell test.nix  # enter a shell where we can run tests manually
 ```
 
+You can also us a new nix flake shell feature to compile the K framework against your current version of haskell backend and bring K into scope of your current shell via
+
+```
+nix shell github:runtimeverification/k/<commit> --override-input haskell-backend $(pwd)
+```
+
+where `<commit>` can be empty or point to a specific version of the K framework github repository. Running this command will add all of the K binaries like `kompile` or `kast` into the `PATH` of your current shell (this is not permanent and will only persist in your current shell window until you close it).
+
+
 [docs]: https://github.com/runtimeverification/haskell-backend/tree/master/docs
 [git]: https://git-scm.com/
 [stack]: https://www.haskellstack.org/