0

I have some simple code to plot some data using the Chart Haskell library:

-- Dynamical/Plot/src/HsPlot.hs
module HsPlot where

import Graphics.Rendering.Chart.Easy
import Graphics.Rendering.Chart.Backend.Cairo

plotToFile :: Double -> [Double] -> [Double] -> IO ()
plotToFile dt r f = toFile def "plot.png" $ do
    layout_title .= "Dynamics idk"
    setColors [opaque blue, opaque red]
    plot (line "rabbits" [zip [0, dt..] r ])
    plot (line "foxes" [zip [0, dt..] f])

and some Agda code which I intend to call it from:

-- Dynamical/Plot/Plot.agda
{-# OPTIONS --sized-types --guardedness #-}

module Dynamical.Plot.Plot where

open import Agda.Builtin.IO
open import Data.Float
open import Data.Unit
open import Data.List as List using (List)
open import Data.Product

postulate
  plotDynamics  : Float → List Float → List Float → IO ⊤

{-# FOREIGN GHC import HsPlot #-}
{-# COMPILE GHC plotDynamics = plotToFile #-}

open import Dynamical.LotkaVolterra
import Data.Vec as Vec

main = do
  -- lvList is a Vec of Floats, needs to be a list
  let dyn = Vec.toList lvList
  let r , f = List.unzip dyn
  plotDynamics 0.1 r f

There is also a cabal file listing Chart and Chart-cairo as dependencies in the directory Dynamical/Plot, so right next to the Agda file. Trying to agda -c Dynamical/Plot/Plot.agda --ghc-flag=-iDynamical/Plot/src will give me

/Users/deco/work/poly/MAlonzo/Code/Dynamical/Plot/Plot.hs:29:1: error:
    Could not find module ‘HsPlot’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
29 | import HsPlot

So it doesn't even find my Haskell module, let alone the Cabal dependencies. I'm trying to avoid using the flag --ghc-dont-call-ghc because that just generates a mountain of Haskell code which would be annoying to integrate with my little plotting code. I don't see any option to give the GHC backend instructions on how to find the cabal file or any modules I might have. How do I do this?

Here's the directory structure in full, too:

> tree
.
├── Categorical
│   ├── Adjunction.agda
│   ├── CartesianClosed.agda
│   ├── CompositionMonoid.agda
│   ├── Coproduct.agda
│   ├── CubicalPoly.agda
│   ├── Exponential.agda
│   ├── Functor
│   │   ├── Constant.agda
│   │   ├── Linear.agda
│   │   ├── PlugInOne.agda
│   │   └── PlugInZero.agda
│   ├── Gist.agda
│   ├── Initial.agda
│   ├── ParallelProductMonoid.agda
│   ├── Product.agda
│   └── Terminal.agda
├── Common
│   └── CategoryData.agda
└── Dynamical
    ├── Fibonacci.agda
    ├── HodgkinHuxley.agda
    ├── LotkaVolterra.agda
    ├── Plot
    │   ├── HsPlot.cabal
    │   ├── Plot.agda
    │   ├── hie.yaml
    │   └── src
    │       └── HsPlot.hs
    ├── System.agda
    └── Turing.agda

1 Answer 1

1

Found a solution. First of all, the Haskell module was imported as the wrong thing. Since I'm giving the raw directory to Agda, I should have just written {-# FOREIGN GHC import HsPlot #-}.

I didn't want to have to install things locally, so I ended up with this nix expression. Key part is haskellDeps and customGhc; callCabal2Nix will read the cabal file it's given and turn it into a nix expression (with package dependencies appearing as propagatedBuildInputs), and the ghcWithPackages function will add the haskell packages it's given to a bespoke GHC package database.

{ pkgs ? import <nixpkgs> {} }:

let
  # So that we don't have to repeat ourselves in the configurePhase and the
  # agdaDeps variable.
  agdaDepsNames = [
    "standard-library"
    "agda-categories"
    "cubical"
  ];
  agdaDeps = builtins.map (n: pkgs.agdaPackages.${n}) agdaDepsNames;
  
  haskellDeps = 
    builtins.filter (d: !(isNull d)) (pkgs.haskellPackages.callCabal2nix "HsPlot" ./Dynamical/Plot/HsPlot.cabal {}).propagatedBuildInputs;
  # Create a custom GHC environment with the needed dependencies. What this will do is "install"
  # a GHC that has a package db listing the dependencies in the cabal file.
  customGhc = pkgs.haskellPackages.ghcWithPackages (ps: haskellDeps);

in
pkgs.stdenv.mkDerivation {
  name = "plot";
  src = ./.;

  nativeBuildInputs = with pkgs; [
    customGhc
    (agda.withPackages (p: agdaDeps))
  ];

  configurePhase = ''
    export AGDA_DIR=$PWD/.agda
    mkdir -p $AGDA_DIR

    for dep in ${pkgs.lib.concatStringsSep " " agdaDepsNames}; do
      echo $dep >> $AGDA_DIR/defaults
    done
  '';

  buildPhase = ''
    agda -c \
      --ghc-flag=-iDynamical/Plot/src \
      ${pkgs.lib.concatMapStrings (dep: "--ghc-flag=-package=${dep.name} ") haskellDeps} \
      --ghc-flag=-package-db=${customGhc}/lib/ghc-${customGhc.version}/package.conf.d \
      Dynamical/Plot/Plot.agda
  '';

  installPhase = ''
    mkdir -p $out/bin
    cp $TMP/poly/Plot $out/bin
  '';

  meta = with pkgs.lib; {
    description = "A simple Agda project that plots data using the Chart library";
    license = licenses.mit;
  };
}
2
  • 1
    With modern cabal, you generally shouldn't be installing libraries. I'm not sure I have a great alternative, but perhaps you can ask cabal to make you an environment file and use that instead? So, inside your cabal package directory, cabal build --write-ghc-environment-files=always, then invoke Agda with something like agda -c Dynamical/Plot/Plot.agda --ghc-flag=-package-env=Dynamical/Plot/.ghc.environment. Mar 17 at 20:43
  • 1
    @DanielWagner yeah I agree that's pretty terrible. I ended up writing a Nix expression that creates a custom GHC environment instead. See the updated answer. Mar 20 at 10:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.