On Mon, 15 Apr 2019, Jean-Christophe Filliatre wrote:
> Hi Julia,
>
> > Couldn't the extraction just leave undefined things as undefined?
>
> You can use the --modular option of Why3's extraction for this purpose.
>
> Move your undefined function(s) to a separate module, say module X in
> file a.mlw, and then extract whatever other file/modules using A, say
> b.mlw, with something like
>
> why3 extract -D ocaml64 --modular b.mlw -o .
>
> You'll get OCaml files such as b__M.ml with references to some OCaml
> module A__X. Now you are free to provide such a module A__X by any means.
That sounds fine. Thanks!
julia
>
> Hope this helps,
> --
> Jean-Christophe
>
> >> Le 14/04/19 à 18:51, Julia Lawall a écrit :
> >>
> >>
> >> On Sun, 14 Apr 2019, Mario Pereira wrote:
> >>
> >> Hi Julia,
> >>
> >> Can you please check if last commit (62c99f) fixes your extraction problem?
> >>
> >> I think it is ok. It doesn't actually work, because I have a function
> >> random_int that has no definition, but it doesn't give the error I was
> >> getting previously.
> >>
> >> julia
> >>
> >> Thank you in advance.
> >>
> >> Best regards
> >> --
> >> Mário
> >>
> >> Le 12/04/19 à 22:34, Julia Lawall a écrit :
> >>
> >>
> >> On Fri, 12 Apr 2019, Jean-Christophe Filliatre wrote:
> >>
> >> I think I managed to reproduce Julia's problem with a small input file:
> >>
> >> --------------------------------------------------
> >> use int.Int
> >>
> >> let f (x: int) : (ghost a: int, ghost b: int) =
> >> x+1, x+2
> >>
> >> let g (x: int) =
> >> let a, b = f x in
> >> ()
> >> --------------------------------------------------
> >>
> >> It fails on the same assertion.
> >>
> >> Thanks. My code has ghost on the let variables as well, but probbaly that
> >> is not necessary.
> >>
> >> julia
> >>
> >> --
> >> Jean-Christophe
> >>
> >> On 4/12/19 6:24 PM, Mario Pereira wrote:
> >>
> >> Do you have any suggestions of what to look for?
> >>
> >> It would maybe be helpful for me to debug the problem to know if this
> >> comes from pattern or type extraction.
> >>
> >> When you are calling the extraction engine, could you please add to your
> >> command line the following: "--debug stack_trace". We might be able to
> >> track down which function is calling the [visible_of_mask] function.
> >>
> >> Bests
> >> --
> >> Mário
> >>
> >>
> >> _______________________________________________
> >> Why3-club mailing list
> >> Why3-club@lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> >> _______________________________________________
> >> Why3-club mailing list
> >> Why3-club@lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> >> _______________________________________________
> >> Why3-club mailing list
> >> Why3-club@lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> >>
> >>>
> >>
> >> _______________________________________________
> >> Why3-club mailing list
> >> Why3-club@lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> >>
> >>
> >
> >
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
