Requires not propagated in file structures

[ewenmaclean]

If you write a file like this (called base.iml)

[@@@program]
[@@@require "decoders-yojson"]
module D = Decoders_yojson.Basic.Decode;; 

let base_decoder = D.int;;

[@@@logic]

this works great in VSCode. If you then write another to depend on it like this (called depender.iml)

[@@@program]
[@@@import "base.iml"]

let depends_decoder = Base.base_decoder

[@@@logic]

this only works if the cache has previously seen "base.iml".

To reproduce the bug - create a repo with these two files (dune file instructions below). Close all files and clear the imandra cache from VSCode. Then open only the second file, then you will get errors about the base.iml file saying it can't open the Decoders_yojson module. If you open base.iml there are no errors and once it gets in the cache, the depender.iml file errors go too.

Here's a dune file to place in the repo, along with an empty file called test_require.opam. Compile with command dune build but ensure the imandra_prelude implementations referenced on this switch are the same as the running imandra-merlin. I do this by running this build command: opam exec --switch=/usr/local/var/imandra -- dune build as my imandra-merlin runs merlin on that switch.

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

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

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

[c-cube]

see https://github.com/AestheticIntegration/imandra/pull/885