Re: [Why3-club] matrix import
On Mon, 2 Jul 2018, Andrei Paskevich wrote: > On 2 July 2018 at 14:56, Julia Lawall wrote: > > Previously, set was a function that returned the new matrix. Now the > > return type is unit. I think that this is the source of the problem. > > Indeed, looking at stdlib/matrix.ml, there is no more pure applicative > version of "set" for matrices. This is a regression, which I've now > fixed in master. The function is called "update", to distinguish it > from the effectful "set". Great. Thanks! julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] matrix import
On 2 July 2018 at 14:56, Julia Lawall wrote: > Previously, set was a function that returned the new matrix. Now the > return type is unit. I think that this is the source of the problem. Indeed, looking at stdlib/matrix.ml, there is no more pure applicative version of "set" for matrices. This is a regression, which I've now fixed in master. The function is called "update", to distinguish it from the effectful "set". Best, Andrei ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] matrix import
On Mon, 2 Jul 2018, Andrei Paskevich wrote: > Hi Julia, > > you simply write "use array.Array" and "use matrix.Matrix" — the import will > be done by default. You wirte "use ... as" when you _don't_ want import. > And, of course, you still can write "use import array.Array as A" if you > want to name the scope "A" _and_ to import it, too. Previously, set was a function that returned the new matrix. Now the return type is unit. I think that this is the source of the problem. julia > > Best, > Andrei > > On 2 July 2018 at 12:04, Julia Lawall wrote: > Hello, > > I am trying to get my 0.88 code to work with why3 1.0. I have > > use import array.Array as A > use import matrix.Matrix as MM > > According to my understanding, the imports are no longer > needed. I tried: > > use array.Array as A > use matrix.Matrix as MM > > but then it doesn't recognize the type matrix. > > With the imports it doesn't recognize MM.set. What should be > done > instead? > > julia > ___ > 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
Re: [Why3-club] matrix import
On Mon, 2 Jul 2018, Andrei Paskevich wrote: > Hi Julia, > > you simply write "use array.Array" and "use matrix.Matrix" — the import will > be done by default. You wirte "use ... as" when you _don't_ want import. > And, of course, you still can write "use import array.Array as A" if you > want to name the scope "A" _and_ to import it, too. OK, I think my system is set up in an incoherent way at themoment. That is probably the source of the problem. julia > > Best, > Andrei > > On 2 July 2018 at 12:04, Julia Lawall wrote: > Hello, > > I am trying to get my 0.88 code to work with why3 1.0. I have > > use import array.Array as A > use import matrix.Matrix as MM > > According to my understanding, the imports are no longer > needed. I tried: > > use array.Array as A > use matrix.Matrix as MM > > but then it doesn't recognize the type matrix. > > With the imports it doesn't recognize MM.set. What should be > done > instead? > > julia > ___ > 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
Re: [Why3-club] matrix import
On Mon, 2 Jul 2018, Andrei Paskevich wrote: > Hi Julia, > > you simply write "use array.Array" and "use matrix.Matrix" — the import will > be done by default. You wirte "use ... as" when you _don't_ want import. > And, of course, you still can write "use import array.Array as A" if you > want to name the scope "A" _and_ to import it, too. >From what you say it seems like what I have should work. But it does not. I can try to make a small example. julia > > Best, > Andrei > > On 2 July 2018 at 12:04, Julia Lawall wrote: > Hello, > > I am trying to get my 0.88 code to work with why3 1.0. I have > > use import array.Array as A > use import matrix.Matrix as MM > > According to my understanding, the imports are no longer > needed. I tried: > > use array.Array as A > use matrix.Matrix as MM > > but then it doesn't recognize the type matrix. > > With the imports it doesn't recognize MM.set. What should be > done > instead? > > julia > ___ > 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
Re: [Why3-club] matrix import
Hi Julia, you simply write "use array.Array" and "use matrix.Matrix" — the import will be done by default. You wirte "use ... as" when you _don't_ want import. And, of course, you still can write "use import array.Array as A" if you want to name the scope "A" _and_ to import it, too. Best, Andrei On 2 July 2018 at 12:04, Julia Lawall wrote: > Hello, > > I am trying to get my 0.88 code to work with why3 1.0. I have > > use import array.Array as A > use import matrix.Matrix as MM > > According to my understanding, the imports are no longer needed. I tried: > > use array.Array as A > use matrix.Matrix as MM > > but then it doesn't recognize the type matrix. > > With the imports it doesn't recognize MM.set. What should be done > instead? > > julia > ___ > 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
Re: [Why3-club] matrix import
On Mon, 2 Jul 2018, Ralf Treinen wrote: > Hi, > > On Mon, Jul 02, 2018 at 12:04:14PM +0200, Julia Lawall wrote: > > > use array.Array as A > > use matrix.Matrix as MM > > > > but then it doesn't recognize the type matrix. > > > > With the imports it doesn't recognize MM.set. What should be done > > instead? > > the stdlib has changed location. In my case I had to remove my old > ~/.why3.conf et rerun "why3 config". I did that already. I have: loadpath = "/home/jll/.opam/default/share/why3/stdlib" This directory exists and contains the file matrix.mlw. That file defines set. julia > > -Ralf. > -- > Ralf Treinen > Institut de Recherche en Informatique Fondamentale > Équipe Preuves, Programmes et Systèmes > Université Paris Diderot, Paris, France. > http://www.irif.fr/~treinen/ > ___ > 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
Re: [Why3-club] matrix import
Hi, On Mon, Jul 02, 2018 at 12:04:14PM +0200, Julia Lawall wrote: > use array.Array as A > use matrix.Matrix as MM > > but then it doesn't recognize the type matrix. > > With the imports it doesn't recognize MM.set. What should be done > instead? the stdlib has changed location. In my case I had to remove my old ~/.why3.conf et rerun "why3 config". -Ralf. -- Ralf Treinen Institut de Recherche en Informatique Fondamentale Équipe Preuves, Programmes et Systèmes Université Paris Diderot, Paris, France. http://www.irif.fr/~treinen/ ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
