I have made debian packages for 4.2.0, to be found at
http://primate.net/~itz/debian/polyml
Tested only on i386.
I added a bit of infrastructure to maintain the chain of child databases for libraries. I myself intend to package a couple of libraries from the net, such as FGL and FXP. Later I'll tackle either Isabelle or ProofPower, but that will be a much bigger job.
Hi, On Tue, Sep 05, 2006 at 09:21:54AM -0400, Ian Zimmerman wrote:
I added a bit of infrastructure to maintain the chain of child databases for libraries. I myself intend to package a couple of libraries from the net, such as FGL and FXP. Later I'll tackle
do you have FXP (I assume you mean the XML Parser, aren't you) runnign with PolyML. I thought PolyML still lacks the Word32 structure which is needed by FXP. At least for us, the workaround of using LargeWord instead of Word32 resulted in a non-functional fxp...
either Isabelle or ProofPower, but that will be a much bigger job.
Debian Packages for Isabelle 2005 (based on sml/nj) and Proof General are available from my website:
http://www.brucker.ch/projects/debian/
The packages should be easily rebuild-able with Polyml. At the moment I'm using sml/nj mainly because HOL-OCL depends on FXP. If FXP can be used with Polyml I will happily provide Polyml-based Isabelle packages. In that case, I would propaply used these packages for the next IsaMorph release (A linux live CD which includes Isabelle).
Achim
Ian> I added a bit of infrastructure to maintain the chain of child Ian> databases for libraries. I myself intend to package a couple of Ian> libraries from the net, such as FGL and FXP.
Achim> do you have FXP (I assume you mean the XML Parser, aren't you) Achim> runnign with PolyML. I thought PolyML still lacks the Word32 Achim> structure which is needed by FXP. At least for us, the workaround Achim> of using LargeWord instead of Word32 resulted in a non-functional Achim> fxp...
No, I haven't tried. Do you know why using LargeWord failed? Maybe this will require actually adding Word32, shouldn't be too hard.
Achim> Debian Packages for Isabelle 2005 (based on sml/nj) and Proof Achim> General are available from my website:
Achim> http://www.brucker.ch/projects/debian/
I'll look, thanks. Chances are I'll have criticisms as I'm the retentive type. But in the end we should build both SMLNJ based and Poly/ML based packages from the same debianized source.
Ian Zimmerman wrote:
Achim> do you have FXP (I assume you mean the XML Parser, aren't you) Achim> runnign with PolyML. I thought PolyML still lacks the Word32 Achim> structure which is needed by FXP. At least for us, the workaround Achim> of using LargeWord instead of Word32 resulted in a non-functional Achim> fxp...
No, I haven't tried. Do you know why using LargeWord failed? Maybe this will require actually adding Word32, shouldn't be too hard.
Presumably the code is relying on the wrap-around semantics of Word32. It shouldn't be difficult to write a Word32 structure based on LargeWord which masked the result of calculations with 0wxffffffff .
David
-
brucker＠spamfence.net -
David.Matthews＠prolingua.co.uk -
itz＠madbat.mine.nu