Merge pull request #18 from input-output-hk/bwbush/peras-hs

Haskell package maintenance

.github/workflows/ci.yaml

@@ -10,7 +10,7 @@ on:
     - main
 jobs:
   typecheck:
-    name: Typecheck Agda and generate Haskell
+    name: Typecheck Agda and build Haskell
     runs-on: self-hosted
     steps:
     - name: 📥 Checkout repository
@@ -25,6 +25,16 @@ jobs:
           trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }}
           substituters = ${{ env.SUBSTITUTERS }}
           experimental-features = nix-command flakes
-    - name: 🧪 Evaluate typecheck derivation
+    - name: 🧪 Typecheck Agda
       run: |
         nix build --show-trace .#peras
+    - name: 🧪 Build `peras-iosim`.
+      run: |
+        nix build --show-trace .#peras-iosim
+    - name: 🧪 Build `peras-quickcheck`.
+      run: |
+        echo "⏳ CURRENTLY DISABLED"
+#       nix build --show-trace .#peras-quickcheck
+    - name: 🧪 Build `random-forks`.
+      run: |
+        nix build --show-trace .#random-forks

Logbook.md

@@ -1,5 +1,14 @@
 ## 2024-02-12
 
+### BB - Haskell package maintenance
+
+1. Separated Haskell files generated by `agda2hs` to separate folders from the Agda source, in the [peras-hs](peras-hs/) package.
+2. Relocated `Peras.Ophans` from `peras-iosim` to `peras-hs`.
+3. Added Haskell package builds to CI.
+4. Added formatting pre-commit check for Haskell and Nix files.
+5. Turned on `StrictData` language extension for `peras-hs` and `peras-iosim`.
+6. Temporarily disabled `peras-quickcheck` in [cabal.project](cabal.project) and [.github/workflows/ci.yaml](.github/workflows/ci.yaml), due to missing `netsim` library.
+
 ### AB - Connecting quickcheck & Rust
 
 Having "fun" calling Rust library from Haskell through FFI.

Makefile

@@ -1,7 +1,8 @@
 # Inspired by https://git.app.uib.no/hott/agda-unimath/-/blob/6f6a48c92912da3f1245b846c5439c63d1461792/Makefile
 AGDAFILES := $(wildcard src/**/*.agda)
 AGDAIFILES := $(patsubst %.agda,%.agdai,$(AGDAFILES))
-HSFILES := $(patsubst %.agda,%.hs,$(AGDAFILES))
+HSDIR=peras-hs
+HSFILES := $(patsubst %.agda,$(HSDIR)/%.hs,$(AGDAFILES))
 AGDAFLAGS := -i src
 AGDA ?= agda
 AGDA2HS ?= agda2hs
@@ -11,18 +12,15 @@ AGDA_LIBS ?=
 
 typecheck: $(AGDAIFILES) $(HSFILES)
 
+
 # From https://stackoverflow.com/questions/34621364/makefile-compile-o-from-c-files
 $(AGDAIFILES): %.agdai: %.agda
 	@$(AGDA) $(AGDAFLAGS) $^
 
-$(HSFILES): %.hs: %.agda
-	@$(AGDA2HS) $(AGDA_LIBS) $^
+$(HSDIR)/%.hs: %.agda
+	@$(AGDA2HS) $(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^
 
 .PHONY : clean veryclean
 clean:
 	@echo "Removing .agdai files"
 	@find src -name \*.agdai -delete;
-
-veryclean: clean
-	@echo "Removing .hs files"
-	@find src -name \*.hs -delete;

cabal.project

@@ -15,9 +15,9 @@ index-state:
   , cardano-haskell-packages 2023-12-15T14:50:31Z
 
 packages:
-  .
+  peras-hs
   peras-iosim
-  peras-quickcheck
+--peras-quickcheck
   random-forks
   sketch
 

fourmolu.yaml

@@ -1,6 +1,17 @@
 indentation: 2
-column-limit: 120
-function-arrows: leading
-haddock-style: single-line
-let-style: inline
-indent-wheres: true
+comma-style: leading # for lists, tuples etc. - can also be 'trailing'
+record-brace-space: false # rec {x = 1} vs. rec{x = 1}
+indent-wheres: false # 'false' means save space by only half-indenting the 'where' keyword
+diff-friendly-import-export: true # 'false' uses Ormolu-style lists
+respectful: true # don't be too opinionated about newlines etc.
+haddock-style: single-line # '--' vs. '{-'
+newlines-between-decls: 1 # number of newlines between top-level declarations
+single-constraint-parens: never # whether or not to put braces around single constraints: https://fourmolu.github.io/config/single-constraint-parens/
+fixities:
+  - infixr 0 $
+  - infixr 1 &
+  - infixl 3 <|>
+  - infixr 3 &&
+  - infixl 1 <&>
+  - infixl 4 <$>
+  - infixl 4 <*>

nix/agda-packages.nix

@@ -39,7 +39,7 @@ let
     };
 in
 
-  pkgs.agdaPackages.override {
-    Agda = frankenAgda;
-    pkgs = frankenPkgs;
-  }
+pkgs.agdaPackages.override {
+  Agda = frankenAgda;
+  pkgs = frankenPkgs;
+}

nix/agda-with-stdlib.nix

@@ -3,4 +3,4 @@
 let
   stdlib = repoRoot.nix.agda-stdlib;
 in
-  repoRoot.nix.agda-packages.agda.withPackages [ stdlib ]
+repoRoot.nix.agda-packages.agda.withPackages [ stdlib ]

nix/agda2hs.nix

@@ -18,4 +18,4 @@ let
 
 in
 
-  project.hsPkgs.agda2hs.components.exes.agda2hs 
+project.hsPkgs.agda2hs.components.exes.agda2hs 

nix/outputs.nix

@@ -4,12 +4,12 @@ let
   project = repoRoot.nix.project;
   peras-agda = repoRoot.nix.peras-agda;
 in
-  [
-    ( 
-      project.flake
-    )
-    {
-      inherit repoRoot;
-      packages.peras = peras-agda;
-    }
-  ]
+[
+  (
+    project.flake
+  )
+  {
+    inherit repoRoot;
+    packages.peras = peras-agda;
+  }
+]

nix/peras-agda.nix

@@ -3,26 +3,26 @@
 let
   agdaPackages = repoRoot.nix.agda-packages;
 in
-  pkgs.stdenv.mkDerivation {
-    version = "1.0";
-    pname = "peras";
-    src = ./..;
-    meta = {
-      description = "Agda library for Peras.";
-    };
-    buildInputs = [
-      repoRoot.nix.agda-with-stdlib
-      repoRoot.nix.agda-stdlib
-      repoRoot.nix.agda2hs
-      pkgs.gnumake
-    ];
-    buildPhase = ''
-      echo "${repoRoot.nix.agda-stdlib}/standard-library.agda-lib" > libraries
-      export AGDA_LIBS="--local-interfaces --library-file=$PWD/libraries"
-      make
-    '';
-    installPhase = ''
-      mkdir "$out"
-      cp -pr peras.agda-lib src "$out"
-    '';
-  }
+pkgs.stdenv.mkDerivation {
+  version = "1.0";
+  pname = "peras";
+  src = ./..;
+  meta = {
+    description = "Agda library for Peras.";
+  };
+  buildInputs = [
+    repoRoot.nix.agda-with-stdlib
+    repoRoot.nix.agda-stdlib
+    repoRoot.nix.agda2hs
+    pkgs.gnumake
+  ];
+  buildPhase = ''
+    echo "${repoRoot.nix.agda-stdlib}/standard-library.agda-lib" > libraries
+    export AGDA_LIBS="--local-interfaces --library-file=$PWD/libraries"
+    make
+  '';
+  installPhase = ''
+    mkdir "$out"
+    cp -pr peras.agda-lib src "$out"
+  '';
+}

nix/project.nix

@@ -16,7 +16,7 @@ let
       };
       name = "my-project";
       compiler-nix-name = lib.mkDefault "ghc96";
-      modules = [];
+      modules = [ ];
     });
 
   cabalProject = cabalProject'.appendOverlays [ ];
@@ -28,4 +28,4 @@ let
 
 in
 
-  project
+project

nix/shell.nix

@@ -10,6 +10,8 @@ cabalProject:
     repoRoot.nix.agda-stdlib
     repoRoot.nix.agda2hs
     repoRoot.nix.emacs-with-packages
+    pkgs.haskellPackages.pointfree
+    # pkgs.haskellPackages.pointful
     pkgs.gnumake
     pkgs.graphviz
   ];
@@ -39,27 +41,21 @@ cabalProject:
     # purs-tidy = null;
   };
 
-  # preCommit = {
-  #   cabal-fmt.enable = false;
-  #   cabal-fmt.extraOptions = "";
-  #   stylish-haskell.enable = false;
-  #   stylish-haskell.extraOptions = "";
-  #   fourmolu.enable = false;
-  #   fourmolu.extraOptions = "";
-  #   hlint.enable = false;
-  #   hlint.extraOptions = "";
-  #   shellcheck.enable = false;
-  #   shellcheck.extraOptions = "";
-  #   prettier.enable = false;
-  #   prettier.extraOptions = "";
-  #   editorconfig-checker.enable = false;
-  #   editorconfig-checker.extraOptions = "";
-  #   nixpkgs-fmt.enable = false;
-  #   nixpkgs-fmt.extraOptions = "";
-  #   optipng.enable = false;
-  #   optipng.extraOptions = "";
-  #   purs-tidy.enable = false;
-  #   purs-tidy.extraOptions = "";
-  # };
+  preCommit = {
+    cabal-fmt.enable = false;
+    #   cabal-fmt.extraOptions = "";
+    fourmolu.enable = true;
+    #   fourmolu.extraOptions = "";
+    hlint.enable = false;
+    #   hlint.extraOptions = "";
+    #   shellcheck.enable = false;
+    #   shellcheck.extraOptions = "";
+    #   editorconfig-checker.enable = false;
+    #   editorconfig-checker.extraOptions = "";
+    nixpkgs-fmt.enable = true;
+    #   nixpkgs-fmt.extraOptions = "";
+    #   optipng.enable = false;
+    #   optipng.extraOptions = "";
+  };
 }