Hi all,
Is PolyML development dead? Is it safe to keep developing ML programs dependent on PolyML compiler?
Cheers,
Paulo> Hi all, Is PolyML development dead? Is it safe to keep developing Paulo> ML programs dependent on PolyML compiler?
How does your program depend on PolyML, specifically? It is quite close to complete conformance to the standard, after all. The one problem is that its Basis library is getting quite out of date, because the standard keeps changing in that respect.
If you ask "is it safe to keep developing for an obsolete Basis" I'd say no, because the next release of PolyML, if it comes, will fix the library and break your code. I don't know if there's a choice, though. Maybe you could grab some other compiler's Basis and link it with your code.
Paulo> So, he wrote it all in Lisp!
More precisely, Scheme :-)
On 16 Mar 2004, at 04:24, Ian Zimmerman wrote:
The one problem is that its Basis library is getting quite out of date, because the standard keeps changing in that respect.
Does anybody know what is really going on with the Basis Library?
When the 2nd edition of my ML book appeared (in 1996!) I had the problem of attempting to track the changes to the Library. I was promised that there would be a feature freeze very soon, but it never happened. Even after the book went to press, major changes were made that affected the text. Some of these, such as removing the equality operator on type real, struck me as being ill-advised.
I can't believe they are still tinkering with it eight years later.
Larry Paulson
Now I got it...
This "Which SML compiler is best? question is giving me a lot of headache lately!". I'm doing my master thesis on a sort of Isabelle plugin for automated theorem proving. In the beginning I didn't know SML so I though, "Well, I know scheme, I'll do it in scheme and I use some FFI and inverse FFI that usually comes with compilers"... at least I knew scheme was able to do it. After some discussion in #sml @ freenode and some personal research I found that it would take a 'temporary thesis' (as some named it) to create bindings between scheme and sml so I got ML for the Working Programmer and started reading it. Soon I found that SMLNJ was not able to do fact 35, without overflowing, like you did in the book and I asked yesterday at #sml @ freenode which compiler would be able to do that (maybe a compiler with infinite precision, which I initially thought it would be a ML standard requirement). Now, I get it... You used PolyML. :D This makes me a bit 'sad' since I've read some times (not only in the Isabelle Mailing List but also on the web) that PolyML would be better to run Isabelle (since it makes Isabelle a lot of faster) but I thought (and now I'm almost sure) that I shouldn't develop my 'isabelle plugin' (let's call it this way, however you can interpret it as a tactic, if you want, since it is inspired in blast_tac) in PolyML since it seems completely dead and the documentation seems pre-historic. So, it seems to me this is somehow a difficult choice, should I choose between developing on a dead compiler or on a slow compiler (regarding Isabelle)?
Cheers,
Paulo Matos
On Tue, 2004-03-16 at 09:37, Lawrence Paulson wrote:
On 16 Mar 2004, at 04:24, Ian Zimmerman wrote:
The one problem is that its Basis library is getting quite out of date, because the standard keeps changing in that respect.
Does anybody know what is really going on with the Basis Library?
When the 2nd edition of my ML book appeared (in 1996!) I had the problem of attempting to track the changes to the Library. I was promised that there would be a feature freeze very soon, but it never happened. Even after the book went to press, major changes were made that affected the text. Some of these, such as removing the equality operator on type real, struck me as being ill-advised.
I can't believe they are still tinkering with it eight years later.
Larry Paulson
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 16 Mar 2004, at 10:58, Paulo Jorge de Oliveira Cantante de Matos wrote:
should I choose between developing on a dead compiler or on a slow compiler ?
Poly/ML is not dead. Dave Matthews continues to support and develop it.
Larry Paulson
On Tuesday, Mar 16, 2004, at 00:25 Europe/London, Paulo Jorge de Oliveira Cantante de Matos wrote:
Is PolyML development dead? Is it safe to keep developing ML programs dependent on PolyML compiler?
Poly/ML is certainly not "development dead". I do continue to work on it and fix bugs but since this is a largely voluntary endeavour I need to fit this round my other work. My approach has always been to create a stable and efficient platform for writing Standard ML programs rather than to use it as a platform for experimentation. That tends to mean that new releases are infrequent and only when there is a significant change rather than producing a new release every few months. From feedback in the past I feel that this suits the users of Poly/ML better.
There is a specific question about the Basis library. I really don't know when this will be frozen. At one stage it was due to come out as a book, then it sounded as though the contract had been terminated, then I heard that it was supposed to be coming out as a book from CUP. I had intended to wait until the book came out and bring the Basis library in Poly/ML up to date with it so that it would be clear what version of the library Poly/ML supported. Since it was always due "in the next few months" that seemed like the right approach. I'm quite prepared to revisit the Basis library code and bring it a bit more up to date if that's what people would like. The question is which version.
Finally, Poly/ML is open-source. If someone wants a feature in Poly/ML badly enough they can always add it themselves. I'm happy to work with anyone who wants to do development work. If it seems sensible I'll add it to the source I maintain at polyml.org. The same goes for documentation. Although I maintain the version on polyml.org there's nothing to stop anyone else from distributing their version. Perhaps the fact that there isn't a constant stream of changes means that users are fairly content with Poly/ML as it is.
Regards, David.
On Tuesday 16 March 2004 12:13, you wrote:
On Tuesday, Mar 16, 2004, at 00:25 Europe/London, Paulo Jorge de
Is PolyML development dead? Is it safe to keep developing ML programs dependent on PolyML compiler?
Finally, Poly/ML is open-source. If someone wants a feature in Poly/ML badly enough they can always add it themselves.
...
If it seems sensible I'll add it to the source I maintain at polyml.org. The same goes for documentation. Although I maintain the version on polyml.org there's nothing to stop anyone else from distributing their version.
Apart from this, perhaps? "If you are downloading this in order to make it available to others, for example to install it on a server at your University or place of work, you agree that everyone who has use of Poly/ML will abide by this licence." [1]
That surely can't be feasible.
I'm happy to work with anyone who wants to do development work.
Yet, when asked about the issues relating to the license you don't answer? [2] For the sake of curiosity - was the license chosen, or was it imposed by a university IPR policy?
My interest is the result of frustration at the lack of easily available (by that I guess I mean tidily packaged) formal methods tools. While evaluating potential tool support for my PhD work, I have in several cases spent longer installing tools than using them. (I dread to how long it will take to reinstall on a new machine...)
There seem to be many examples of such tools not being easily distributable to a broad(er) community because of license problems: - HOL4 has a BSD license, but it depends on MoscowML (which some copyright issues) - NuSMV (LGPL) depends on a BDD library, with no license information - Isabelle (whose license appears to allow distribution) depends on PolyML (whose license doesn't appear to - see above) - LETOS, I think, had similar problems, but I gave up on it a long time ago.
Of course, this is all just two cents of off-topic rant - and most of the questions here are slightly rhetorical - but I can't be the first to have had these problems? FWIW, I'm sure I would have offered contributions if it wasn't for these problems.
Martin Ellis
[1] http://www.polyml.org/Get.html [2] http://lists.debian.org/debian-legal/2002/debian-legal-200207/msg00016.html
- Isabelle (whose license appears to allow distribution) depends on
PolyML (whose license doesn't appear to - see above)
Isabelle does not depend on PolyML (or its license...). You can use it with SMLNJ. Whether or not smlnj license is better, I don't know.
Cheers,
Paulo> Isabelle does not depend on PolyML (or its license...). You can Paulo> use it with SMLNJ. Whether or not smlnj license is better, I Paulo> don't know.
SMLNJ is classic GPL, so license-wise at least it wins.
I wrote:
Ian> SMLNJ is classic GPL, so license-wise at least it wins.
Oops, my bad. Looks more like BSD + advertising clause. Sorry.
The licensing situation for Poly/ML is complicated because of its history. I originally wrote Poly/ML nearly twenty years ago when I was a post-doc at Cambridge. In those days there wasn't the same attitude to making software freely available especially as distribution was a matter of half-inch tapes in Jiffy bags. As an employee of the university the rights were split between myself as author, the university and the SRC who had provided the grant. I transferred my rights to the university's company, originally called Lynxvale later renamed CUTS, who after some false starts agreed a licensing deal with Abstract Hardware (AHL). AHL then wrote the X-Windows code, translated the original Poly code into Standard ML and did much of the work on the i386 port. When AHL went bust that left the rights split between CUTS and AHL's liquidators. I eventually managed to persuade the liquidators to transfer AHL's intellectual property to CUTS on condition that the customers of AHL's other intellectual property could use Poly/ML. So, I personally own very little of the intellectual property rights in Poly/ML, really only work done since it went open source, for instance the Basis library code.
The present licence was based on the BSD licence. It was drafted by a lawyer at Edinburgh and after a long delay it was finally signed by CUTS. A number of people looked at it particularly at LFCS in Edinburgh and made suggestions. The clause that seems to be causing problems was inserted largely to prevent the situation where a company developed, say, a new code-generator, and didn't make it available to everyone. On the other hand, GPL is too strong because it would appear to make it impossible for a company to develop software and distribute it with Poly/ML in such a way that they could retain their code as closed source. It's possible that the "Lesser GPL" that is used for libraries might be acceptable.
Any change to the licence would have to be agreed by CUTS and given the time I spent trying to get them to sign the current licence I feel there would have to be a convincing case to make changes. If people really are being discouraged from contributing to Poly/ML or using it then I might be able to make a case.
On Tuesday, Mar 16, 2004, at 16:19 Europe/London, Martin Ellis wrote:
Apart from this, perhaps? "If you are downloading this in order to make it available to others, for example to install it on a server at your University or place of work, you agree that everyone who has use of Poly/ML will abide by this licence." [1]
That surely can't be feasible.
Most universities require their students and staff to agree to abide by software licensing rules. That would be quite sufficient.
I'm happy to work with anyone who wants to do development work.
Yet, when asked about the issues relating to the license you don't answer? [2]
That particular message was posted to the Debian legal mailing list. Previous messages in the thread had been copied to me and I replied and copied my reply to the list. I don't read the list so naturally I didn't see that message.
David.
David, Thanks for the history. Like the historical digressions in the aforementioned 'ML for the Working Programmer', I find such explanations more interesting than the actual programming!
On Wednesday 17 March 2004 09:55, David Matthews wrote:
Any change to the licence would have to be agreed by CUTS and given the time I spent trying to get them to sign the current licence I feel there would have to be a convincing case to make changes. If people really are being discouraged from contributing to Poly/ML or using it then I might be able to make a case.
Well, I count two examples covered in this thread already. :o)
That surely can't be feasible.
Most universities require their students and staff to agree to abide by software licensing rules. That would be quite sufficient.
OK. Point taken. As long as one is not bothered about making their own version/build widely available, I guess that's adequate.
That particular message was posted to the Debian legal mailing list. Previous messages in the thread had been copied to me and I replied and copied my reply to the list. I don't read the list so naturally I didn't see that message.
Yep. Apologies - I see that now.
On Tuesday, Mar 16, 2004, at 16:19 Europe/London, Martin Ellis wrote:
Of course, this is all just two cents of off-topic rant
And, OK. Touch' e. I was wrong about Isabelle depending on PolyML. SML/NJ didn't work for me, so in my head Isabelle did indeed depend on PolyML. But I maintain my point that -in general- many tools we use 'suffer' in some way from their own licenses or those of related software, perhaps it was a wee bit off-topic here, I did warn you!
Regards, Martin
On Tuesday 16 Mar 2004 12:13 pm, David Matthews wrote:
On Tuesday, Mar 16, 2004, at 00:25 Europe/London, Paulo Jorge de
Oliveira Cantante de Matos wrote:
Is PolyML development dead? Is it safe to keep developing ML programs dependent on PolyML compiler?
Poly/ML is certainly not "development dead". I do continue to work on it and fix bugs but since this is a largely voluntary endeavour I need to fit this round my other work. My approach has always been to create a stable and efficient platform for writing Standard ML programs rather than to use it as a platform for experimentation. That tends to mean that new releases are infrequent and only when there is a significant change rather than producing a new release every few months. From feedback in the past I feel that this suits the users of Poly/ML better. ...
I endorse that completely. ProofPower compiles on both Poly/ML and SML/NJ but it's always been a lot more trouble keeping track of SML/NJ. The situation is particular bad on Mac OS X at the moment, where the only version of SML/NJ is much later than the version that's advertised as stable, and you need a source patch to work-around the differences between the basis library changes. As Poly/ML is leaner and faster for ProofPower, I much prefer it.
On Tuesday 16 Mar 2004 4:19 pm, Martin Ellis wrote:
On Tuesday 16 March 2004 12:13, you wrote:
On Tuesday, Mar 16, 2004, at 00:25 Europe/London, Paulo Jorge de
Is PolyML development dead? Is it safe to keep developing ML programs dependent on PolyML compiler?
Finally, Poly/ML is open-source. If someone wants a feature in Poly/ML badly enough they can always add it themselves.
...
If it seems sensible I'll add it to the source I maintain at polyml.org. The same goes for documentation. Although I maintain the version on polyml.org there's nothing to stop anyone else from distributing their version.
Apart from this, perhaps? "If you are downloading this in order to make it available to others, for example to install it on a server at your University or place of work, you agree that everyone who has use of Poly/ML will abide by this licence." [1]
I agree that this is a bit tricky. However, it seems to be part of the "agreement" rather than the licence itself. I suspect it would have no force whatsoever in law, since it's unenforceable and the "agreement" isn't a contract in law in any case (and nor is the licence).
I actually think this business of getting people to push an "agree" button is misleading. It's giving the mistaken impression that the licence imposes obligations on the user (as a contractual licence can do, e.g., to pay the licence fee). An open source licence is really just a public statement by a supplier of conditions under which a user can reasonably expect to use the software without risk of the contractor suing for misuse of IPR. I don't think it matters whether the user has in any sense "agreed" to the licence unless it's become the basis of a contract with a vendor.
It would be nicer to say something more practical. E.g. "you agree to make the terms of the licence known to everyone who has use of Poly/ML". This could easily be achieved by putting the text of the licence in the software somewhere. Of course, if the inclusion of this precise form of words was a CUTS requirement, David may find it hard to get it changed.
On Wednesday 17 Mar 2004 9:55 am, David Matthews wrote:
... The present licence was based on the BSD licence. It was drafted by a lawyer at Edinburgh and after a long delay it was finally signed by CUTS. A number of people looked at it particularly at LFCS in Edinburgh and made suggestions. The clause that seems to be causing problems was inserted largely to prevent the situation where a company developed, say, a new code-generator, and didn't make it available to everyone. On the other hand, GPL is too strong because it would appear to make it impossible for a company to develop software and distribute it with Poly/ML in such a way that they could retain their code as closed source. It's possible that the "Lesser GPL" that is used for libraries might be acceptable.
I think the GPL is actually much less restrictive than many people think (ProofPower is distributed under GPL, although I did agonise over this for a long time).
The relevant paragraph of the GPL is this:
2 b) You must cause any work that you distribute or publish, that in whole or in part contains or is derived from the Program or any part thereof, to be licensed as a whole at no charge to all third parties under the terms of this License.
I don't believe that code compiled with a compiler counts as "derived from the compiler". The situation would, of course, be a bit less muddy if one had true separate compilation for ML (but even with gcc, compiled object code will contain compiled open source libraries, and I don't believe that the above paragraph means you can't sell binaries compiled with gcc).
Regards and apologies for this long off-topic diversion,
Rob.
-
David.Matthews＠deanvillage.com -
itz＠buug.org -
lp15＠cam.ac.uk -
m.a.ellis＠ncl.ac.uk -
pocm＠netvisao.pt -
rda＠lemma-one.com