Change path of prelude

[xldenis]

In why3find we have no direct equivalent to -Lprelude which we currently use to make the prelude available to creusot code. Instead, it implicitly does -L .. To ensure that our code works with why3find, I changed the generation done by creusot so that all modules are prefixed by an additional prelude.. This ensures that our code is now verifiable by both why3find and why3, setting us up for a migration afterwards.

[jhjourdan]

Isn't this a missing feature of why3find? Could we ask them to support that?

[xldenis]

Isn't this a missing feature of why3find? Could we ask them to support that?

No I think this is intentional, as part of the idea of why3find is to control the notion of "packages", I don't think they want to be able to inject random files into the environment. Given that it's really a minor change to make this work with why3, I don't see any reason either.

[mojeanmac]

So currently the master branch of why3find accepts .mlcfg but not yet .coma since it's not a valid extension in Why3.Env in the current Why3 release. Did you need to rebuild why3find with the coma Why3 branch to get this to work? I came across the same exact issue as you did in https://git.frama-c.com/pub/why3find/-/issues/86

[xldenis]

Yes, you'll need to install why3find from the master branch (after having done opam install . --deps-only to update why3).

[Armael]

LGTM. Namespacing everything under prelude sounds good; if in the future we want identifiers that look less weird than prelude.prelude.Foo I guess we could split the contents of prelude/prelude.mlw into several prelude/foo.mlw files? (In any case we don't need to do that now.)

[Armael]

(feel free to merge after rebasing.)