Merge pull request #12 from input-output-hk/bwbush/iogx

IOGX flake and CI

.github/workflows/ci.yaml

@@ -1,18 +1,21 @@
 name: CI
+env:
+  ALLOWED_URIS: "https://github.com https://api.github.com"
+  TRUSTED_PUBLIC_KEYS: "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ="
+  SUBSTITUTERS: "https://cache.nixos.org/ https://cache.iog.io"
 on:
   pull_request:
   push:
     branches:
     - main
-
 jobs:
   check:
+    if: false  # FIXME: The `agda2hs` step fails.
     name: Typecheck Agda
     runs-on: ubuntu-latest # or macOS-latest, or windows-latest
     steps:
     - name: 📥 Checkout repository
       uses: actions/checkout@v4
-
     # Setup Agda 2.6.3 with recommended version of agda-stdlib and
     # uses standard-library as default
     - name: ❄ Setup Agda
@@ -24,7 +27,26 @@ jobs:
           standard-library
         agda-libraries: |
           https://github.com/agda/agda2hs.git#v1.2
-
     - name: ❓ Typecheck
       run: |
         make typecheck
+  typecheck:
+    if: true  # FIXME: Consider disabling until caching is set up.
+    name: Typecheck Agda and generate Haskell
+    runs-on: ubuntu-latest
+    steps:
+    - name: 📥 Checkout repository
+      uses: actions/checkout@v4
+    - 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: 🧪 Evaluate typecheck derivation
+      run: |
+        nix build --show-trace .#peras

.gitignore

@@ -9,3 +9,5 @@ node_modules
 *.csv
 *.agdai
 src/MAlonzo/
+.pre-commit-config.yaml
+.libraries

.hlint.yaml

@@ -0,0 +1,24 @@
+# this is rarely an improvement
+- ignore: {name: Move brackets to avoid $}
+# this is often worse
+- ignore: {name: Use <$>}
+# this aids clarity since you can name the parameters
+- ignore: {name: Avoid lambda}
+- ignore: {name: Avoid lambda using `infix`}
+- ignore: {name: Replace case with fromMaybe}
+# whether this is better is very variable
+- ignore: {name: Use infix}
+# hlint can't handle typed TH: https://github.com/haskell-suite/haskell-src-exts/issues/383
+# annoyingly, 'within' doesn't seem to work if there's a parse error, so we have to blanket
+# ignore it
+- ignore: {name: Parse error}
+# This is rarely better, and often more confusing
+- ignore: {name: Use asks}
+# It seems clearer to use case than fromMaybe
+- ignore: {name: Use fromMaybe}
+- ignore: {name: Use section}
+
+- fixity: infixr 8 .*
+- fixity: infixr 3 ***
+- fixity: infixr 3 &&&
+- fixity: infixr 1 <=<

Logbook.md

@@ -1,5 +1,14 @@
 ## 2024-02-08
 
+### BB - Nix, Agda, and Haskell housekeeping
+
+1. Reconciled Haskell package dependencies.
+2. Included pre-built Agda standard library.
+3. Added `nix build .#peras` for building the Peras library in Agda and Haskell.
+4. Nix-based CI.
+
+*Issue:* the Nix-based CI test takes ~28 minutes, but this will be far faster when caching is enabled.
+
 ### Pairing session - Agda modelling of messages
 
 Some resources on agda2hs:

Makefile

@@ -5,6 +5,7 @@ HSFILES := $(patsubst %.agda,%.hs,$(AGDAFILES))
 AGDAFLAGS := -i src
 AGDA ?= agda
 AGDA2HS ?= agda2hs
+AGDA_LIBS ?=
 
 .PHONY: typecheck
 
@@ -15,9 +16,13 @@ $(AGDAIFILES): %.agdai: %.agda
 	@$(AGDA) $(AGDAFLAGS) $^
 
 $(HSFILES): %.hs: %.agda
-	@$(AGDA2HS) $^
+	@$(AGDA2HS) $(AGDA_LIBS) $^
 
-.PHONY : clean
+.PHONY : clean veryclean
 clean:
 	@echo "Removing .agdai files"
-	@find src -name \*.agdai -exec rm {} \;
+	@find src -name \*.agdai -delete;
+
+veryclean: clean
+	@echo "Removing .hs files"
+	@find src -name \*.hs -delete;

README.md

@@ -14,10 +14,13 @@ This repository is intended to host more or less formal specifications, experime
 
 The repository provides a nix flake from which one can enter a development shell suitable for Agda using the following command:
 
-```
+```bash
 nix develop
+make
 ```
 
+The Peras library for Agda can be built with `nix build .#peras`.
+
 #### Without nix
 
 Please check instructions for [Installing Agda](https://agda.readthedocs.io/en/latest/getting-started/installation.html) on the official website.