Re: [Why3-club] session update

2020-03-25 Thread Guillaume Melquiond 
Le 25/03/2020 à 10:07, Julia Lawall a écrit :
> It's not clear to me how why3 session update works.  I have a file called
> system.mlw, and thus a session directory called system.  I tried why3
> session update -rename-file system xxx and I obtain no file containing xxx
> in its name and grep -r xxx turns up nothing.  I did why3 session update
> -rename-file system xxx && echo ok and it printed ok, so I guess that it
> did not actually fail.

According to the code, it did absolutely nothing. It seems that you also
need to pass the session file on the command line. So, something like

why3 session update system/why3session.xml -rename-file system.mlw
xxx.mlw

But, even so, it still failed for me (anomaly: Not_found).

I had to use the fully canonicalized names for Why3 to find the files:

why3 session update system/why3session.xml -rename-file `pwd
-P`/system.mlw `pwd -P`/xxx.mlw

And yes, it did 'mv'.

Note that it does not move the session file itself. So, the modified
session is still system/why3session.xml.

Best regards,

Guillaume
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] session update

2020-03-25 Thread Julia Lawall 
It's not clear to me how why3 session update works.  I have a file called
system.mlw, and thus a session directory called system.  I tried why3
session update -rename-file system xxx and I obtain no file containing xxx
in its name and grep -r xxx turns up nothing.  I did why3 session update
-rename-file system xxx && echo ok and it printed ok, so I guess that it
did not actually fail.

I would actually like to copy an existing .mlw file and get a new copy of
the session as well (ie system should still exist and xxx should be
created referring to xxx.mlw).  The documentation suggests that why3
session update -rename-file does a mv and not a cp, which is less
convenient, but which I could live with.

thanks,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club