imandra-ai / imandra-vscode

VSCode extension for developing imandra
Other
2 stars 0 forks source link

`[@@@require]` not working #26

Closed ewenmaclean closed 5 years ago

ewenmaclean commented 5 years ago

As an example consider the below file - the require does not seem to be executed by the imandra-server even though it checks that the required library exists ([@@@require "foo"] correctly raises an error for example)

let f x = x + 1;;

[@@@program]
[@@@require "decoders-yojson"]
open Decoders_yojson.Basic.Decode;;

let int_decoder = int

this raises imandra tagged errors:

File "/Users/ewenmaclean/ai/testImandra2/test.iml", line 5, characters 5-33:
Error: Unbound module Decoders_yojson
imandra

this is not a merlin error with appropriate dune file this works for merlin - e.g.:

(rule
  (targets test.ml)
  (deps test.iml)
   (action
    (with-stdout-to test.ml
       (run imandra-extract test.iml))))

(library
  (name test)
  (public_name test)
  (wrapped false)
  (flags (:standard -open Imandra_prelude -warn-error -A+8+39))
  (libraries imandra-base.prelude decoders-yojson)
)