Added formal spec to Nix shell and CI

.github/workflows/ci.yaml

@@ -13,12 +13,52 @@ on:
     - main
 jobs:
 
+  typecheck:
+    name: Typecheck specification
+    runs-on: ubuntu-22.04
+    steps:
+    - name: 📥 Checkout repository
+      uses: actions/checkout@v4
+    - name: 💾 Cache Nix store
+      uses: actions/[email protected]
+      id: nix-cache
+      with:
+        path: /tmp/nixcache
+        key: ${{ runner.os }}-nix-typecheck-${{ hashFiles('flake.lock') }}
+        restore-keys: ${{ runner.os }}-nix-typecheck-
+    - name: 🛠️ Install Nix
+      uses: cachix/install-nix-action@v21
+      with:
+        nix_path: nixpkgs=channel:nixos-unstable
+        install_url: https://releases.nixos.org/nix/nix-2.10.3/install
+        extra_nix_config: |
+          allowed-uris = ${{ env.ALLOWED_URIS }}
+          trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }}
+          substituters = ${{ env.SUBSTITUTERS }}
+          experimental-features = nix-command flakes
+    - name: 💾➤ Import Nix store cache
+      if: "steps.nix-cache.outputs.cache-hit == 'true'"
+      run: "nix-store --import < /tmp/nixcache"
+    - name: 🏗️ Build specification
+      run: |
+        nix build --show-trace --accept-flake-config .#leiosSpec
+    - name: ➤💾 Export Nix store cache
+      if: "steps.nix-cache.outputs.cache-hit != 'true'"
+      run: "nix-store --export $(find /nix/store -maxdepth 1 -name '*-*') > /tmp/nixcache"
+
   compile:
     name: Build libraries
     runs-on: ubuntu-22.04
     steps:
     - name: 📥 Checkout repository
       uses: actions/checkout@v4
+    - name: 💾 Cache Nix store
+      uses: actions/[email protected]
+      id: nix-cache
+      with:
+        path: /tmp/nixcache
+        key: ${{ runner.os }}-nix-compile-${{ hashFiles('flake.lock') }}
+        restore-keys: ${{ runner.os }}-nix-compile-
     - name: 🛠️ Install Nix
       uses: cachix/install-nix-action@v21
       with:
@@ -29,12 +69,18 @@ jobs:
           trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }}
           substituters = ${{ env.SUBSTITUTERS }}
           experimental-features = nix-command flakes
+    - name: 💾➤ Import Nix store cache
+      if: "steps.nix-cache.outputs.cache-hit == 'true'"
+      run: "nix-store --import < /tmp/nixcache"
     - name: 🏗️ Build `exe:leios`
       run: |
         nix build --show-trace --accept-flake-config .#leios
     - name: 🏗️ Build `exe:ouroboros-net-vis`
       run: |
         nix build --show-trace --accept-flake-config .#ouroboros-net-vis
+    - name: ➤💾 Export Nix store cache
+      if: "steps.nix-cache.outputs.cache-hit != 'true'"
+      run: "nix-store --export $(find /nix/store -maxdepth 1 -name '*-*') > /tmp/nixcache"
 
   tests:
     if: true
@@ -43,6 +89,13 @@ jobs:
     steps:
     - name: 📥 Checkout repository
       uses: actions/checkout@v4
+    - name: 💾 Cache Nix store
+      uses: actions/[email protected]
+      id: nix-cache
+      with:
+        path: /tmp/nixcache
+        key: ${{ runner.os }}-nix-tests-${{ hashFiles('flake.lock') }}
+        restore-keys: ${{ runner.os }}-nix-tests-
     - name: 🛠️ Install Nix
       uses: cachix/install-nix-action@v21
       with:
@@ -53,9 +106,15 @@ jobs:
           trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }}
           substituters = ${{ env.SUBSTITUTERS }}
           experimental-features = nix-command flakes
+    - name: 💾➤ Import Nix store cache
+      if: "steps.nix-cache.outputs.cache-hit == 'true'"
+      run: "nix-store --import < /tmp/nixcache"
     - name: 🔬 Test with `leios-sim-test`
       run: |
         nix run --accept-flake-config .#leios-sim-test
+    - name: ➤💾 Export Nix store cache
+      if: "steps.nix-cache.outputs.cache-hit != 'true'"
+      run: "nix-store --export $(find /nix/store -maxdepth 1 -name '*-*') > /tmp/nixcache"
 
   build-docusaurus:
     runs-on: ubuntu-22.04

Logbook.md

@@ -1,3 +1,30 @@
+## 2024-08-30
+
+### Nix and CI support for Leios specification
+
+The Nix flake now builds the Leios specification and the libraries upon which it depends. The type checking of the spec is now added to the CI.
+
+```console
+$ nix develop
+
+Welcome to Ouroboros Leios!
+
+Locations of Agda libraries:
+  /nix/store/1yxiwwy44xxxgzdmvyjizq53w9cfinkn-standard-library-2.0/standard-library.agda-lib
+  /nix/store/ppsczpm7l2gx1zd3cx2brv49069krzzh-agda-stdlib-classes-2.0/standard-library-classes.agda-lib
+  /nix/store/gkci6kgv4v9qw2rh5gc0s26g53b253jy-agda-stdlib-meta-2.0/standard-library-meta.agda-lib
+  /nix/store/2gk6rvsplxww4i8dnflxbd319lfxdcvv-formal-ledger-1d77a35a/formal-ledger.agda-lib
+
+Run 'emacs' to edit .agda files.
+
+
+Type 'info' to see what's inside this shell.
+
+$ cd formal-spec
+
+$ emacs Leios/SimpleSpec.agda
+```
+
 ## 2024-07-26
 
 ### Running `ouroborous-net-viz` in the browser

flake.nix

@@ -6,10 +6,6 @@
   inputs = {
     iogx = {
       url = "github:input-output-hk/iogx";
-      # inputs.hackage.follows = "hackage";
-      # inputs.CHaP.follows = "CHaP";
-      # inputs.haskell-nix.follows = "haskell-nix";
-      # inputs.nixpkgs.follows = "nixpkgs";
     };
 
     # nixpkgs.follows = "haskell-nix/nixpkgs";
@@ -28,6 +24,7 @@
     #   url = "github:input-output-hk/haskell.nix";
     #   inputs.hackage.follows = "hackage";
     # };
+
   };
 
 

formal-spec/Leios/SimpleSpec.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module Leios.SimpleSpec where
 
 open import Ledger.Prelude

formal-spec/leios-spec.agda-lib

@@ -3,6 +3,6 @@ depend:
   standard-library
   standard-library-classes
   standard-library-meta
+  formal-ledger
 include:
   .
-  ../../formal-ledger-specifications/src/