/home/laney/.irssi/irclogs/Freenode/#agda.log-20180208

--- Day changed Wed Feb 07 2018
Fractal697I’m trying to use the Haskell trace function from an Agda program. I tried the following but it didn’t work.07/02 16:56
Fractal697{-# FOREIGN GHC import qualified Debug.Trace as Trace #-} postulate   trace : {A : Set} → String → A → A {-# COMPILE GHC trace = \ _ s x -> Trace.trace s x #-} 07/02 16:56
Fractal697I get:     • Couldn't match type ‘Data.Text.Text’ with ‘[Char]’       Expected type: String         Actual type: MAlonzo.Code.Agda.Builtin.String.T6     • In the first argument of ‘Trace.trace’, namely ‘s’       In the expression: Trace.trace s x       In the expression: \ _ s x -> Trace.trace s x 07/02 16:57
Fractal697Anyone knows what I’m doing wrong?07/02 16:57
pgiarrussoFractal697: educated guess: `Trace.trace` takes a Haskell `String`, but Agda `String` are mapped to `Text` (ahem, `Data.Text.Text`), so you need to convert from `Text` to `String`07/02 17:06
pgiarrussoFractal697: when looking up the function from the `text` package, remember it has multiple `Text` datatypes (from different packages)07/02 17:07
Fractal697Ah, good point, I didn’t realize that Haskell’s String type was something different07/02 17:07
pgiarrussoFractal697: IIRC MAlonzo generates plain Haskell code, so you should be able to look at it to verify it07/02 17:07
pgiarrussoFractal697: I’m hypothesizing that from the error07/02 17:08
pgiarrussoI’d guess in the Agda “builtin” libraries there’s a COMPILE_GHC directive setting up the mapping07/02 17:08
Fractal697I converted the Text to a String using Data.Text.unpack and it seems to work now, thanks!07/02 17:10
pgiarrussoyep, that sounds correct! good luck!07/02 17:11
mietekI wonder if they’re getting useful output07/02 18:17
trikl[m]Is it possible to generate PDF documents with colour from literate Agda sources with xelatex?07/02 22:49
trikl[m]If I define the `code` environment as a verbatim I get the actual tex commands generated by `agda --latex` as verbatim07/02 22:58
trikl[m]If I define `code` as a dummy environment xelatex complains about missing `$`s where Agda's tex commands go07/02 23:03
trikl[m]I forgot to actually load the generated `agda.sty` :S07/02 23:17

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!