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