Error running timer ‘dhall-buffer-type-compute’: (wrong-type-argument stringp nil)

[reuleaux]

I get this error currently

Error running timer ‘dhall-buffer-type-compute’: (wrong-type-argument stringp nil)

with

(setq debug-on-error t)

I get to see

Debugger entered--Lisp error: (wrong-type-argument stringp nil)
  string-match("↳" nil nil)
  dhall-buffer-type()
  dhall-buffer-type-compute()
  apply(dhall-buffer-type-compute nil)
  timer-event-handler([t 23511 2211 494750 nil dhall-buffer-type-compute nil nil 157000])

any idea? - don't know if this is related to issue #18
thanks.

[purcell]

Which dhall version are you using?

[reuleaux]

Steve Purcell <[email protected]> writes: R> Which `dhall` version are you using? rx@mirabelle ~/work/site $ dhall version 1.18.0 rx@mirabelle ~/work/site $ Thanks, -A

[purcell]

1fa48e3 addresses the error, but I still need to figure out the cause. I think I might have seen something about dhall changing so that it no longer prints out the type of the expression by default -- perhaps that's it?

[haitlahcen]

@purcell I encountered the same issue. And as you said, the type is no longer given to stderr by dhall since 1.17. Either we have to pipe the file to cat file.dhall | dhall resolve | dhall type to get the type or extract the annotation after calling cat file.dhall | dhall --annotate. See dhall-lang/dhall-haskell#641

[purcell]

Does it work for you with the following version of dhall-buffer-type?

(defun dhall-buffer-type ()
  "Return the type of the expression in the current buffer."
  (interactive)
  (when (executable-find dhall-command)
    (let ((stderr (make-temp-file "dhall-buffer-type")))
      (unwind-protect
          (when (zerop (call-process-region (point-min)
                                            (point-max)
                                            dhall-command
                                            nil
                                            (list nil stderr)
                                            nil
                                            "--annotate"))
            (let ((type (car (split-string (with-temp-buffer
                                             (insert-file-contents stderr)
                                             (buffer-string))
                                           "[�]+"
                                           t
                                           split-string-default-separators))))

              (unless (and type (string-match-p "↳" type))
                (ansi-color-apply (replace-regexp-in-string "[\n\s]+" " " type)))))
        (delete-file stderr)))))

[haitlahcen]

@purcell The type annotation is now given in an Idris style:

1.15: cat test.dhall | dhall

{ X : Type }

{ X = { a : Text } }

1.18: cat test.dhall | dhall --annotate

{ X = { a : Text } } : { X : Type }

1.18: cat test.dhall | dhall resolve | dhall type

{ X : Type }

I've made it working by hardcoding ugly code (not very fluent in lisp yet).

(defun dhall-buffer-type ()
  "Return the type of the expression in the current buffer."
  (interactive)
  (when (executable-find dhall-command)
    (ansi-color-apply (replace-regexp-in-string "[\n\s]+" " " (shell-command-to-string (concat (concat "cat " buffer-file-name) " | dhall resolve | dhall type"))))))

I think that it would be much more robust against upgrades if we actually use the dhall type command instead of splitting the result of dhall --annotate

[purcell]

Thanks. That method won't work when there's no file backing the current buffer, but I'll see what I can do. Certainly looks like the combination of dhall resolve and dhall type is the way to go.