Anthony, I'm copying the mailing list to my replies because this is of general interest.
On 10/02/2016 16:02, Anthony Fox wrote:
I just occurred to me that I could have done:
structure Int :> INTEGER = IntInf
if I wanted IntInf everywhere (rather than having the choice of fixed ot arbitrary). I still think it would be nice to have a command line option for this? At the very least, this way of getting the old behaviour should be advertised.
That would work if you use the Int structure but there are lots of places that pick up the default "int". For instance, if you have an overloaded function: fun f x y = x+y; that will fall back to the default "int". Also, all the library functions that use "int" e.g. Array.sub, String.size, List.length or TextIO.inputN, will still have the fixed precision int.
I'm inclined to think that having a "configure" option would be the answer. David
On Wed, 10 Feb 2016, David Matthews wrote:
fun f x y = x+y; that will fall back to the default "int". Also, all the library functions that use "int" e.g. Array.sub, String.size, List.length or TextIO.inputN, will still have the fixed precision int.
This reminds me of the situation in SML/NJ, before I spent some efforts to force int = IntInf.int on it. It includes a somewhat "patched" basis library like this: http://isabelle.in.tum.de/repos/isabelle/file/9343649abb09/src/Pure/RAW/prop...
I'm inclined to think that having a "configure" option would be the answer.
That would greatly simplify the Isabelle setup, because we always provide a separately compiled version of Poly/ML.
Since we are about to discontinue SML/NJ altogether, it would allow to remove the above tricks, and not move them over to Poly/ML.
Makarius
On 10 Feb 2016, at 17:01, Makarius <makarius at sketis.net> wrote:
On Wed, 10 Feb 2016, David Matthews wrote:
This reminds me of the situation in SML/NJ, before I spent some efforts to force int = IntInf.int on it. It includes a somewhat "patched" basis library like this: http://isabelle.in.tum.de/repos/isabelle/file/9343649abb09/src/Pure/RAW/prop...
ProofPower takes a different approach to this: it uses the compiler's native integers except where logical soundness requires an IntInf, where it uses a type it defines called INTEGER, which has its own operations @+, @-, @* etc. implemented using the operators of Int or IntInf as appropriate (selected at compile-time by using a conditional compilation feature that is built into the way ProofPower packages ML code into documents).
ProofPower builds and tests fine using poly built from the FixedPrecisionInt branch after tweaking the conditionally compiled bits of code so that Poly/ML is treated just like Standard ML of New Jersey in the definition of the type INTEGER. (And tweaking a few tests that accidentally forgot that INTEGER and int are not necessarily the same.)
I'm inclined to think that having a "configure" option would be the answer.
I think that's a good idea, but it gives me a bit of problem as my conditial compilation is based on the compiler and not how the compiler has been configured.
That would greatly simplify the Isabelle setup, because we always provide a separately compiled version of Poly/ML.
I can see why you do that, but I don't want to do it for ProofPower. So if we have a "configure" option, then it would be good for me if there some well-defined way, e.g., using "poly -v", for a build script to find out how a pre-installed Poly/ML installation has been configured.
Since we are about to discontinue SML/NJ altogether, it would allow to remove the above tricks, and not move them over to Poly/ML.
I can unerstand why you are doing that too, but in this case I'm really glad I tried to maintain compatibility, as it meant I already had almost everything I needed to accommodate the proposed change :-).
All that said, I would be surprised if the change made any significant performance improvement on any of my code, because anything that is computationally intensive in the theorem prover tends to be dealing with object language data, and, if that data is numeric, it will be arbitrary precision.
Regards,
Rob.
On Wed, 10 Feb 2016, Rob Arthan wrote:
ProofPower takes a different approach to this: it uses the compiler's native integers except where logical soundness requires an IntInf, where it uses a type it defines called INTEGER, which has its own operations @+, @-, @* etc. implemented using the operators of Int or IntInf as appropriate (selected at compile-time by using a conditional compilation feature that is built into the way ProofPower packages ML code into documents).
We used to have separate Int vs. IntInf over a few years (2004-2007), but it was so awkward in mixed tool implementations that people knocked at my door and were asking for more uniformity. So I made some tricks to get int = IntInf.int in SML/NJ.
Now I've started to think about separate int types again, but it would probably be a big upheaval in parts of the system that don't have active maintainers.
Since we are about to discontinue SML/NJ altogether, it would allow to remove the above tricks, and not move them over to Poly/ML.
I can unerstand why you are doing that too, but in this case I'm really glad I tried to maintain compatibility, as it meant I already had almost everything I needed to accommodate the proposed change :-).
The reason for thinking about discontinuation of SML/NJ is not its constant annoyance wrt. type errors, but more profane: many Isabelle sessions run out of memory, even basic things like HOL-Library. So the question needs to be revisted seriously in a few weeks on isabelle-dev mailing list -- it will have far-reaching consequences to have just one ML platform.
Makarius
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
rda＠lemma-one.com